Industrial Experiments in IMS, ATC, and SDR Projects of Property Verification Techniques

Advances in Systems Analysis, Software Engineering, and High Performance Computing - Handbook of Research on Embedded Systems Design ◽

10.4018/978-1-4666-6194-3.ch019 ◽

2014 ◽

pp. 455-468

Author(s):

Emmanuel Gaudin

Keyword(s):

Modeling Languages ◽

Critical Systems ◽

Research Projects ◽

Safety Critical ◽

Industrial Experiments ◽

Representative Model ◽

Safety Critical Systems ◽

Paris Region ◽

Property Verification ◽

Verification Techniques

The increasing complexity of embedded systems calls for verification techniques to make sure the systems behave properly. When it comes to safety-critical systems, this aspect is even more relevant and is now taken into consideration by certification authorities. For that matter, property verification is accepted to be done not only on the system itself but also on a representative model of the system. This chapter first introduces the different properties and how they could be expressed. Then associated modeling languages characteristics are discussed to describe the systems on which the properties can be verified. Finally, different technologies to verify the properties are presented, including some practical examples and existing tools. This last part is illustrated by several research projects such as the PRESTO ARTEMIS European project and the exoTICus System@tic Paris Region competitiveness cluster project.

Download Full-text

AUTOMATIC FAILURE ANALYSIS USING SAFECHARTS

International Journal of Software Engineering and Knowledge Engineering ◽

10.1142/s0218194007003136 ◽

2007 ◽

Vol 17 (01) ◽

pp. 57-78

Author(s):

YEAN-RU CHEN ◽

PAO-ANN HSIUNG

Keyword(s):

Failure Analysis ◽

Formal Verification ◽

Timed Automata ◽

Consumer Electronics ◽

Critical Systems ◽

Human Beings ◽

Medical Systems ◽

Safety Critical ◽

Safety Critical Systems ◽

Verification Techniques

With rapid developments in science and technology, we now see the ubiquitous use of different types of safety-critical systems in our daily lives such as in avionics, consumer electronics, and medical systems. In such systems, unintentional design faults might result in injury or even death to human beings. To avoid such mishaps, we need to verify safety-critical systems thoroughly and formal verification techniques such as model checking are a very promising approach. However, modeling the systems formally is a challenging task, which is further aggravated by the necessity to model faults and automatic repairs in safety-critical systems. Currently, there is no automatic technique in formal verification that can aid system designers in formally modeling the faults and repairs. This work contributes by proposing an extension to the Safecharts model so that faults and repairs are easily modeled and then the Safecharts are transformed into semantically equivalent Extended Timed Automata models that can be directly model checked. In this way, automatic failure analysis techniques are integrated into the SGM model checker. Application examples show the feasibility and benefits of the proposed model-driven verification of safety-critical systems.

Download Full-text