Wei Guan, Nicolae Marian, and Christo Angelov
Embedded control system, runtime verification, component-based software development, model-driven engineering, linear temporal logic
Formal verification methods, such as exhaustive model checking, are often infeasible because of high computational complexity. Runtime observers (monitors) provide an alternative, light-weight verification method, which offers a non-exhaustive yet feasible approach to monitoring system behavior against formally specified properties. This paper presents a component-based design method for runtime observers, which are configured from instances of prefabricated reusable components---Predicate Evaluator (PE) and Temporal Evaluator (TE). The PE computes atomic propositions for the TE; the latter is a reconfigurable component processing a data structure, representing the state transition diagram of a non-deterministic state machine, i.e. a Buchi automaton derived from a system property specified in Linear Temporal Logic (LTL). Observer components have been implemented using design models and design patterns specified in the COMDES framework. Observer models and their constituent components are automatically configured using the COMDES Tool-chain. The application design model, including the runtime observers, is then transformed into a semantics-preserving Simulink model, making it possible to verify formally specified properties via simulation. The presented method has been experimentally validated in an industrial case study---a control system for a safety-critical medical ventilator unit.
Important Links:
Go Back
