The software development challenge

Esterel Technologies' safety manager, Jean-Louis Camus, analyses how the soon to be finalised DO-178C update may leverage benefits of model-based development with qualified tools. Embedded software is truly pervasive; technology facilitated through embedded software is routinely injected into our everyday lives to create functionality on which we grow to depend.
 
Whilst the embedded avionics software domain shares the dynamics of increasing complexity and decreasing development schedules with the wider embedded software discipline, we as consumers can thankfully rely on a rigorous design and certification processes as defined in the DO-178B standard to minimise the occurrence of potentially catastrophic software bugs.

As software complexity increases, there is a reasonably linear increase in development time; however the real sting is in the tail. Verification costs of the highest integrity applications now exceed the development costs for that software if traditional development methods are used. Qualified development tools provide a solution to this problem by front loading the development process and minimising costly low level testing activities.

ED-12/DO-178B provides guidelines for the production of software for airborne systems and equipment. The objective of the guideline is to assure that software performs its intended function with a level of confidence in safety that complies with airworthiness requirements. These guidelines specify objectives for software life cycle processes, description of activities and design considerations for achieving those objectives, and description of the evidence that indicates that the objectives have been satisfied.

Levels of assurance

DO-178B defines five ‘development assurance levels': A - catastrophic failure condition for the aircraft; B - hazardous/severe failure condition for the aircraft; C - major failure condition for the aircraft; D - minor failure condition for the aircraft; E - no effect on aircraft operation or pilot workload.

Airborne software of levels A, B or C is designated safety critical and as a consequence verification processes are of the highest importance. Verification encompasses reviews, analyses and testing. Every piece of life cycle data needs to be reviewed, in most cases with independence. Very thorough testing has to be performed. Low level test cases have to be written against the low level requirements and integration test cases have to be developed against the high level requirements. Then structural code coverage needs to be analysed and resolved using demanding coverage criteria, such as Modified Condition/Decision (MC/DC) for level A.

Verification may account for up to 80% of the total costs of a DO-178B level A software development project. The effective productivity of such a project, when including these costs is less than 10 lines of code per person per day.

Formal Model-based Development and Verification (FMBDV) is the first step to efficient software development and verification. Its principle is to represent the requirements in the form of a model, which is a readable, structured description of the software functions and/or architecture. Models are often edited in a graphical form, making them easy to understand by a large number of people.

As an example, Esterel Technologies offers SCADE, an integrated workbench based on a formal graphical language, featuring automated design documentation generation, automated formal verification and simulation. The SCADE product family addresses critical embedded control applications and critical embedded graphics display applications in SCADE Suite and SCADE Display respectively. A key differentiator of SCADE versus other informal and semi-formal modelling tools is its automated code generator, which is qualified as a level A development tool.

Qualification of a tool can leverage the benefits of FMBD. Primarily, this saves verification of its output. When a failure in this type of tool cannot introduce an error in the final software (for instance a checker), but just misses an error, then it is categorised as a ‘verification tool'. Accordingly, when a failure in the tool can introduce an error in the final software (for instance a code generator) then it is categorised as a ‘development tool'.

Qualification of a code generator that has appropriate requirements (such as traceability, coding standards, etc) not only saves review of the generated code; it allows saving of most of the low level testing and structural code coverage effort.

Formal model-based development with a qualified code generator has been used effectively for 20 years for a number of complex safety critical software applications. These include the Flight Control System of the Airbus A380, most Eurocopter autopilots and the FADEC of many Pratt & Whitney engines. Experience has shown that the total software development and verification cost has been divided by a factor of two, compared to traditional approaches. Additionally, formal model-based development with qualified code generation dramatically decreased the time and effort needed to take into account requirement changes, which are frequent for complex systems.

The trends of DO-178C

DO-178C is being defined by a group of experts from certification authorities, aircraft and equipment manufacturers, tool providers, consulting companies, and academics. It is planned to be released by end of 2010 and will be composed of the following documents:

• The core document, which is near to DO-178B and applies to traditional development
• The Tool Qualification supplement, which defines guidelines for the qualification of tools that are much more complete and accurate than those provided by DO-178B
• The Model-Based Development and Verification supplement which defines guidelines for the use of model-based development and verification. Whilst DO-178B did not prohibit such approaches, it did not provide an explicit rule for such methods
• The Formal Methods supplement which defines guidelines for the use of model-based development approaches. Whilst DO-178B did not prohibit such approaches, it granted no certification credit and did not provide an explicit rule
• Object Oriented Development. Whilst DO-178B did not prohibit such approaches, it did not provide an explicit rule for such methods
• Air Traffic Management

In summary, DO-178C now acknowledges rigorous and efficient techniques (tool qualification, FMBD, formal methods and object orientation) as first class methods, allowing applicants to take full benefit of the power of these methods and their related techniques, such as automated code generation from formal models.

This article has summarised the challenges that a company faces when developing DO-178B software in today's economic context and shows how a first level of improvement can be achieved with formal model-based development. Above all, it demonstrates how a significant additional competitive advantage can be gained from the use of qualified tools.

www.esterel-technologies.com