Model Based Safety Analysis with smartIflow

Verification of safety requirements is one important task during the development of safety critical systems. The increasing complexity of systems makes manual analysis almost impossible. This paper introduces a new methodology for formal verification of technical systems with smartIflow (State Machines for Automation of Reliability-related Tasks using Information FLOWs). smartIflow is a new modeling language that has been especially designed for the purpose of automating the safety analysis process in early product life cycle stages. It builds up on experience with existing approaches. As is common practice in current approaches, components are modeled as finite state machines. However, new concepts are introduced to describe component interactions. Events play a major role for internal interactions between components as well as for external (user) interactions. Our approach to the verification of formally specified safety requirements is a two-step method. First, an exhaustive simulation creates knowledge about a great variety of possible behaviors of the system, especially including reactions on suddenly occurring (possibly intermittent) faults. In the second step, safety requirements specified in CTL (Computation Tree Logic) are verified using model checking techniques, and counterexamples are generated if these are not satisfied. The practical applicability of this approach is demonstrated based on a Java implementation using a simple Two-Tank-Pump-Consumer system