Session 5: Application

Session chair: Jean-Marc Roussel

14:00 - 16:00 Thursday 5th September 2013
14:00 Systems Modeling with EAST-ADL for Fault Tree Analysis through HiP-HOPS
Authors: DeJiu Chen, Nidhal Mahmud, Martin Walker, Lei Feng, Henrik Lonn, Yiannis Papadopoulos
Abstract: EAST-ADL is a domain-specific modeling framework with methodology and language support for the engineering of automotive embedded systems. In regard to functional safety, it aims to provide the maximum possible support for ISO 26262 so that all safety related information can be consolidated seamlessly in a common system model together with the requirements specification. This paper describes the EAST-ADL support for the modeling of plausible error behaviors as an orthogonal system view. We introduce in particular an integration of such EAST-ADL models with the HiP-HOPS method for automated temporal fault tree analysis.
14:30 Boolean and Modular Abstractions for Programmable Logic Controllers
Authors: Sebastian Biallas, Dimitri Bohlender, Stefan Kowalewski
Abstract: This paper introduces a Boolean and a modular abstraction of programs for programmable logic controllers in order to make them amenable for formal verification. In the Boolean abstraction, complex control-flow conditions are replaced by fresh Boolean input variables to defer the evaluation of such conditions. The modular abstraction replaces function block calls by so-called function block summaries, which over-approximate their possible return values. Both abstractions can subsequently be refined in an automatic process to allow for checking of complex programs using expressive formulae. The approach has been implemented in the Arcade.PLC model checker, which is used to show the effectiveness in a case-study. 
15:00 An Analytic Expression of the Reliability of Transmissions in Fieldbuses with Propagated Failures
Authors: Damien aza-vallina, Jean-Marc Faure
Abstract: This paper shows first that the behaviour of a fieldbus whose terminals can be represented by multi-state components with propagated failures may be described by a set of connected mode automata; the input and output flows of these automata represent either data exchanges or failure propagations. A method to obtain an analytic expression of the reliability of a transmission between two terminals from this model is then proposed.
15:30 On Formal Verification of Function Block Applications in Safety-related Software Development
Authors: Doaa Soliman, Georg Frey, Kleanthis Thramboulidis
Abstract: The realization of application software, which is a part of a safety-related system (SRS), is a challenging engineering task due to the necessary verification activities. To assure that safety-related systems will offer the necessary risk reduction required to achieve safety, the IEC 61508 standard software safety lifecycle requirements. The standard specifies verification activities associated with all the development phases. In this paper, the verification activity of the safety application code against the model design is presented. To this end, the code, which is implemented according to IEC 61131-3 programming standard and PLCopen specification, is automatically transformed to Uppaal formal models using a software tool called SA2TA (Safety Application to Timed Automata). Moreover, to automate the validation of the transformed formal model, another tool called TCG (Test Case Generator) is presented. The method is demonstrated using a case study. The main contribution of this paper is the formalization approach of the application software responsibilities in TCTL (Time Computational Temporal Logic).