Reducing the gap between design and code for critical software with Ada 2012

The latest version of the Ada language standard, known as Ada 2012 [1], has extended the language’s support for minimizing the gap between design and code by raising the level of discourse, a principle that is fundamental to software development and that has been an underlying goal throughout Ada’s evolution.

The initial version of the language, Ada 83, provided modular programming with real-time message-based multi-tasking. Ada 95 added object-oriented features and data-oriented synchronization. Ada 2005 introduced interfaces for both normal and synchronized types.

In Ada 2012, contracts have been added in the form of pre- and postconditions, type invariants, and subtype predicates, along with finer-grained control for multicore programming. Ada has, in effect, integrated low-level requirements into the source code, and is the first ISO standard language to include contract-based programming,.

How to embed the design in the code
A key ongoing challenge for software developers is to reduce the gap between the high level requirements (design) of the system and the coded program, simplify development, and reduce the likelihood of error. Ada helps achieve this goal though a set of portable high level features that relate directly to concepts relevant at design time, while still providing lower level control where needed.

As an example, many critical embedded systems involve concurrent activities that need to interact safely through shared data or message passing while meeting hard or soft real-time requirements. In Ada, such activities map directly to multiple Ada tasks, with their interactions and real-time constraints representable directly in the code.

These facilities help make concurrent programming in Ada simpler and more reliable than in languages based on lower-level constructs. Another example is Ada’s support for object-oriented programming, where the interface feature allows multiple-inheritance class hierarchies to be directly represented.

Figure 1 illustrates how Ada reduces the gap between the design and the code, and between the code and the underlying hardware platform.

Figure 1: Reducing the gap

How to connect the model with the code
A new trend in a number of domains is the increasing usage of executable models, with products such as MathWorks’ Simulink, Esterel's SCADE, and various UML-based tools. The developer can use such tools to represent a portion of the system’s high-level logic in a form that can be directly executed by a simulation engine, and/or translate it automatically into compilable source code. Yet even with the best modeling systems, some portions of the system still need to be hand coded, either as modules that are plugged in to the modeling system, or as wholly separated components that are not amenable to executable modeling.

A major challenge is then how to test and verify the ultimate system, which combines the automatically generated code and the hand-written code, as represented in the compilable language. Translating from the modeling language to the compilable language may introduce synchronization, timing, or correctness issues, necessitating a full system test and certification on the compilable code even if the model has been shown to conform to the higher-level requirements.

When Ada is used as the compilable language generated from the model, Ada's strong interface checking helps detect potential inconsistencies. Moreover, its higher-level features such as tasks, protected objects, and interface types reduce the distance between the modeling language and the compilable language, making the transformation performed by the automatic code generator simpler to validate.

How to embed formal low-level requirements in the code
Anotherchallenge for high-level languages comes from the increasing acceptanceof formal methods in the certification of critical systems, asevidenced by the new DO-178C avionics safety standard [2] and the CommonCriteria security standard [3]. The support for formal methods requiresan appropriate language infrastructure as well as specific features.

Adais leading the way in meeting this challenge. The language’s strongtype checking and robust modularization facilities make Ada a strongcandidate for rigorous (mathematically based) analysis, and variousstatic analysis and proof tools are available for formally ensuring theabsence of run-time check failures [4][5].

Furthermore, Ada 2012is the first ISO-standardized language to include specific features forcontract-based programming: preconditions, postconditions, typeinvariants, and subtype predicates. A precondition is a logicalexpression that must be true when a subprogram is called, andanalogously a postcondition must be true when the subprogram returns.

Atype invariant is a postcondition that applies to every 'public'subprogram for a type, and a subtype predicate is a logical expressionthat characterizes a subset of values for a type. Contracts, which arein effect low-level requirements, may be verified dynamically, and theymay also be verified statically using appropriate tools.

The neteffect of these new Ada 2012 capabilities, together with the emergenceof new static analysis and proof tools, is that Ada programs can be anintegral part of the move toward formal methods and the accompanyingsignificant reduction in the time and expense associated withtraditional testing approaches.

Design-focused development in Ada 2012
TheAda language and its accompanying tools ecosystem provide a robust setof capabilities for the design-focused development of high-integritysoftware. The latest revision of the ISO standard for the language, Ada2012, has further strengthened these capabilities through the newcontract-based programming features.

Ada 2012 also helps addressthe increasing availability of multicore processors, providing controlover CPU affinity as well as supporting non-preemptive schedulingmodels. Finally, the Ada tools ecosystem is growing in its support ofadvanced static analysis, program proving, and combined static/dynamicanalysis approaches, thus reducing the time and expense of satisfyingthe demanding verification requirements for certification.

S. Tucker Taft is VP and Director ofLanguage Research at AdaCore, a company focused on open-source tools tosupport the development of high-integrity software.  Mr. Taft joinedAdaCore in 2011 as part of a mergerwith SofCheck, which he had founded in 2002 to develop advanced staticanalysis technology. Prior to that Mr. Taft was a Chief Scientistat Intermetrics, Inc. and its follow-ons for 22 years, where in1990-1995 he led the design of Ada 95.  He received an A.B. Summa Cum Laudedegree from Harvard University, where he has more recently taughtcompiler construction and programming language design.

References

  1. Ada 2012 Language Reference Manual
  2. RTCA /EUROCAE DO-178C/ED-12C – Software Considerations in Airborne Systems and Equipment Certification , December 2011.
  3. Common Criteria for Information Technology Security Evaluation , V3.1. Common Criteria Portal
  4. Project Hi-Lite: simplifying the use of formal methods
  5. John Barnes, SPARK: The Proven Approach to High Integrity Software, Altran UK, 2012.

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.