High-integrity Java Applications using Circus

Lead Research Organisation: University of York
Department Name: Computer Science

Abstract

The use of computers and computer programs is pervasive nowadays, but every computer user knows that programs go wrong. While it is just annoying when our favourite text editor loses a bit of our work, the consequences are potentially much more serious when a computer program that, for instance, controls parts of an airplane goes wrong. Software validation and verification are central to the development of this sort of application. In fact, the software industry in general spends a very large amount of money in these activities. One of the measures taken to promote correctness of programs is the use of a restricted set of features available in programming languages. This usually means that most of the more recent advances in software engineering are left out. In this project, we propose to provide development, validation, and verification facilities that allow object-orientation and a modern real-time computational model to be used for the programming of safety-critical systems. In particular, we will work with one of the most popular programming languages: Java, or more specifically, its profiles for high-integrity engineering proposed by the Open Group. As our main case study, we will verify parts of the controller of the first Java Powered Industrial Robot, developed by Sun. One of our collaborators, a senior engineer in Sun tells in an interview that Distributed Real-Time Systems are really hard to build and the engineering community doesn't really know how to build them in a coherent repeatable way. (java.dzone.com/articles) Real-Time Java is entering the industrial automation and automotive markets. Lawyers did not allow the Java Robot to get anywhere near a human, even in a JavaOne conference demo. To proceed in that kind market, better support is needed.Programming is just one aspect of the development of a modern system; typically, a large number of extra artefacts are produced to guide and justify its design. Just like several models of a large building are produced before bricks and mortar are put together, several specification and design models of a program are developed and used before programs are written. These models assist in the validation and verification of the program. To take our civil engineering metaphor one step further, we observe that, just like there can be various models of a building that reflect several points of view, like electricity cabling, plumbing, and floor plans, for example, we also have several models of a system. Different modelling and design notations concentrate on different aspects of the program: data models, concurrent and reactive behaviour, timing, and so on. No single notation or technique covers all the aspects of the problem, and a combination of them needs to be employed in the development of large complex systems. In this project, we propose to investigate a novel integrated approach to validation and verification. Our aim is to provide a sound and practical technique that covers data modelling, concurrency, distribution, and timing. For that, we plan to investigate the extension and combined use of validation and verification techniques that have been successfully applied in industry. We do not seek an ad hoc combination of notations and tools, but a justified approach that provides a reliable foundation for the use of practical techniques. We will have succeeded if we verify a substantial part of the robot controller: using a model written in our notation, we will apply our techniques to verify parts of the existing implementation, execute it using our verified implementation of Safety-critical Java. Measure of success will be provided by our industrial partners and the influence of our results in their practice or business plans.

Publications

10 25 50
 
Description The use of computers and computer programs is pervasive nowadays, but every computer user knows that programs go wrong. While it is just annoying when our favourite text editor loses a bit of our work, the consequences are potentially much more serious when a computer program that, for instance, controls parts of an airplane goes wrong. Software validation and verification are central to the development of this sort of application. In fact, the software industry in general spends a very large amount of money in these activities.
One of the measures taken to promote correctness of programs is the use of a restricted set of features available in programming languages. This usually means that most of the more recent advances in software engineering are left out. In this project, we have desgined techniques to support development, validation, and verification facilities that allow modern programming technology (object-orientation and an advanced real-time computational model) to be used in safety-critical systems. In particular, we have considered one of the most popular programming languages: Java and its two profiles for high-integrity engineering proposed by the Open Group, namely SCJ (Safety-Critical Java) Levels 1 and 2. We have also produced a technique to allow the verification that the extra software that needs to run in machines to enable the execution of SCJ programs is correct and in accordance with the Open Group Standard.
Exploitation Route Others can use our results by adopting Java as a programming language, in particular, the version for safety-critical systems. They are now in a position to consider the application of verification techniques based on mathematics (formal methods) as suggested by regulators (DO-178C), for instance. The Open Group that is responsible for the standardisation of SCJ has been benefiting of our results. We are in constant contact, and have influenced the evolution of the SCJ language in many ways. There are many ways in which the research can be taken forward. The suitability of the techniques has generated theoretical results (namely, semantic theories for time and object orientation) that are particular assets of general interest. The SCJ standardisation group has considered the possibility of combining SCJ with another programming language, called Scala, to ease validation and verification. This imposes challenges in terms of the implementation platform for SCJ, and we are discussing with colleagues the development of verified platforms of mixed criticality. We now have developed techniques to enable verification of programming platforms for SCJ.
Sectors Aerospace, Defence and Marine,Agriculture, Food and Drink,Digital/Communication/Information Technologies (including Software),Electronics,Healthcare,Transport

URL http://www.cs.york.ac.uk/circus/hijac/index.html
 
Description Yes, they have been used by the Open Group that is in charge of defining Safety-Critical Java. We are in close contact, and have influenced several aspects of the definition of the language. These cover core aspects of Safety-Critica Java: its schedule and memory management mechanisms.
First Year Of Impact 2011
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Economic

 
Description EPSRC Standard Grant
Amount £1,776,973 (GBP)
Funding ID EP/R025479/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 04/2018 
End 03/2023
 
Description EU FP7
Amount € 1,000,000 (EUR)
Organisation European Commission 
Sector Public
Country European Union (EU)
Start 10/2011 
End 09/2014
 
Description EU Horizon 2020
Amount € 900,000 (EUR)
Organisation European Commission 
Sector Public
Country European Union (EU)
Start 01/2015 
End 12/2017
 
Description International Exchanges Scheme
Amount £9,900 (GBP)
Organisation The Royal Society 
Sector Academic/University
Country United Kingdom
Start 03/2012 
End 03/2014
 
Description Newton Mobility Grant
Amount £12,000 (GBP)
Organisation The Royal Society 
Sector Academic/University
Country United Kingdom
Start 12/2015 
End 11/2017
 
Description RAEng Brazil 1
Amount £24,000 (GBP)
Funding ID NRCP1617/5/68 
Organisation Royal Academy of Engineering 
Sector Learned Society
Country United Kingdom
Start 06/2016 
End 07/2017
 
Description RAEng Brazil 2
Amount £24,000 (GBP)
Funding ID NRCP1617/6/164 
Organisation Royal Academy of Engineering 
Sector Learned Society
Country United Kingdom
Start 01/2017 
End 01/2018
 
Description Butterfield TCD UTP 
Organisation Trinity College Dublin
Department School of Computer Science and Statistics
Country Ireland 
Sector Academic/University 
PI Contribution I have been collaborating with Andrew Butterfield since 2002 on Unifying Theories of Programming (UTP) and the formal semantics of of real-time, hybrid, and probabilistic systems. We meet regularly (at least twice a year) and have published 10 joint papers (five journal and five refereed conference papers). I have made contributions in foundations of UTP (including donating extensive course materials) and in applications to systems of systems and robotic and autonomous systems.
Collaborator Contribution Andrew Butterfield at TCD has made contributions to understanding hardware/software co-design and real-time and probabilistic systems. He contributed a strong background in functional programming.
Impact Outputs: DOIs: 10.1007/978-3-319-47166-2_26 10.1016/j.scico.2008.09.014 10.1109/TASE.2009.57 10.1109/ICECCS.2008.35 10.1109/ICECCS.2007.23 10.1007/978-3-540-73210-5_5 10.1016/j.entcs.2006.04.026 10.1007/s10009-004-0181-6 10.1016/S1571-0661(04)80821-1 10.1016/S1571-0661(04)80762-X The collaboration is multi-disciplinary, involving computer science and electronic engineering.
 
Description D'Souza IISc Verification 
Organisation Indian Institute of Science
Department Department of Computer Science and Automation
Country India 
Sector Academic/University 
PI Contribution My team contributed expertise in formal specification, refinement, and verification of software. We contributed to the verification of FreeRTOS, the popular open-source real-time operating system. We helped our Indian colleagues develop expertise in Z and Z/Eves and helped them apply it to verification problems.
Collaborator Contribution Colleagues at the Indian Institute of Science and General Motors India helped us to understand the FreeRTOS code and extract suitable abstract specifications of aspects of its behaviour.
Impact Three projects funded by the British Council, the Royal Academy of Engineering, and the Robert Bosch Centre for Cyber-Physical Systems (total value £175k). One conference paper (10.1007/978-3-319-25423-4_11). One journal paper (10.1007/s00165-014-0308-9). Two Phd theses: Sumesh Divakaran: A Refinement-Based Methodology for Verifying Abstract Data Type Implementations (IISc, 2015). Shu Cheng: Formally modelling and verifying the FreeRTOS real-time operating system (York, 2014).
Start Year 2010
 
Description FitzLarsen CPS EU 
Organisation Aarhus University
Department School of Engineering
Country Denmark 
Sector Academic/University 
PI Contribution Our collaboration has involved two major EU projects. My research team brought expertise in modelling, formal semantics, mechanised proof, and model checking.
Collaborator Contribution Newcastle made contribution in modelling and methods. Aarhus made contributions in tool building.
Impact Also see http://www.compass-research.eu/. Outputs: Funding for two large EU projects. Publications: 8 conference papers, 4 journal papers, 2 book chapters. Citations: > 600 in total. Multi-disciplinary collaboration covering systems, software, hardware, control theory, and electronics.
Start Year 2009
 
Description Formal testing 
Organisation University Paris Sud
Country France 
Sector Academic/University 
PI Contribution All the work on formal model-based testing based on the notation of relevance.
Collaborator Contribution This is a scientific collaboration, and we developed testing theories and techniques in collaboration.
Impact A. Alberto, A. L. C. Cavalcanti, M.-C. Gaudel, and A. Simao. Formal mutation testing for Circus. Information and Software Technology, pages --, 2016. [ bib | DOI | .pdf ] A. L. C. Cavalcanti and M.-C. Gaudel. Test selection for traces refinement. Theoretical Computer Science, 563(0):1 - 42, 2015. A. L. C. Cavalcanti and M.-C. Gaudel. Data Flow coverage for Circus-based testing. In Fundamental Approaches to Software Engineering, volume 8441 of Lecture Notes in Computer Science, pages 415-429, 2014. A. L. C. Cavalcanti and M.-C. Gaudel. Testing for Refinement in Circus. Acta Informatica, 48(2):97-147, 2011. A. L. C. Cavalcanti, M.-C. Gaudel, and R. M. Hierons. Conformance Relations for Distributed Testing based on CSP. In B. Wolff and F. Zaidi, editors, IFIP International Conference on Testing Software and Systems, Lecture Notes in Computer Science. Springer-Verlag, 2011. A. L. C. Cavalcanti and M.-C. Gaudel. Specification Coverage for Testing in Circus. In S. Qin, editor, Unifying Theories of Programming, volume 6445 of Lecture Notes in Computer Science, pages 1-45. Springer-Verlag, 2010. A. L. C. Cavalcanti and M.-C. Gaudel. A note on traces refinement and the conf relation in the Unifying Theories of Programming. In A. Butterfield, editor, Unifying Theories of Programming 2008, volume 5713 of Lecture Notes in Computer Science. Springer-Verlag, 2010. A. L. C. Cavalcanti and M.-C. Gaudel. Testing for Refinement in CSP. In 9th International Conference on Formal Engineering Methods, volume 4789 of Lecture Notes in Computer Science, pages 151-170. Springer-Verlag, 2007.
Start Year 2007
 
Description Process-algebra based testing for refinement with inputs and outputs 
Organisation Brunel University London
Department Department of Education
Country United Kingdom 
Sector Academic/University 
PI Contribution Expertise in process algebra and refinement, and testing for refinement based on process algebra.
Collaborator Contribution Testing with inputs and outputs and distributed systems.
Impact A. L. C. Cavalcanti, R. M. Hierons, S. Nogueira, and A. C. A. Sampaio. A suspension-trace semantics for CSP. In International Symposium on Theoretical Aspects of Software Engineering, pages 3--13, 2016. Invited paper. A. L. C. Cavalcanti, M.-C. Gaudel, and R. M. Hierons. Conformance Relations for Distributed Testing based on CSP. In B. Wolff and F. Zaidi, editors, IFIP International Conference on Testing Software and Systems, Lecture Notes in Computer Science. Springer-Verlag, 2011. A. L. C. Cavalcanti and R. M. Hierons. Testing with Inputs and Outputs in CSP. In Fundamental Approaches to Software Engineering, volume 7793 of Lecture Notes in Computer Science, pages 359-374, 2013.
Start Year 2011
 
Description SCJ VM Verification 
Organisation Newcastle University
Country United Kingdom 
Sector Academic/University 
PI Contribution We are working together on the verification of an SCJ VM. In our group, we are contributing to the development of the virtual macine.
Collaborator Contribution They are leading the modelling of the virtual machine and the proof that it is correct.
Impact L. Freitas, J. Baxter, A. L. C. Cavalcanti, and A. Wellings. Modelling and verifying a priority scheduler for an SCJ runtime environment. In Integrated Formal Methods, Lecture Notes in Computer Science. Springer, 2016. J. Baxter, A. L. C. Cavalcanti, A. J. Wellings, and L. Freitas. Safety-Critical Java Virtual Machine Services. In L. Ziarek, editor, 13th International Workshop on Java Technologies for Real-time and Embedded Systems, pages 7:1--7:10. ACM, 2015.
Start Year 2014
 
Description Testing from Circus with Mealy Machines 
Organisation University of Sao Paulo
Department Institute of Mathematical and Computer Sciences (ICMC)
Country Brazil 
Sector Academic/University 
PI Contribution Expertise on model-based testing based on process algebras and resfinement.
Collaborator Contribution Expertise on testing based on Mealy machines.
Impact Publications: (1) A. Alberto, A. L. C. Cavalcanti, M.-C. Gaudel, and A. Simao. Formal mutation testing for Circus. Information and Software Technology, 81:131--153, 2017. (2) A. L. C. Cavalcanti and A. Simao. Fault-based testing for refinement in CSP. In N. Yevtushenko, A. R. Cavalli, and H. Yenigün, editors, 29th IFIP WG 6.1 International Conference on Testing Software and Systems, volume 10533 of Lecture Notes in Computer Science, pages 21--37. Springer, 2017.
Start Year 2015
 
Title Mechanised Unifying Theories of Programming 
Description Mechanisation of a framework for reasoning about notations and techniques for refinement. The concept was developed on an industrial theorem prover, ProofPower-Z, adopted by our industrial collaborator. More recently, we have implemented the design using a theorem prover of more general use: Isabelle. It has been used in an EU project to verify Systems of Systems. 
Type Of Technology Software 
Year Produced 2010 
Open Source License? Yes  
Impact It has been relevant for all our research and will continue to support our work, as we consider different areas of application: robotics, medical devices, and so on. 
 
Description Hay Festival session 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Public/other audiences
Results and Impact More than 300 people attended, and the presentation sparked many questions and discussion afterwards.

I have been asked by the Royal Society to participate of a campaign to encourage colleagues to engage with the public.
Year(s) Of Engagement Activity 2013
 
Description Open Day 
Form Of Engagement Activity Participation in an open day or visit at my research institution
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Schools
Results and Impact Presentation of robotic applications developed using our techniques.
Year(s) Of Engagement Activity 2016
 
Description Spring School on Engineering Trustworthy Software Systems 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Spring School on Engineering Trustworthy Software Systems (SETSS), held in April, 2016, at Southwest University in Chongqing, China. The school was aimed at post-graduate students, researchers, academics, and industrial engineers who are interested in the theory and practice of methods and tools for the design and programming of
trustworthy software systems.
Year(s) Of Engagement Activity 2016