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.

Publications

10 25 50
publication icon
Alberto A (2017) Formal mutation testing for Circus in Information and Software Technology

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

publication icon
Cavalcanti A (2010) Unifying Theories of Programming

publication icon
Cavalcanti A (2013) Test-data generation for control coverage by proof in Formal Aspects of Computing

publication icon
Cavalcanti A (2010) Unifying Theories of Programming

publication icon
Cavalcanti A (2011) Testing for refinement in Circus in Acta Informatica

 
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