DO-332, the Liskov Substitution Principle, and local type consistency ramp up DO-178 certification

Story

March 12, 2013

Benjamin Brosgol

AdaCore

DO-332, the DO-178C standard's supplement on Object-Oriented Technology (OOT) and related techniques, analyzes the issues raised by object orientation in safety-critical software and supplies new guidance to deal with OOT's vulnerabilities. An important new objective of DO-332 is "Local Type Consistency Verification," which exploits a type theory result known as "the Liskov Substitution Principle" and helps address some of the key certification challenges raised by OOT's dynamic flexibility.

Object-Oriented Technology (OOT) is widely used and is supported by a range of programming languages including C++, Java, and Ada, but for various reasons its popularity has not spread to airborne and other safety-critical software. The underlying problem is the complexity of verifying software that makes use of three of OOT’s basic elements: inheritance, polymorphism, and dynamic binding. (Figure 1 explains the object orientation basics.) A simple example illustrates the issues:

Figure 1: Object orientation basics

(Click graphic to zoom by 1.8x)

Suppose that the Sensor class is the root of an inheritance hierarchy, ref is a polymorphic reference to an object from any class in this hierarchy, and Reset is an operation defined differently for different Sensor classes. The statement ref.Reset(…) dynamically binds to the appropriate version, based on the class of the object denoted by ref. How does one verify that this invocation meets the requirements for the Reset operation?

One problem arises if inheritance is used to define a subclass that is not a specialization of Sensor. This subclass’s Reset may have some effect unrelated to resetting a Sensor, or it may generate an exception. It would be an error for ref to reference an object from such a subclass, and analysis would be needed to show that the error could not occur. This complicates the verification process.

Another issue concerns structural coverage analysis. For systems at any of the three highest levels (A, B, or C) of the DO-178 standards, complete statement coverage must be demonstrated using requirements-based tests. But there are several implementation strategies that a compiler might choose for handling dynamic binding, with different implications on what “statement coverage” means. The scope of the structural coverage should not depend on the implementation strategy that the compiler uses.

DO-332[1], the OOT supplement to DO-178C[2], has addressed these issues through the new concept of local type consistency, which exploits the principle that inheritance should only be used for class specialization.

Inheritance and the Liskov Substitution Principle

In an object-oriented design, the system’s architecture reflects the classes and their relationships. A particularly important relationship is specialization (“is a”), but there are many others. Implementing the design involves choosing language mechanisms for capturing the relationships.

In an object-oriented language, inheritance may be used to implement a variety of relationships between two classes. However, anomalies can arise when inheritance is used for anything besides specialization since operations defined for the superclass might not make sense for the subclass. Restricting inheritance to specialization relationships has been studied in the context of type theory, where it is known as the Liskov Substitution Principle (LSP)[3]. Informally, LSP means that wherever an instance of a superclass can be used, substituting an instance of any subclass should be permissible.

Using inheritance for specialization has an important interaction with an operation’s preconditions and postconditions (its “contract”). A precondition is an assumption that the operation is making with respect to the program state when the operation is invoked. A postcondition is a guarantee that the operation is making on the program state when the operation is completed. Pre- and postconditions may be specified explicitly – either in the source text, as in Ada 2012[4] or SPARK[5], or separately – or they may be implicit in the logic of the operation.

If inheritance is to comply with LSP, a subclass’s version of an operation should not impose a stronger (more restrictive) precondition than the superclass’s version. Otherwise an invocation might succeed in some cases (on a superclass instance) but fail in others (on a subclass instance). Analogously, a subclass’s version of an operation should not specify a weaker (more general) postcondition than the superclass’s version.

Complying with LSP thus means satisfying two properties:

Contract consistency: No subclass operation strengthens a precondition or weakens a postcondition of the superclass operation that it is overriding.
Behavioral consistency: Each subclass operation meets its superclasses’ requirements.

DO-332 captures these concepts in a new objective, Local Type Consistency Verification. This objective does not require demonstrating that the class hierarchy complies with LSP, which would be overly restrictive. Instead, it reflects that the verification effort is simpler for class architectures that do comply, and that the analysis only needs to consider local context.

Local type consistency

Figure 2 shows the activity associated with verifying local type consistency, which DO-332 requires for software at levels A, B, or C. The wording “for each subtype where substitution is used” refers to contexts where dynamic binding occurs, such as ref.Reset(…), and the “subtype” in question is the class of an object that ref could reference at that point. The potential classes will not necessarily be the full hierarchy, and different sets of classes may be applicable at different invocations of the same operation.

Figure 2: The activity associated with verifying local type consistency, which DO-332 requires for software at levels A, B, or C

(Click graphic to zoom by 1.9x)

Consider a particular occurrence of ref.Reset(…), and let HeatSensor be one of the possible subclasses for the objects that ref could reference there. Local type consistency of ref.Reset(…) for HeatSensor may be demonstrated either “optimistically” or “pessimistically.” The optimistic approach works if HeatSensor satisfies LSP, and may be carried out in two ways:

Through formal methods, by demonstrating that HeatSensor’s version of Reset meets the requirements for Sensor’s version and does not strengthen the preconditions or weaken the postconditions of Sensor’s Reset.
Through testing, by running the requirements-based tests for Sensor’s version of Reset, using an instance of HeatSensor.

Formal methods may be facilitated by appropriate support from the programming language and its toolset, for example, Ada 2012 or SPARK.

The optimistic approach will demonstrate contract and behavioral consistency between the superclass’s and subclass’s versions of the operation. Additional verification is obtained through requirements-based tests for the subclass and possibly also through formal methods.

If the classes do not comply with LSP, or if there are few dynamically bound calls or the hierarchy is shallow and/or narrow, then it may be simplest just to test each possible case that can arise. This is the pessimistic testing specified in the third bullet item in Figure 2. Requirements-based tests are needed to exercise the operation for each subclass that could arise.

DO-332, local type consistency, and LSP guide certification

Local type consistency verification is just one aspect of using OOT safely; DO-332 contains guidance on other OOT elements as well as related techniques such as generic templates. DO-332 is “language agnostic”; more specifics are available on how to apply OOT in safety-critical or high-security systems, using Ada 2012 as the programming language[6].

DO-332’s local type consistency guidance is consistent with DO-178C’s general approach to verification, ensuring that all tests are based on requirements. It adapts the verification activities in a novel way to reflect the semantics of object orientation and the class structure’s degree of compliance with LSP. The new guidance should help to promote the safe use of Object-Oriented Programming (OOP) in avionics and other critical domains.

References

[1] RTCA/EUROCAE DO-178C/ED-12C. Software Considerations in Airborne Systems and Equipment Certification, December 2011.

[2] RTCA/EUROCAE DO-332/ED-217. Object-Oriented Technology and Related Techniques Supplement to DO-178C and DO-278A, December 2011.

[3] B. Liskov and J. Wing. “A behavioral notion of subtyping,” ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 16, Issue 6 (November 1994), pg. 1811-1841.

[4] Ada 2012 Language Reference Manual (December 2012), www.ada-auth.org/standards/ada12.html

[5] J. Barnes with Altran Praxis. SPARK – The Proven Approach to High Integrity Software. Altran Praxis, 2012.

[6] AdaCore, High-Integrity Object-Oriented Programming in Ada, July 2011. extranet.eu.adacore.com/articles/HighIntegrityAda.pdf

Dr. Benjamin M. Brosgol is a senior member of the technical staff at AdaCore. He has more than 30 years of experience in the software industry, concentrating on languages and technologies for high-integrity systems. He has presented papers and tutorials on safety and security certification at numerous conferences and has published articles on this subject in a variety of technical journals. He holds a Ph.D. in Applied Mathematics from Harvard University. He can be contacted at [email protected].

AdaCore 212-620-7300 • www.adacore.com www.linkedin.com/company/adacore www.twitter.com/AdaCoreCompany