| |
Formal checker verifies software
|
Werner Damm and Moshe Cohen
EE Times
(06/15/2001 3:39 PM EDT)
 |
 |
 |
 eople may seem willing to put up with PC applications that crash regularly. But the same cannot be said for embedded software applications such as planes, trains and automobiles, where significantly higher performance and safety standards are demanded. To support the creation of high-availability systems within increasingly tight development schedules, there is a growing need for advanced software validation techniques such as formal model checking.
Often, embedded software is still coded by hand in response to textual descriptions of the desired product attributes. Product behavior is invariably validated at a very late stage in the design process, resulting in expensive post-implementation surprises; serious quality, performance and safety obstacles; and delays in release schedules. Consequently, software testing can account for 30 percent to 60 percent of development time.
With the increasing complexity of computer-controlled devices, combined with tightening development deadlines, programmers are having to change the way they work. Concept-to-code solutions are increasingly being used to integrate the analysis, design, implementation and testing of embedded systems. They are designed to improve productivity by enabling programmers to build applications in an iterative manner with an associative approach that links every facet of the design process, ensuring that product behavior is completely validated up front, before anything is built.
Model-based design
Model-based design processes, which are used to build executable models of systems and components early on in the development cycle, are a significant advance in the embedded industry. They blend both functional decomposition and object methods in a visual programming environment. The identification of the right decomposition, into either functions or objects, depends on the thorough analysis of systems prior to code generation. This requires textual descriptions of typical end-user behavior or, increasingly, Unified Modeling Language (UML) sequence diagram notations.
Embedded designs can be optimized using such models in a variety of ways. The interaction of the environment and the system are graphically captured. For real-time applications, end-to-end latencies are also documented using real-time annotations in sequence diagrams. Then the overall system architecture is derived in an iterative process that explores a number of design alternatives.
State charts have become the standard visual method for capturing the behavior of reactive system components with both the functional decomposition style of system modeling. These solutions bridge the gap between design-level and code-level testing. They enable developers to automatically generate code from system-level actors that can both monitor and stimulate the system under design to ensure that the application will meet its functional requirements. Designs are validated in a virtual mode that links design documentation and implementation and generates production quality code that is readily deployable.
In general, executable specifications provide the basis for model validation through animated simulation. The solution is functionally validated with reference to the predefined requirements and the dynamic interaction of system components simulated during virtual system integration testing. Finally, integration testing is carried out. Such validation phases lead to the production of iterative prototypes. They can be employed to evolve the model in the design phase toward a definition of its software-architecture, while automatic code-generation tools can greatly speed up the implementation phase.
The identification of system components and their communication structure are key activities in the capture phase. The complexity of the dialogs is indicative of the quality of the selected partitioning that results from the exploration of the design space and the information flow between the identified components. Iterating such steps leads to the essential object model in a UML-based approach, or the identification of the activity chart hierarchy in an approach based on the functional decomposition paradigm.
Live sequence charts
In many software applications, feature testing is done to an adequate level. However, it is much harder to test expected and unexpected interactions between features. However, by turning sequence charts into a formal semantics-based language, model checking can be extended to not only cover functional requirements but also virtual system integration testing of interacting features. More generally, it also covers verification of conformance of object models with requirements, expressed as scenarios.
Sequence diagrams can be enriched via live sequence charts, adding the capability to enforce progress along instance lines and for message reception. By adding activation conditions and more general pre-charts, situations where the scenario must be observed can be clearly captured. In solutions such as Rhapsody from I-Logix Inc., UML sequence diagrams have been semantically enhanced along these lines, opening the way to exploit the semantic relationship between the object model and associated scenarios for formal consistency checks. The UML formal verification suite ensures that all interobject communication complies to the dialogs captured in live sequence charts. In the future, formal verification capabilities will be extended to cover virtual system integration.
Model checking techniques
Model checking requires the creation of a complete test suite, where all possible combinations of inputs must be examined in order to check that certain behavior requirements are not violated. A whole generation of research has gone into the development of efficient model-checking techniques. In 1981, Ed Clarke showed that for finite state machine models, a complete analysis can be carried out in finite time, because of the regularity of the model representation. Key milestones since then have been symbolic representations of models, compositional methods allowing model checking to focus on design components and various abstraction techniques that focus on unbounded data items.
As a prerequisite for applying this technology, a rigorous semantic foundation of the supported modeling tool is required. Combined with model-checking capabilities, it effectively turns these tools into a formal method for ensuring compliance with industry safety standards, such as Cenelec for train systems. In cooperation with key industrial partners in automotive, avionics and train systems, the Offis Systems research institute has advanced the technology to a level where it is capable of routinely handling typical electronic control unit models. I-Logix and OSC, the commercial spin-off of Offis, have entered into a strategic partnership to offer this technology to the embedded system-and software market via a set of tools with a simple user-interface.
The product is optimized for model debugging that prioritizes fast turnaround times over completeness and model verification that emphasizes completeness and is based heavily on abstraction to reduce verification time. Model checking can therefore be used to create a golden device that has a fully and rigorously validated specification—a formally proven essential object model—that is taken as reference for all subsequent implementation steps.
Generating test vectors
Once the golden device has been created, it can be used as a reference for tests. Ideally, it is necessary to prove that all functionality captured during the specification phase is realized in the embedded system.
Given the fact that physical entities are now involved, it is possible to derive test-cases—better known as test-vectors—from the golden device that capture its main functionality. All information collected during the system or component specification stage or both is used, including the executable model, requirements on the model and scenarios. These guide the process of extracting meaningful test cases automatically, allowing a high degree of conformance testing of implementations against their specification.
Scenario-driven test vectors additionally allow black box testing of an implementation against its requirements. The user can configure testbenches from selected scenarios to automatically derive test cases for feature interaction and resource contention stress testing. Invoking a testbench will cause the generation of stimuli to the UML model which, at the same time, follow all selected scenarios.
The testbench thus effectively replaces manual replay of operation calls and events originating from actors through the automatic generation of those compliant to the scenarios. At the same time it monitors the communication between objects for compliance with the selected scenarios. Any violations will be detected by the monitor and shown to the user as a replay of the UML model, animating the selected sequence diagrams.
Model-driven test generation, which requires looking inside the model, extends this capability by allowing the user to drive the UML model into situations where activation conditions of sequence charts apply, or to derive test cases covering all operation calls, event generations, guards or states of the object model.
The challenge stemming from today’s growth in complexity of embedded software applications and the pervasive nature of these applications can be met only by following a model-based development process. The real-time embedded system needs to be executed as it is being designed, and advanced formal validation techniques need to be incorporated into the design flow.
Werner Damm is cofounder, Offis Systems and Consulting (oldenburg, germany). Moshe Cohen is director of systems products, I-Logix inc. (Andover, Mass.).
|
|
|
|
 |
|
|
|
|
CAREER CENTER
Ready to take that job and shove it?
SEARCH JOBS
SPONSOR
RECENT JOB POSTINGS
CAREER NEWS
|
|
|
|
RSS
RSS| 
Digital| 
Mobile
