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
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.
Additional Information
For additional information, please contact James Davis at james.r.davis@vanderbilt.edu or at (615) 343-7530.
ISIS Home | Model-Integrated Computing for Surety of High Assurance Systems | Technical Overview | Publications
