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.
Organisations
- University of York, United Kingdom (Lead Research Organisation)
- Universidade de São Paulo (Collaboration)
- University of Paris South 11, France (Collaboration)
- Aarhus University, Denmark (Collaboration)
- Brunel University London, Uxbridge (Collaboration)
- Newcastle University, United Kingdom (Collaboration)
- Grants Admin Office (Collaboration)
- Indian Institute of Science Bangalore, India (Collaboration)
- Sun Microsystems, United Kingdom (Project Partner)
- IBM, United States (Project Partner)
- Altran UK Ltd, United Kingdom (Project Partner)
- AWE, United Kingdom (Project Partner)
Publications

Alberto A
(2017)
Formal mutation testing for Circus
in Information and Software Technology

Antonino P
(2014)
FM 2014: Formal Methods

Baxter J
(2015)
Safety-Critical Java Virtual Machine Services

Baxter J
(2017)
Integrated Formal Methods

Baxter James
(2018)
Ahead-of-time algebraic compilation for safety-critical Java

Bryans J
(2014)
SysML contracts for systems of systems

Canham S
(2015)
Unifying Theories of Programming

Carvalho G
(2014)
Formal Methods and Software Engineering

Carvalho G
(2016)
Modelling timed reactive systems from natural-language requirements
in Formal Aspects of Computing

Carvalho G
(2015)
Software Engineering and Formal Methods
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 | Public |
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 | Charity/Non Profit |
Country | United Kingdom |
Start | 03/2012 |
End | 03/2014 |
Description | Newton Mobility Grant |
Amount | £12,000 (GBP) |
Organisation | The Royal Society |
Sector | Charity/Non Profit |
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 | Charity/Non Profit |
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 | Charity/Non Profit |
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 Bangalore |
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 | Joint papers |
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 | Universidade de São 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 | Joint papers |
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 |