Software based systems within aerospace are becoming increasingly complex. The typical approach to the development of software based systems has a cost profile heavily weighted towards the end of the project; this represents considerable project risk. For systems and software in the aerospace domain, the recently released ARP4754A and DO-178C are the key documents to support platform certification under CS-23/25. While these documents specifically relate to the civil domain, they are increasingly used to assist in the development of military systems as a baseline for their own certification processes. Gaining the required evidence from development life cycle processes that support platform certification, needs to be designed into all stages of the life cycle. The production of evidence should therefore drive the selection of the best development life cycle, processes and tools. The production of verification evidence through review, analysis or test to meet DO-178C objectives can therefore be costly and unresponsive, even to small changes.
The use of formal methods in aerospace has been adopted in some small measure and has typically employed experts to write formal specifications by hand and then to prove the necessary properties using appropriate qualified tools as support. The claims for certification credit have been made as an ‘alternate method’ under DO-178B and how this has been achieved has become company specific knowledge, not available to the wider community. With the advent of DO-333, the Formal Methods Supplement to DO-178C, it is possible for others to define how Objectives can be met.
D-RisQ has taken an approach which enables the power of formal methods to be exploited without any specialist training. By using commonly available tools such as Simulink® and commercial auto coders it is now possible for current engineers to develop systems and software in a rigorous manner, whilst gaining as a by-product, the required evidence to support certification. The D-RisQ suite of tools include Modelworks® and CLawZ® which tackle different aspects of verification and meet Tool Qualification Level 4 under DO-330. Our tools provide verification evidence that meets Objectives from DO-333 Annex A in tables A-3 to A-7.
Modelworks® proves that requirements have been correctly captured in a design expressed in Stateflow®, or will show the manner in which compliance has failed. The design can be of a System of Systems, a single system or a software program. It allows a designer to check that the design does what is required. More importantly, it allows a proof that undesired properties will never happen, a check that is typically attempted at the end of a development life-cycle. It is also possible to show behaviour under failure conditions. Modelworks can be used to show the behaviour of distributed Systems-of Systems such as multiple platforms and Integrated Modular Avionics, as well as how architectures of more conventional systems behave.
CLawZ® automatically proves that automatically produced code implements a design expressed in Simulink®. By using the ADI Ada auto-coder or the TargetLink® C auto-coder aligned to the Simulink control system subset, CLawZ produces evidence that the code correctly implements the design, or shows where the coder has made a mistake. This relieves the need to undertake unit testing thus gaining considerable time benefits.