The DO-178B guidelines, adopted in 1992, have served the aviation industry well for more than 15 years. Adherence to these guidelines in millions of lines of safety-critical code has allowed the aviation industry to deploy increasingly sophisticated software capabilities in hundreds of new avionics applications. These applications exhibit extremely low software failure rates, and deployed systems generally operate safely.
The highly anticipated DO-178C guidelines are designed as a response to a growing concern that the existing DO-178B standard ignores more modern software development technologies and imposes restrictions that add significantly to the costs of software development without necessarily increasing software safety. Part of the motivation for the new DO-178C guidelines is a desire throughout the industry to enable more modern software engineering practices, offering the potential for decreasing development costs and increasing software generality. Among the topics specifically addressed in draft supplements to DO-178C is the use of formal methods. Formal methods characterize the use of various mathematical techniques in the specification, development, and verification of software and hardware systems.
Concurrent with development of DO-178C guidelines, a parallel effort has focused on creation of the JSR-302 standard for safety-critical development with the Java language. Similar to the motivations for DO-178C, the goals associated with the safety-critical Java standardization effort are to enable more modern software engineering practices that will reduce development costs and improve software flexibility and generality. Both standardization efforts have been ongoing for several years, and both standards are due for public release in 2010. Kelvin examines the potential synergies between the two standards, focusing on their encouragement of formal methods in support of high-integrity, object-oriented development.
Choosing the right tool for the job
Today, most safety-critical software systems are developed in either C or Ada. Developers who choose C typically cite benefits such as improved availability of development tools and platform support, along with ease of recruiting engineers and new software engineering graduates. Today’s developers who choose Ada for a new development effort typically explain that the language offers superior abstraction and type safety than C. Both groups have had valid reasons for their respective choices, but much of the rationale of the choice between Ada and C is founded on rationales that aren’t necessarily relevant in today’s software engineering environment, including:
- Type safety versus abstraction – While the strong type system benefits of Ada represent a significant benefit in comparison with C or C++, the Ada programming language’s retrofitted approaches to object orientation lack the strong portability, encapsulation, modularity, and scalability benefits that have been demonstrated in more recent languages like Java.
- Problem size versus modular composition – Today’s safety-critical software systems are much larger and more complex than the typical systems constructed 10 or even 15 years ago and thus often require more sophisticated modular development methodologies than were appropriate previously.
DO-178C and safety-critical Java: New tools for a new problem domain
Whereas the typical safety-critical system of 10 years ago was comprised largely of handcrafted application code developed specifically for a particular project, today’s safety-critical systems often consist of an integration of many independently developed components. Airframes, for example, are often repurposed between civilian and military applications. Additionally, military systems are often deployed in different configurations depending upon the nation to which they are sold. And with some airframes experiencing 50-year service lifetimes, the electronics and software undergoes many upgrades over the system’s service history.
Among the goals associated with more modern object-oriented software development approaches are to reduce the costs of porting, integrating, and evolving independently developed software capabilities. The mainstream Java language has demonstrated solutions to these challenges, which is part of the reason for its widespread adoption in mainstream data-processing applications. The recent DO-178C and safety-critical Java specification efforts both endeavor to deliver these benefits to developers of safety-critical systems. Object-oriented programming is largely about enabling modular composition of independently developed components. The use of formal methods in combination with object-oriented development is part of what enables safety-critical real-time code and certification evidence to be created through modular composition.
The guidelines of the draft DO-178C recommendations are entirely consistent with the existing DO-178B recommendations. A major contribution of DO-178C is the inclusion of several technology-specific supplements, which clarify the certification expectations for various software development approaches only discussed superficially (if at all) in DO-178B. Figure 1 lists the various supplements that will accompany publication of DO-178C.
Object-oriented process via formal methods maintains separation of real-time concerns
A crucial consideration with safety-critical software systems certification is that the safety of individual software components depends on how each component interacts with other components within its execution environment. Time-critical functionality might be pushed off schedule if other components’ priorities are set incorrectly, or if other components consume more CPU time than was anticipated in the safety analysis. Likewise, functionality that requires temporary access to memory, network bandwidth, or shared database records will be compromised if other components fail to release exclusive access to these shared resources with sufficient frequency. The most difficult aspects of building safety-critical software components from object-oriented integration of independently developed components include understanding and validating that all potential interference between software components is properly resolved.
While thorough testing is an essential ingredient in the certification of a safety-critical system under both DO-187B and the anticipated DO-178C standards, it is usually not possible to synthesize all of the tests required to exercise all possible worst-case interactions between software components. This is one of the reasons why DO-178C introduces an increased emphasis on formal methods, and why the emerging safety-critical Java standard is designed to enable the application of formal methods.
Though the draft standard for safety-critical Java does not specify the formal method approaches that are to be supported by vendors of compliant safety-critical Java implementations, the standard is designed to enable various formal method approaches. Some of these approaches are demonstrated in Atego Systems, Inc.’s PERC Pico, a Java development environment geared toward the creation of resource-constrained and deeply embedded hard real-time applications. PERC Pico is based on preliminary drafts of the safety-critical Java standard.
Among specific concessions designed into the draft safety-critical Java specification to enable the use of formal methods are the following:
- Rather than support the entirety of Java Standard Edition libraries or Real-Time Specification for Java extensions, the safety-critical Java standard is structured as a small subset of both. For each supported library capability, the specification clarifies whether the method allocates memory and whether it performs operations that might temporarily suspend the thread’s execution.
- Applications are structured as missions, with each mission comprising multiple independent execution threads. Each thread within the mission may only access its own private memory or the shared memory of an enclosing mission. The restrictive programming API is combined with strong type checking to enforce this separation of concerns. The safety-critical Java mission life cycle is illustrated in Figure 2.
- All temporary memory needs of individual software components are satisfied from stack memory. The working memory for individual threads is structured as a hierarchical decomposition of a single primordial stack. The initialization thread’s stack is divided into multiple smaller stacks for threads spawned from the initialization thread. Each spawned thread may in turn divide its stack into even smaller stacks for threads spawned from within that spawned thread.
- Formal methods designed to complement the safety-critical Java standard enable proof that software components do not create dangling pointers to reclaimed stack memory segments, facilitate reliable composition of independently developed software components, and make it possible to automate the analysis of each thread’s stack memory and CPU time resource consumption.
New standards enable cost savings and increased software generality
The potential benefits offered by the emerging DO-178C standard for safety certification of airborne systems and the JSR-302 standard for safety-critical Java development include greater reuse and repurposing of existing software through the use of formal methods in support of high-integrity, object-oriented development. This reduces the integration effort when building large software systems by modular composition of independently developed components. Ultimately, this has the effect of improving developer productivity, reducing development costs, and increasing the generality of safety-critical software systems.
Atego Systems, Inc. 858-457-2700 www.atego.com