Formal Verification of Simulation Traces

Background:

Simulation engines provide detailed understanding of how a system behaves in a particular environmental conditions. Each simulation trace corresponds to one particular thread of system behavior, but this behavior is recorded in a very detailed fashion. Simulation traces however are just that, a faithful collection of system parameter values across time steps. They provide no understanding of what properties the trace conforms to or what characteristics they possess. One would need to perform further analysis to ascertain insights about the generated traces.

Model checking tools on the other hand consider all possible behaviors of a given system. They attempt to verify that all possible behaviors of a given system will conform to a specific property. Thus model checking tools tend to consider smaller abstract systems with manageable size of possible states where the information contained in each state is kept to a minimum level. The properties they can handle are usually very expressive and intuitive. Their additional lure is the ability to provide counter examples in the cases where the given property is not maintained by the given system description.

Our work:

Our work aimed to bring together the strength of simulation tools and model checkers. The goal was to utilize model checkers to assess desired property conformance on part of almost real life like traces recorded by simulation engines. Since, simulation traces contain just one single trace of behavior, it may seem very straightforward to analyze them with the model checker. However the very nature of simulation traces containing fine grained detailed values for each state the system goes through at each time step turns out to be a huge computational burden for the model checkers. Model checkers are incapable of handling the vast array of data that needs to be stored at each state, where usually the data are often of continuous rather than discrete nature. Model checking principles shy away from continuous data as they can very easily lead to state explosion problem while verifying properties. This signifies the need to abstract down simulation traces in a manner that will allow model checking tools to get off the ground while at the same time containing the flavor of being generated by the actual system not an abstracted finite state machine.

We have provided simple rules for trace abstraction. Our rules state that any abstraction performed on the traces will have to be property driven. Based on the propositions mentioned in a given property, we can narrow our focus on a subset of the different types data contained in the trace. Also, if the system designers agree, we can focus on a specific time slice of the trace. We can take abstraction steps to remove need for floating point values and even fit integer type values into suitable smaller ranges. We developed a tool that takes as input (a) the trace file and related information, (b) the time slice we want to focus on, and ©the desired property. It then automatically extracts information from the related auxiliary sources, couples them with the interesting portion of the trace and translate into Promela, the input language for the model check SPIN. Then it translates the desired property, generates scripts to execute SPIN and process feedback generated by SPIN. The tool was developed using the scripting language python. Although this tool was designed for aircraft flight simulation data, the concepts developed by us are generic ones and can be applied to any scenario involving automated systems.

The advantage of the above mechanism is that once we have generated a Promela model from a simulation trace, we can analyze it with respect to many different properties without having to regenerate the model again and again. Also the tool can recurse through a given directory full of simulation traces generated under various different environment conditions and provide an understanding about whether the system's conformance to a specific property can be influenced by the environment and exactly which environment. Thus we can retain the fine grained information collected in simulation traces and yet perform model checking to determine whether the simulation traces maintain required properties.

This methodology allows us to get an understanding of how different human action patterns and environmental conditions can interact and influence safety and effectiveness of automated safety-critical systems. Instead of working with an abstract model for the automated system, we can use simulation engines to provide us with realistic data to be verified.

Implementation:

We developed a python based tool to process and analyze the simulation traces generated by the WMC simulator developed at Georgia Tech. This tool takes a simulation trace, abstracts, models and encodes the trace into Promela, the input language for the model checker Spin. The model is then analyzed using Spin against the desired properties. The simulation traces ensue from simulation of aircraft landing procedure using the continuous descent approach. The properties that we wanted to verify involved checking that the aircraft does indeed perform the guidelines for continuous descent approach. The code for the tool can be obtained here:

Papers:

  1. Formal Analysis of Safety-Critical System Simulations; Ayesha Yasmeen, Karen M. Feigh, Gabriel Gelman, Elsa L. Gunter;ATACCS 2012.

Acknowledgements:

This material is based upon work supported by the National Science Foundation under Grant Number 0917218