Almost all of the capabilities developed in this project depend on the use of formal verification tools such as model checkers and theorem provers. Model checkers use a variety of underlying technologies, but essentially work by checking if a property holds for every reachable state. Recent breakthroughs have made it possible for symbolic (BDD-based) model checkers to explore very large (1020 to 10200) reachable states. Bounded model checkers use a combination of state space exploration and induction to deal with even larger state spaces.
The primary advantage of model checkers is that they are relatively easy to use and produce counterexamples when a property is not true. Their main disadvantage is that even moderately large models can still exceed the capacity of the model checker.
Theorem proving is a technique where both the system and its desired properties are expressed as formulas in a mathematical logic, and these properties are shown to hold through use of a mechanical theorem prover. While theorem provers do not have the state space limitation of model checkers, they generally require more skill and labor to prove the desired properties.
As part of this project, we have developed translators from several modeling languages to a variety of model checkers and theorem provers. In the first part of the project, we demonstrated the viability of this approach by developing translators from the RSML-e language to the NuSMV model checker and the PVS theorem prover. Using these translators, we were able to prove hundreds of functional and safety properties about the mode logic of a Flight Guidance System, finding several errors in the process. More details can be found in the papers listed at the end of this page.
To make this same capability available with commercial tools, we recently developed translators from the Lustre language that the SCADE tool set from Esterel Technologies is based on, making it possible to prove properties about SCADE models. By using the Simulink gateway provided by Esterel Technologies, we have also been able to prove properties of Simulink models.
Most recently, we have developed a translator from Lustre to the SAL (Symbolic Analysis Language) developed by SRI International, allowing us to use the model checkers and theorem provers included in the SAL toolset. We have also developed translators from the Reactis test case generation tool to Lustre, providing an alternative path from Simulink to Lustre. This translator is being extended to support a subset of StateFlow models as well as Simulink.
Publications Related to Formal Methods
home | welcome | quick page | philosophy | team | research | quote | links | new?
Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 18 October 2002 (09:23:08)