SSI: Continued Assurance from Requirements to Code

Download this article in PDF format.

The development of systems, whether high-assurance or mission-critical, faces a perennial problem: We can envision and therefore want to build systems that are much more capable and complex than we can assure with traditional approaches. The result is predictable: System errors resulting in system failures that result in losses—sometimes including loss of life.

Many system errors can be traced to erroneous behavior of critical system software. Software, even more than systems, is prone to escape from the envelope of manageable complexity. Software has no physical extent, no physical weight, and no physical power demand per se. The pressures that constrain the features we want to add to systems don’t constrain software. If we can imagine a feature, we can add the feature to software. The result is again predictable: Software that’s far too complex to assure; that fails; and that causes system failure.

Going Formal?

Software assurance has traditionally been gathered through extensive testing. Unfortunately, testing isn’t exhaustive and thus can only reveal the presence—not absence—of errors. But we can do better than just testing. At the system level, we apply analysis as well as testing. For example, when designing an aircraft, aerospace engineers conduct extensive aerodynamic analysis using computational fluid dynamics before going into the wind tunnel. The wind-tunnel tests validate the analytical model, upon which the fundamental assurance is based.

For software, we can apply formal methods. These are techniques based on mathematical representations of software behavior that allow for a truly exhaustive examination of software state to prove the absence of errors. Software testing then validates this comprehensive analysis.

Despite its power, the use of formal methods isn’t a silver bullet. In particular, software engineers must ask the right questions when conducting analysis. Asking the right questions is hard when critical system-level properties haven’t been explicitly traced to software. Software engineers often don’t know which properties need to be proved.

When focusing on SSI, systems engineers identify critical system-level properties and trace those properties through decomposition across system architecture and through translation from one artifact to the next. This attention to the evolution of system-level properties enables systems engineers to effectively communicate to software engineers the critical properties that they should prove. Focusing on SSI enables engineers to take full advantage of formal methods.

As model-based systems engineering has become more popular, tools supporting this approach have included increasingly powerful analyses. These tools go beyond simple checks for latency or space, weight, and power consumption, and they seek to demonstrate functional correctness of the architecture. Effectively, these tools apply formal methods at a higher level of abstraction. To take full advantage of these tools, systems engineers need clearly identified properties that they should prove. Focusing on SSI enables systems engineers to take full advantage of these analysis tools.

Talking to systems and software engineers in industry, we often hear that systems-engineering artifacts like requirements documents and design documents are “tossed over the wall” from one team to the next. This statement is somewhat astonishing. Surely all engineers involved in development—from systems engineers to software engineers—should be a single, integrated team.

Different people have different specialties, and software standards such as DO-178B/C require, at the highest Design Assurance Level, independence between those who develop a component and those who verify it. However, integrity is certain to be lost if there’s not constant and managed communication amongst team members. Focusing on SSI enables systems and software engineers to bridge the walls that separate them, by focusing communication on the critical properties along with the artifacts that serve as the interface between team members.

How Is SSI Supported?

SSI is a trait of high-assurance systems engineering—not a tool or technology. However, to facilitate SSI in systems engineering, tool support is essential. There are four integral parts to this tool support, plus an optional fifth: translation, traceability, analysis, argument, and (optionally) test-case generation.

Translation

Translation assists in preserving integrity by automating the representation of properties expressed in one artifact into the next. For example, in the SysML modeling language, a constraint associated with a requirement that’s written in OCL (the Object Constraint Language) and attached to an output port on an Internal Block Diagram might be translated into a synchronous observer in a Simulink model that’s written using Simulink blocks and attached to an output port of a subsystem. Similarly, the constraint might be translated to a postcondition in a programming language like SPARK that supports software contracts.

Translation bridges the gap separating the architecture (in SysML) from the design (the Simulink model) or the implementation (in SPARK). It also reduces the likelihood of error by not requiring that an engineer manually recode the property in the target language. Of course, this requires that we have confidence in the correctness of the translation, but techniques are available (such as tool qualification under DO-178B/C) that can offer this confidence.

Traceability

Traceability assists in preserving integrity by allowing engineers to follow the evolution of properties through system development. Continuing the example above, the Simulink synchronous observer would be traced to the OCL constraint so that if either was changed, engineers would be notified that the other must be reexamined or regenerated.

Analysis

Analysis assists in preserving integrity by allowing engineers to prove property satisfaction across decompositions. At each phase of system development, greater abstraction is replaced by greater precision, until the system has been fully and precisely described. Decomposition plays a critical role in this ever-increasing precision, as larger abstract components are broken into multiple, smaller components.

With analysis, engineers can prove that the smaller components, together, satisfy the intended functionality of the larger, abstract component. Continuing the example above, the Simulink subsystem would be broken up into smaller subsystems, each with its own contracts that, together, must satisfy the observer for the top-level subsystem.

Argument

Argument assists in preserving integrity by allowing engineers to record their rationale for property continuity when traceability or analysis are insufficient or unable to provide sufficient support. Continuing the example above, one of the subsystems may be COTS and might not have a sufficiently precise contract to enable proof that the observer for the top-level subsystem is satisfied. Engineers may know, however, that the way in which the COTS subsystem is used will, together with the other subsystems, always satisfy the observer for the top-level subsystem. The argument documents this rationale.

Test-Case Generation

Test-case generation assists in confirming integrity by demonstrating that critical properties are satisfied by the system. Continuing the example above, the observer for the subsystem could form the basis of a test case or set of test cases to be included in that phase of integration testing.