Executive Summary
This case study is about the use and potential impact of the entire suite of D-RisQ automatic, formal methods tools on a case study set by Abrial in 1996 in the nuclear sector, for the control over a ‘steam boiler’. The original case study is considered an important reference point in regards to applying formal methods, in industrial and real world applications.
For the uninitiated, embedded software and control systems are like the brain and nerves of machines, helping them to perform specific tasks accurately and reliably. Our tools are designed to simplify the process of creating the 'brain', making it faster and more cost-effective for developers to build and certify their systems.
The case study demonstrates how our D-RisQ Toolsuite can make a significant difference to software development and verification. The case study demonstrates that our tools can speed up development time, reduce costs, and meet strict certification requirements — all without needing specialized knowledge of formal methods. This is a game-changer because it means more people can use these powerful techniques.
What's really exciting is that this is the first time in the world that formal methods — a rigorous approach to ensure that software is correct — have been integrated directly into easily accessible, automatic tools that address every stage of the software life cycle. This integration allows every stage of development, from initial requirements to the final product, to be more efficient and reliable: see the metrics we gathered below.
In essence, our tools democratize access to advanced development techniques, enabling a broader range of developers to create sophisticated control systems for sectors as varied as aerospace, rail, medical devices, autonomous systems, automotive, and even nuclear power. And with our case study showing clear benefits in terms of time-to-market and cost savings, we're excited to offer a solution that truly advances the field.
If you would like to know more, please contact us at info@drisq.com
The following hours expended per stage were gathered:
Labour Hours Used
In summary, from the System Requirements Allocated to Software (SRATS) defined at the outset, 37 requirements and assorted, declarations, were transformed and verified through software High Level Requirements, resulting in the software design and thereafter into 5577 lines of code in a total of 224.5 hours of labour. This is approximately 6 weeks effort by one software engineer and equates to roughly 930 lines of safety critical code produced per week. If you currently produce 100 lines of verified code per week, then the application of the D-RisQ Toolsuite results in roughly 9x your own productivity and provides the certification evidence required by regulators.
Note that this is a study and not a real ‘steam boiler’
Can formal methods be used by a typical software developer to speed up the development of control systems while also meeting certification needs?
For Aerospace embedded software, compliance to DO-178C/DO-333 must be verified and evidenced in order for the software to be so certified. Where such certification credit claims are able to be made, a quick reference table based upon the Annex A tables for DO-333 is provided as to how each Objective could be met through the use of the various tools. The key to colour is as follows:
Like many applications across diverse fields — including aerospace, rail, medical, autonomous systems, automotive, and nuclear — this exemplar can be effectively tackled with the D-RisQ Toolsuite by our tool users.
As a result of automation, there is no need for specialist knowledge of formal methods languages, techniques or interpretation which democratises access to the power of formal methods. It covers every development stage from system requirements, through software requirements, design, source code and the binary. We showed how the aerospace software standard,
DO-178C can be used in this context.
We also gathered a set of metrics that showed how much effort was expended per development/verification stage. The answer to the question is therefore an emphatic ‘Yes’, and here are some high-level details.
System Requirements, Validation and Verification - System Kapture
The Abrial specification is used as the basis for the development of a set of System Requirements Allocated to Software (SRATS). We used System Kapture, which exploits structured English in easy to use templates. The use of a tool to write clear, concise, unambiguous SRATS enables an exploration of desired properties and crucially, to show absence of undesired behaviour. There is a ‘requirements standard’ adhered to as a by-product of the use of this technology, which means that a user focuses on the important aspects of requirements. This provides a robust base upon which to develop the software, with the bulk of the effort dedicated to evolving the SRATS.
Certification Credit
For DO-178C/DO-333, there are no objectives to be met. However, without a good set of SRATS it is very difficult to develop good software. System Kapture assists in the development of a sound basis from which to develop ‘certifiable’ software.
Software Requirements and Verification – Kapture®
The next step is to develop a software specification in Software High Level Requirements, again using a structured English approach in Kapture®. This is a tool that has formal semantics in the background and complies with a requirements standard encapsulated within the tool. We showed that we can prove that these software requirements implement the SRATS.
Certification Credit
If Kapture is used in conjunction with System Kapture, then the table below gives a guide to the DO-333 Objectives that may be met and the extent to which they are automated by the use of the tools.
Extract from DO-333 Annex A Table FM.A-3 (including use of System Kapture)
Design and Verification - Modelworks®
A design has been undertaken in a subset of Simulink®/Stateflow® and compliance with a standard is checked. Then an automatic independent proof is undertaken using Modelworks® to show that the graphical design correctly implements the requirements, or to show where it does not.
Certification Credit
The table below gives a guide to the DO-333 Objectives that may be met and the extent to which they are automated by the use of Modelworks.
Extract from DO-333 Annex A Table FM.A-4
Source Code and Verification – CLawZ®
By using an autocoder, the production of source code is a matter of a few seconds and is automatically checked for compliance to a coding standard. It is then automatically and independently verified using the formal proof in CLawZ® to show that the code correctly implements the design or to highlight issues.
Certification Credit
The table below gives a guide to the DO-333 Objectives that may be met and the extent to which they are automated by the use of CLawZ®.
Extract from DO-333 Annex A Table FM.A-5
Executable and Verification – FEVER®
The final part of the development discussed is the verification of the Executable Object Code (EOC), again through the use of formal proof embedded in our forthcoming FEVER® tool. By bringing all the tools together, we also show how to achieve an equivalent to ‘coverage’ of both requirements and code structure, thus significantly reducing effort.
Tool Qualification
The certification claims are based upon use of DO-333, the Formal Methods Supplement to DO-178C. This also includes tool qualification that users would have to undertake to DO-330, the Tool Qualification guidance for Aerospace. Certification and tool qualification is discussed in each of the relevant stages.
Although every tool has its limitations and, some are still in development, our Toolsuite tackles numerous software development challenges. It empowers developers to quickly create verified software functionality, boosting productivity, accelerating time-to-market, and cutting costs.
Certification Credit
The tables below give a guide to the DO-333 Objectives that may be met and the extent to which they are automated by the future use of FEVER®.
DO-333, section FM.6.7.f gives options for the verification activities of EOC. In our case we have used formal models for the HLR, design, source code and of the EOC. It is in this context that claims for certification credit may be made meeting; see the diagram below which shows the transitivity of proof.
We are therefore effectively undertaking a ‘complementary analysis’ which shows that the translation of the source to EOC is correct; that is, the desired properties of the source code are preserved. The tables below give a guide to the DO-333 Objectives that may be met and the extent to which they are automated by the use of FEVER®:
Extract from DO-333 Annex A Table FM.A-6
Noting the transitivity of proof, the table below is a summary of the Objectives expected to be met by the full use of the Toolsuite:
Extract from DO-333 Annex A Table FM.A-7
For further information get in touch with us today via email or telephone.
