A Model-Driven Approach for Safety Critical Systems

Abstract

Rapidly increasing dependence on computers for the purpose of monitoring, control and automation raise safety concerns. Some applications demand high availability and reliability of the system. Example of such systems are the y-by-wire, pace-maker (for heart patients) and stability control systems. Failure or unavailability of such systems usually have severe consequences. The complexity of system software has increased in recent years. While a remarkable amount of effort has gone into the standardization of PLC programming, control systems are still largely implemented in an ad hoc manner. Shorter time-to-market and higher expectations on reliability of embedded systems, demands improvements in the development practices. We suggest using model-driven development (MDD) paradigm for implementing safety critical systems using IEC 61499 standard. IEC 61499 is a recent standard for PLC programming using a block-diagram oriented visual language. The component-based approach of IEC 61499 supports a modular system design with a scope of re-usability of models. We have proposed a formal verification approach for IEC 61499 systems for the purpose of evaluating reliability. An observer based approach is proposed for capturing system properties in an intuitive manner. We employ model checking and reachability analysis algorithms that formally prove the absence of certain errors in the system, thus providing reliability guarantees. This formal verification approach in conjunction with synchronous execution semantics ensure that the system is deterministic, free from deadlocks and satisfies certain correctness criteria. We have implemented an integrated development environment (IDE) named TimeMe Studio, for safety critical systems. It implements IEC 61499 as a domain specific language that leverages the automatic code generation using synchronous compiler, observer-based formal verification and static timing analysis. This provides certain guarantees on the predictability, dependability and timeliness aspects of safety critical systems. Observability and executability features of MDD are provided by implementing a visual simulator.