Engineers use control law diagrams in industry every day. Techniques and tools for analysis of these diagrams or their models are plentiful; verification of code created to implement them, however, is a challenge that has been taken up by few. A lot of approaches rely on verification of (models of) the diagrams, and on the correctness of code generated automatically. This is not appropriate assurance of code safety if the code generator has not been verified. Frequent updates, however, make such verification costly, and also hardware requirements often mean that specific algorithms are needed, so that code generated automatically is not adequate.
What we propose is to develop the foundations of a sound and practical technique to prove correctness of implementations of control diagrams. In the approach that we will investigate, the formalisms that justify soundness are hidden from engineers, and high levels of automation ensure practicality. Scientific challenges are imposed by comprehensive diagrammatic notations, large data sets, and dynamic scheduling. We propose to provide (1) a semantics for
discrete-time control diagrams to capture both their functionality and inherent concurrency; (2) a verification technique based on refinement; (3) strategies and laws tailored for the diagrams models and implementations; and (4) automated support for the application of the technique.
We collaborate with the Systems Assurance Group at QinetiQ, Malvern, in the context of a Royal Society Industry Fellowship. We interact with their engineers and, with them, tackle issues raised by industrial-scale systems. Their experience is with Z and CSP, supported by successful tools; their verification technique is mostly automatic and affords drastic cost reductions. This project addresses
difficulties arising from the separate treatment of functionality and concurrency.
Our approach is based on Circus, a notation that combines Z and CSP; initial results from our collaboration with QinetiQ were published in the top conference in the area. Our more recent results also show that the Circus refinement theory can be a sound basis for reasoning techniques.
This line of work is a novel application of refinement techniques of programming: implementation of control diagrams. The results will widen our knowledge of reactive systems in general, and of control systems in particular. A large number of laws of programming for data-rich and for concurrent programs have been published. Our work will reveal a wealth of novel laws that capture properties arising from the interaction of these features.
We also expect to make a contribution to the digital embedded systems industry in general, where the diagrammatic notation that we study, Simulink, is a de facto} standard. In the experience of QinetiQ, Praxis High Integrity Systems, General Dynamics, Jaguar, and Ford, to cite some examples, Z and CSP are valuable used in isolation. We perceive technical and practical benefits in their integration. QinetiQ have contributed generously to the production of Circus; they expect to start using it in about four years. They will be in a strong position to carry out the technological developments needed to exploit the research proposed here. By funding this research, the EPSRC will guarantee that its results will be publicly available to academia and industry in general (as well as to QinetiQ).
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.
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
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.
|Effective start/end date||1/07/07 → 30/09/11|