Mathworks says models work for the military
Mark Walker discusses the evolution of the DO-178 standard alongside the emergence of model-based design and formal methods tools.
A modern commercial aircraft relies on many millions of lines of embedded source code to fly. Fundamental systems, such as those used for guidance, navigation and control depend on software to function.
Software used in this way can be described as “high integrity”. In developing the software, rigorous design, inspection and test procedures must be used and these procedures are called the development process for high integrity software.
To provide guidance when developing high-integrity software for aerospace systems, the FAA and RCTA developed the DO-178 standard to define the objectives that the high-integrity software development process must meet.
When DO-178 was introduced almost 30 years ago, the avionics industry was undergoing a major shift from analogue to digital systems. Today, the standard required by the FAA and EASA is DO-178B (Software Considerations in Airborne Systems and Equipment Certification).
DO-178B provides guidelines for the production of aerospace systems. It specifies 66 software development process objectives across various stages in the development lifecycle.
When the B revision of the standard was developed in 1992, the normal development approach was to create specification and design documents and then write code from the design by hand. The documents and source code would undergo review followed by testing of the source and object code.
Over the last 20 years, tool advances have enabled engineers to approach the task of software development with greater efficiency. Instead of developing written specifications, it is now common to specify the software behaviour in an executable form, i.e. a model. Just as with a document, this model can be reviewed. Importantly, it can also be analysed and simulated.
This helps engineers determine if their design is correct before committing effort to implementation, review and test in software.
Additionally the software source code can be directly generated from the model, as opposed to hand-writing the code.
Finally, the model can support testing and review by acting as a definition for expected software function. This overall approach, model-based design, emerged after the publication of DO-178B.
The DO-178 committee has responded to this and other advances by updating the standard and in January 2012, DO-178C and new accompanying supplements were published. These create a framework that reflects the capabilities of modern software tools.
DO-178 requires an applicant to demonstrate that appropriate stages of design development, inspection and verification have been met. A project defines the process up-front, in a planning document called a PSAC (Plan for the Software Aspects of Certification) and this plan will be agreed with the authorities in advance.
Figure 1 shows a typical process for a project using model-based design. Each of the boxes in the diagram represents a stage in the development process. Stages might be completed in succession or worked on simultaneously, but once complete, they must be signed off in sequence since a downstream stage depends on definitions from the previous one.
The solid arrows between process boxes represent the design work, such as modelling or coding. The dotted arrows on the diagram represent the processes used to show that a stage has been developed correctly, in other words the verification activities.
Fig 1. DO-178 workflow
Projects using model-based design can also benefit by maximising automation in the verification process. It is possible to automate many of these verification stages. Wherever a tool replaces a manual verification process, such as an inspection, DO-178 requires the project to assess the impact of the tool use in the software life cycle and then qualify the tool at an appropriate level.
Increasingly tool vendors offer qualification kits to assist and the DO-330 supplement provides guidance on how projects should carry out qualification.
The introduction of the Formal Methods Supplement (DO-333) represents a significant evolution between the B and C revisions of DO-178.
Formal methods complement the established verification techniques of review, functional testing and traceability. They can be applied from the highest levels of requirement definition right through to the most specific aspects of implementation, such as low level software.
Property proving against requirements models is perhaps best illustrated by an example. Consider the reverse thrust capability of a jet engine.
It is used when landing to rapidly slow down the aircraft before the runway ends. For the system to be safe, however, the software must not allow the thrust reverser to engage in the air.
If you want to make sure something can’t happen, testing every possible input combination is one way to do it.
However, as noted in DO-178, the number of test cases you need to cover will grow unreasonably large very quickly for all but the simplest of routines. By contrast, formal methods tools can apply solvers to more efficiently examine all possible inputs.
Where an input combination exists that violates the property you have specified, in this case thrust reversal in flight, a test case will be generated showing how it can happen. Where no test case exists, the tool will tell you the property has proven valid.
Software used in high-integrity aerospace environments has always had to go through a rigorous development process.
DO-178C clarifies how modern techniques, such as model-based design and formal methods, can be applied in this process. These techniques allow projects to develop complex software systems efficiently and still maintain high levels of integrity.
Mark Walker is a senior en gineer at MathWorks