Programming from Control Laws
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 looses a bit of our work, the consequences are potentially much more serious when a computer program which, for instance, controls parts of an airplane goes wrong. To develop this sort of application, the UK government has produced guidelines which require the use of special techniques. Anybody can develop and sell a text editor, but programs whose failure can endanger lives need to be certified by the proper authorities. Engineers use a graphical notation called control law diagrams to specify control applications. Typically, they are implemented by specialised pieces of equipment in conjunction with programs. A lot of effort needs to be put into assuring that the programs are correct and, therefore, certifiable. The most widely used technique for certification is testing. This requires that the program is run several times, in an attempt to cover all its possible uses. QinetiQ is a British company; they are Europe's largest science and technology organisation. They have devised a much cheaper way of providing evidence of the correctness of control programs. They use mathematical notations and powerful computer tools to establish that the programs satisfy all the requirements specified in a control law diagram. In this project, we propose to further develop their ideas by applying well-established techniques of programming from specifications to this novel area. What we want is a technique for programming from control law diagrams. Our challenge is to provide a specialised technique, supported by tools, that allows programmers to ignore the mathematical theory involved. Control systems are key in the avionics, automotive, and power sectors, among others.The project will be part of an ongoing collaboration with QinetiQ through a Royal Society Industry Fellowship. This close contact with industry will guarantee that our results are relevant. Experience at QinetiQ shows a potential reduction factor of two and a half to four and half in the cost of certification.
People |
ORCID iD |
| Ana Cavalcanti (Principal Investigator) |
Publications
Mishra S
(2023)
'Cyclic syndrome' of arrears and efficiency of Indian judiciary.
in SN business & economics
Oliveira M
(2007)
A Denotational Semantics for Circus
in Electronic Notes in Theoretical Computer Science
Stefanini C
(2023)
A novel synthesis of two decades of microsatellite studies on European beech reveals decreasing genetic diversity from glacial refugia.
in Tree genetics & genomes
Sherif A
(2010)
A process algebraic framework for specification and validation of real-time systems
in Formal Aspects of Computing
Cavalcanti A
(2016)
A Suspension-Trace Semantics for CSP
Oliveira M
(2011)
A tactic language for refinement of state-rich concurrent specifications
in Science of Computer Programming
Oliveira M
(2009)
A UTP semantics for Circus
in Formal Aspects of Computing
Vernon M
(2010)
Abstract State Machines, Alloy, B and Z
Marriott C
(2012)
Abstract State Machines, Alloy, B, VDM, and Z
| Description | We have consolidated the semantics of Circus, covering challenging constructs, like angelic nondeterminism, which is central in refinement calculi. We have mechanised the semantics. Based on Circus, we have devised a complete refinement strategy to justify the correctness of implementations of control law diagrams specified in Simulink. This is based on a specific, but widely used program architecture. We have also considered Circus models and verification of implementations of Stateflow diagrams. These are an important category of control law diagrams blocks. Based on the mechanised semantics of Circus, we have also explored the mechanisation of the ProCLaws refinement strategies for verification of implementations. It is based on the mechanised generation of Circus models, their verification, and a refinement tactic language tailored for Circus. Finally, we have explored the use of Circus in supporting an alternative verification technique: testing. We have also explored the application of our technique to communication systems, like software-defined radios. |
| Exploitation Route | In the study of refinement of graphical notations. |
| Sectors | Aerospace, Defence and Marine |
| URL | http://www.cs.york.ac.uk/circus/research/control_law_diagrams.html |
| Description | Yes. The techniques have been applied by our industrial collaborator. |
| First Year Of Impact | 2010 |
| Sector | Aerospace, Defence and Marine |
| Impact Types | Economic |
| Description | International Joint Project |
| Amount | £12,000 (GBP) |
| Funding ID | YOR001 |
| Organisation | The Royal Society |
| Sector | Charity/Non Profit |
| Country | United Kingdom |
| Start | 11/2006 |
| End | 10/2008 |
| 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 | 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 | 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 | 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 | BCS FACS Evening Seminar |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Professional Practitioners |
| Results and Impact | The BCS Specialist Group for practitioners in Formal Aspects of Computing Science has members drawn from both industry and academia. It acts as a bridge between the two communities, helping British industry to stay in the forefront of formal computer techniques, and British academics to maintain the applicability of their research. It arranges informal seminars to encourage technology transfer throughout the year: about four a year. |
| Year(s) Of Engagement Activity | 2016 |
| URL | http://www.bcs.org/content/ConWebDoc/56123 |