The goal of this project is to develop formal-method based system design tools with an emphasis on reliability, safety, and security. The tools will utilize models, generic in construct but domain specific for each application. This project is a joint effort with Sandia National Laboratories.

Objectives

The primary objectives of this project involve increasing the reliability, safety, and security of systems by performing analysis of design models. Analyzing these aspects of a system can greatly reduce the time required to produce a safe, secure, and reliable system by assuring the system meets specifications before prototyping.  The analyses rely heavily on formal verification and validation methods, especially symoblic model analysis.

The specific analysis tools that are being identified and developed include: verification of the consistency of requirements, validation of design models versus requirement models, simulation of system behavior (including forward and backward system execution), safety and reliability analysis (using proprietary tools), and automatic fault-tree generation. From an integrated model, safety, reliability, and diagnostic analyses can be performed. 
 

Technical Overview

The modeling approach is based on multiple-aspect structural and behavioral models. The Graphical Modeling Editor (GME) is used to implement the modeling environment. System behavior is described in a discrete state space using hierarchical, parallel state machines.  Both nominal and fault system behaviors are modeled.  System structure and component failures are modeled in the physical models. Relationships between the structure and behavioral aspects are explicitly modeled. This ensures the relationship between physical failure modes and system behavior are explicitly represented.

Figure 1: An example set of behavioral models in GME
 

The domain specific models are converted into a domain independent representation.  An extension of Finite State Machines (FSM) is used as the domain independent modeling paradigm.  The domain independent representation is then converted into a symoblic system representation.  The symoblic models can be used to represent and analyze large systems (state spaces of 2^100 have been analzyed).

Ordered Binary Decision Diagrams (OBDDs) are used to symbolically represent the system. Using a symbolic representation allows exhaustive search techniques to be used on the system without the need to enumerate the discrete state space. OBDDs have been used to represent and analyze systems with 10^100 unique, discrete states. OBDDs allow for the analysis of "real" systems.

The State Space Analysis Tool (SSAT) was designed to provide model analysis capabilities. SSAT converts from the GME models to a symbolic (OBDD) representation of the system. Then, the SSAT allows the user to validate their models through simulation, reachability analysis, loop detection, and deterministic analysis. Once the models have been validated, the user can use the SSAT to generate safety and reliability information for further analysis. A tool developed at Sandia, WinR, is used to analyze the safety and reliability information SSAT generates.
 

Figure 2: The SSAT User Interface
 

Figure 3: An example fault tree automatically generated by SSAT
 

Current Project Status

Currently, the system is being used at Sandia National Labs. A version of GME was configured for the specified modeling paradigm. The SSAT has been implemented and fielded. The tools are currently being used for evaluation purposes.  Analyses of  available high consequence systems are being performed with SSAT.

Among the current research tasks are: integrating security information into the modeling environment and analysis tools, extending the modeling environment to better support Sandia's "Surety Process" of development, and extending the SSAT to incorporate more efficient OBDD analysis routines. With these enhancements, the tools will cover more of the areas of concern for the surety domain and allow much larger systems to be analyzed.  Among the future directions of the research is the involvment of timing in the models.  Timing information is not explicitly used in the current system.  Improvements of system scalability are always being investigated.