Search

Recent advances in modeling languages have made it feasible to formally specify and analyze the behavior of large system components. Synchronous data flow languages, such as Lustre, SCR, and RSML are well suited to this task, and commercial versions of these tools such as SCADE and Simulink are growing rapidly in popularity among designers of safety critical systems, largely due to their ability to automatically generate code from the models. At the same time, advances in formal analysis tools have made it practical to formally verify important properties of these models to ensure that design defects are identified and corrected early in the lifecycle. This report describes how such formal verification tools have been applied to the FCS 5000, a new family of Flight Control Systems being developed by Rockwell Collins Inc.

Assurance that a formal specification (system specification or software specification) possesses desired properties can be achieved through (1) manual inspections, (2) formal verification of the desired properties, or (3) simulation and testing of the specification. To achieve the high level of confidence in the correctness required in a safety-critical system, all three approaches must be used in concert. We have developed an specification language, called RSML/sup -e/, and an environment, called NIMBUS, which provides support for all these activities. The three V&V techniques fill complementary roles within the validation and verification process. Manual inspections and visualization provide the specification team, customers, and regulatory representatives the means to informally verify that the behavior described formally matches the desired "real world" behavior of the system. RSML/sup -e/ is a fully formal, synchronous, data-flow language. NIMBUS supports large-scale, distributed simulation of specifications through communications over Microsoft's distributed COM or OMG's CORBA.

Inaccuracies, or deviations, in the measurements of monitored variables in a control system are facts of life that control software must accommodate $the software is expected to continue functioning correctly in the face of an expected range of deviations in the inputs. Deviation analysis can be used to determine how a software specification will behave in the face of such deviations in data from the environment. The idea is to describe the correct values of an environmental quantity; along with a range of potential deviations, and then determine the effects on the outputs of the system. The analyst can then check whether the behavior of the software is acceptable with respect to these deviations. In this report we wish to propose a new approach to deviation analysis using model checking techniques. This approach allows for more precise analysis than previous techniques, and refocuses deviation analysis from an exploratory analysis to a verification task, allowing us to investigate a different range of questions regarding a system's response to deviations.

Automated translation, or code generation, of a formal requirements model to production code can alleviate many of the problems associated with design and implementation. In this paper, we outline the requirements of such code generation to obtain a high level of confidence in the correctness of the translation process. We then describe a translator for a state-based modeling language called RSML (Requirements Specification Modeling Language) that largely meets these requirements.

Although autocoding techniques promise large gains in software development productivity, their "real-world" application has been limited, particularly in safety-critical domains. Often, the major impediment is the missing trustworthiness of these systems: demonstrating - let alone formally certifying - the trustworthiness of automatic code generators is extremely difficult due to their complexity and size. We develop an alternative product-oriented certification approach which is based on five principles: (1) trustworthiness of the generator is reduced to the safety of each individual generated program; (2) program safety is defined as adherence to an explicitly formulated safety policy; (3) the safety policy is formalized by a collection of logical program properties; (4) Hoare-style program verification is used to show that each generated program satisfies the required properties; (5) the code generator itself is extended to automatically produce the code annotations required for verification. The approach is feasible because the code generator has full knowledge about the program under construction and about the properties to be verified. It can thus generate all auxiliary code annotations a theorem prover needs to discharge all emerging verification obligations fully automatically. Here we report how this approach is used in a certification extension for AutoBayes, an automatic program synthesis system which generates data analysis programs (e.g., for clustering and time-series analysis) from declarative specifications. In particular, we describe how a variable-initialization-before-use safety policy can be encoded and certified.

Formal specifications can be hundreds of pages in length-a reflection of the size and complexity of the systems being specified. Lengthy documents are difficult to read understand, and use. Program slicing was developed to address these issues for programs. The authors apply similar techniques to formal specifications expressed as hierarchical state machines. They present a two tiered approach to slicing (or simplification) of hierarchical state machines. They have applied their techniques to a large case study and present empirical data highlighting the reduction and simplification capabilities of their approach to large specifications.

Code certification is a lightweight approach for formally demonstrating software quality. Its basic idea is to require code producers to provide formal proofs that their code satisfies certain quality properties. These proofs serve as certificates that can be checked independently. Since code certification uses the same underlying technology as program verification, it requires detailed annotations (e.g., loop invariants) to make the proofs possible. However, manually adding annotations to the code is time-consuming and error-prone. We address this problem by combining code certification with automatic program synthesis. Given a high-level specification, our approach simultaneously generates code and all annotations required to certify the generated code. We describe a certification extension of AutoBayes, a synthesis tool for automatically generating data analysis programs. Based on built-in domain knowledge, proof annotations are added and used to generate proof obligations that are discharged by the automated theorem prover E-SETHEO. We demonstrate our approach by certifying operator- and memory-safety on a data-classification program. For this program, our approach was faster and more precise than PolySpace, a commercial static analysis tool.