Programme

Contact

2013-07-17T04:41:54+00:00

You can contact the organisers for information with the following email address: dcds.info@cs.york.ac.uk

Session 1: MBSA

2013-06-20T10:08:30+00:00

Session chair: David Parker

10:30 - 12:30 Wednesday 4th September 2013
10:30	Towards a unified definition of Minimal Cut Sequences
	Authors: Pierre-Yves Chaux, Jean-Marc Roussel, Jean-Jacques Lesage, Gilles Deleuze, Marc Bouissou
	Abstract: The growing complexity of systems makes the complexity of reliability model growing, implying the need to model both the dynamics of systems and the reparability of components. The qualitative reliability analyses aim at finding the minimal representation of all the scenarios of failures and repairs of the components, leading to the system failure. This minimal representation is the set of Minimal Cut Sequences. In order to provide a formal definition of these specific scenarios, whatever the risk analysis model used, this paper proposes coherency rules for dynamic and repairable systems those dysfunctional scenarios are modeled by a finite automaton.
11:00	Introducing Temporal Behaviour into Binary Decision Diagrams
	Authors: Ernest Edem Edifor, Martin Walker, Neil Gordon
	Abstract: Binary Decision Diagrams (BDDs) are an alternative technique used in the analyses of safety-critical system fault trees. BDDs have been found to produce the exact top-event probability more efficiently by reducing computing resources drastically. Unfortunately, this efficient technique is not used in the analysis of fault trees featuring sequential ordering of events. However, in the real world, the sequential ordering of events cannot be overlooked because it produces a more accurate evaluation of systems. We introduce a new technique, Temporal BDD (TBDD), that incorporates temporal behaviour – via Priority-AND gates – into BDDs. TBDD provides the exact results for both qualitative and quantitative analyses. However, unlike BDD, quantitative analyses cannot be performed on 'unminimised' cut sequences yet. It is hoped that this work will form the foundation for the full qualitative and quantitative analyses of Dynamic Fault Trees and Temporal Fault Trees in the near future.
11:30	Preliminary System Safety Analysis with Limited Markov Chain Generation
	Authors: Pierre-Antoine Brameret, Jean-Marc Roussel, Antoine Rauzy
	Abstract: Markov chains are powerful and versatile tool to calculate reliability indicators.However, their use is limited for two reasons: the exponential blowup of the size of the model, and the difficulty to design models. To overcome this second difficulty, a solution consists in generating automatically the Markov chain from a higher level description, e.g. a stochastic Petri net or an AltaRica model. These higher level models describe the Markov chain implicitely. In this article, we propose an algorithm to generate partial Markov chains. The idea is to accept a little loss of accuracy in order to reduce the size of the generated chain. The cornerstone of this method is a Relevance Factor associated to each state of the chain. This factor enables the selection of the most representative states. We show on an already published test case, that our method provides very accurate results while reducing dramatically the complexity of the assessment. It is worth noticing that the proposed method does not depend on any particular high-level modeling formalism.
12:00	Using Coloured Petri Nets for integrated reliability and safety evaluations
	Authors: Bruno Pinna, Genia Babykina, Nicolae Brinzei, Jean-Francois Petin
	Abstract: Integrated Deterministic and Probabilistic Dependability Analysis (IDPDA) is respectively required for safety properties verication and reliability & availability assessment of critical systems. This paper presents an approach towards IDPDA using Coloured Petri Nets (CPN). Contributions are related to: (a) hierarchical modelling guidelines that cover deterministic and probabilistic features of a physical system under control, (b) coupling Monte-Carlo simulation with CPN model checking that requires a previous determinisation of the CPN stochastic model. Our approach is illustrated using a toy case study.

Session 2: MBSA (Optimisation)

2013-06-20T10:08:30+00:00

Session chair: Frank Ortmeier

14:00 - 16:00 Wednesday 4th September 2013
14:00	Combined Optimisation of System Architecture and Maintenance
	Authors: Shawulu Hunira Nggada, Yiannis Papadopoulos, David J. Parker
	Abstract: The dependability analysis of safety-critical engineering systems during the early stages of design helps ensure that requirements are met and also reduces cost that may be incurred due to modifications later in the process. One attribute that can be analysed during the infancy of design is scheduled preventive maintenance (PM) through optimisation. PM is normally optimised in isolation to other system design improvement mechanisms. It is however helpful if PM could be optimised in combination with other mechanisms such improving the system's architecture. By combining these optimization objectives more design possibilities can be simultaneously explored, therefore helping to make better design decisions. In this paper we explore this type of optimization by using HiP-HOPS a scalable dependability analysis and optimisation tool.
14:30	Multi-objective Architecture Optimisation Modelling for Dependable Systems
	Authors: Zhibao Mian, Leonardo Bottaci
	Abstract: The design of dependable systems must address both cost and dependability (i.e. safety, reliability, availability and maintainability) concerns. For large systems, the design space of alternatives with respect to both dependability and cost is very large and automation is essential to explore this space. The model-based approach to the development and analysis of complex dependable systems is increasingly popular and recently, the Architecture Analysis and Design Language (AADL) has emerged as a potential future standard for model-based development of dependability-critical systems. The paper tackles the problem of describing, within an AADL model, the design space of alternatives. A new AADL property set is proposed for modelling component and system variability for cost and dependability optimisation. The proposed method is illustrated with an example of an AADL model of a safety critical embedded system.
15:00	Implementing the functional requirements for determining the optimal arrangement of a distributed charging infrastructure
	Authors: Tamás Kurczveil, Eckehard Schnieder
	Abstract: The optimized operation of future traffic by intelligent control systems will need to take into account boundary conditions that arise from alternative drive concepts. New challenges will need to be mastered when it comes to corresponding energy systems, control of operations, and communication interfaces, such as needed for the sufficient energy supply of traffic participants. However, they will need to be conformed to existing systems, technologies, and infrastructure to allow the common operation and positioning of charging elements with minimum interference between different modes of transport. Funded by the German Federal Ministry of Transport, Building and Urban Development (Bundesministerium für Verkehr, Bau und Stadtentwicklung) the project emil (Elektromobilität mittels induktiver Ladung - electric mobility via inductive charging) will integrate an inductive vehicle charging system and a compatible prototype bus fleet into Braunschweig's traffic infrastructure. This paper describes the methodic approach and the implementation of functional requirements in a traffic simulation tool that are required for an evaluation of future urban road traffic with an increased rate of electric vehicles. The modifications can subsequently be used to determine the optimal placement of the corresponding charging infrastructure with consideration of conventional traffic demand.
15:30	Integrated Monitoring Tasks for the Safety of Critical Systems
	Authors: Amer Dheedan, Ajith Kumar Parlikad
	Abstract: Nuclear power plants, chemical processes and means of transportation are seen as critical systems, the failure of which may hazard lives and assets. Thus, the safety of such systems is rigorously considered and established during the design and operational stages. In the design stage, an off-line safety analysis investigates, retrofits and affixes whenever necessary fault-tolerant means and reliable components. In the operational stage, the functionality of systems is monitored through the delivery of three safety tasks: fault detection and diagnosis, alarm annunciation and fault controlling. However, systems still showing malfunctions and hazardous failures continue to be recorded. To address this issue, this paper develops a distributed on-line safety monitor. The monitor aims to achieve an effective integration among the delivery of the three safety tasks through the exploitation of the thorough and cost-effective abstraction of the off-line safety analysis and the distributed reasoning of a multi-agent system.

Session 3: DES Control

2013-06-20T10:08:30+00:00

Session chair: Klaus Schmidt

16:30 - 18:00 Wednesday 4th September 2013
16:30	Fault-Hiding Control Reconfiguration for a Class of Discrete Event Systems
	Authors: Thomas Wittmann, Jan Richter, Thomas Moor
	Abstract: Fault-hiding control reconfiguration aims at hiding a fault from the nominal controller, so that the closed-loop system subject to faults complies as well as possible with the nominal design requirements. This is achieved by suitably influencing the signals between nominal controller and faulty plant using a reconfiguration block. In discrete event systems, the reconfiguration block needs to convert plant events to controller events, and vice versa, such that the self-reconfiguring closed-loop system is non-conflicting, complete, controllable and conforms with the design specifications. In this paper, we discuss the resulting control architecture, state our reconfiguration problem and address the synthesis of discrete event dynamic reconfiguration blocks. To illustrate our results, we provide a running example.
17:00	Synthesizing bounded-delay communication protocols for decentralized discrete-event systems
	Authors: John Daniel Maguire, Laurie Ricker
	Abstract: A strategy for synthesizing communication protocols for a given upper-bounded delay d is proposed. Although the strategy is illustrated for the decentralized control domain, it is straightforward to adapt this strategy to decentralized diagnosis and prognosis. Previous work in the control domain has examined circumstances when all observations are communicated, under conditions of bounded delay, as well as determining whether or not a synchronous communication protocol is robust w.r.t. a given bounded delay. We are interested, without resorting to fully timed models, in the direct synthesis of communication protocols for a given upper-bounded delay [0,d].
17:30	Algebraic Synthesis for Online Adaptation of Dependable Discrete Control Systems
	Authors: Christian Hillmann, Olaf Stursberg
	Abstract: Common practice in industrial design of discrete controllers as well as in most synthesis procedures advocated for discrete control in academia is to create the control logic and to transfer it into a PLC language before start-up. Changes in the operational constraints of the controlled process (e.g. of available resources, nominal set-points, occurrences of failures) have to be accounted for by dedicated alternative routines, i.e. dependability is restricted to variations which are envisaged during design. In contrast, the approach proposed in this paper operates online on an uncontrolled model process model to compute a control strategy that is adapted to the current set of constraints. By using algebraic computations largely resembling techniques for discrete-time continuous-valued controllers, a perceived process variation (including newly defined control-goals) are first assessed with respect to the existence of a feasible successful control strategy, before such a dependable strategy is computed.

Session 4: DES Diagnosis

2013-06-20T10:08:30+00:00

Session chair: Jose Cury

10:30 - 12:30 Thursday 5th September 2013
10:30	Conjunctive Decentralized Diagnosis of Discrete Event Systems
	Authors: Takashi Yamamoto, Shigemasa Takai
	Abstract: In this paper, we study conjunctive decentralized diagnosis of discrete event systems. A notion of conjunctive codiagnosability which guarantees that any failure is detected by a conjunctive decentralized diagnoser within a uniformly bounded number of steps has been defined in literature. However, the existing condition for the system not to be conjunctively codiagnosable is sufficient but not necessary. Motivated by this fact, we propose a new algorithm for verifying conjunctive codiagnosability based on a necessary and sufficient condition for the system not to be conjunctively codiagnosable. To construct a conjunctive decentralized diagnoser for a conjunctively codiagnosable system, we need to compute the delay bound. We show how to compute the delay bound.
11:00	Supervision Patterns: Formal Diagnosability Checking by Petri Net Unfolding
	Authors: Houssam-Eddine Gougam, Audine Subias, Y. Pencolé
	Abstract: This paper addresses the problem of checking diagnosability of supervision patterns in discrete-event systems. With a supervision pattern, it is possible to represent a complex behavior of the system, and especially a faulty behavior. As opposed to classical diagnosability analyzers that check by exploring the marking graph of the underlying net, the proposed method relies on Petri net unfoldings and thus avoids the combinatorial explosion induced by the use of marking graphs. The method is an adaptation of the twin-plant method to net unfolding: a pattern is diagnosable if the unfolding representing the twin-plant does not implicitly contain infinite sequences of events that are ambiguous.
11:30	Active Diagnosis of Deterministic I/O Automata
	Authors: Melanie Schmidt, Jan Lunze
	Abstract: A method for the active fault diagnosis of systems modeled by sets of deterministic input/output automata is presented, where each automaton describes the behavior of the system subject to a different fault. It is shown that the system is diagnosable if and only if there are no equivalent states in different automata. An active diagnostic algorithm is presented, which generates adequate input sequences for the system and evaluates the outputs of the system in order to identify the present fault. The applicability of the developed method is demonstrated by means of an example.
12:00	A Discrete Time Consensus Approach for Fault Detection and Recovery in Unreliable Networks
	Authors: Maria Pia Fanti, Agostino Marcello Mangini, Walter Ukovich
	Abstract: In this paper we address the problem of the fault detection and recovery in networks of agents with discrete time dynamics. In particular, we apply a fault detection and recovery approach, proposed for the standard linear consensus protocol, to a consensus algorithm that has been previously presented by the authors and is based on a triangular splitting of the iteration matrix of the standard consensus algorithm. Moreover, we show that for a particular topology of the communication graph the fault recovery strategy can be implemented by the agents in a fully decentralized and autonomous approach. An example describes how in the considered framework the fault recovery is implemented by each agent.

Session 5: Application

2013-06-20T10:08:30+00:00

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).

Session 6: DES Control

2013-06-20T10:08:30+00:00

Session chair: Maria Pia Fanti

16:30 - 18:00 Thursday 5th September 2013
16:30	Computation of Fault-Tolerant Supervisors for Discrete Event Systems
	Authors: Ayse Nur Sulek, Klaus Schmidt
	Abstract: Fault-tolerance addresses the problem of operating a system even in case of faults. In this paper, we study fault-tolerance in the supervisory control framework for discrete event systems (DES). We consider DES, where certain events might no longer be possible in case a fault happens. In this setting, we first identify necessary and sufficient conditions for the existence of a supervisor that realizes a given behavioral specification both in the non-faulty and in the faulty case. We further show that it is possible to determine a supremal fault-tolerant sublanguage in case the existence condition is violated. Finally, we propose an algorithm for the computation of this sublanguage and prove its correctness. Different from existing work, our fault-tolerant supervisor allows fault occurrences and system repairs at any time. The concepts and results developed in this paper are illustrated by a manufacturing system example.
17:00	Heuristic Search of Supervisors by Approximated Distinguishers
	Authors: Raquel Stella Silva Aguiar, Antonio Eduardo Carrilho da Cunha, Jose E. R. Cury, Max H. de Queiroz
	Abstract: The use of distinguishers was introduced for Supervisory Control Theory (SCT) in order to simplify the task of modeling specications, while guaranteeing the synthesis of maximally permissive supervisors. On the other hand, by approximating the language of a distinguisher, a supervisor can be obtained with computational savings in the synthesis, although there is no guarantee that this is the maximally permissive solution. The main purpose of this work is to propose a procedure to obtain the least restrictive achievable supervisor, in the context of approximations in the SCT with distinguishers. The procedure consists of a heuristic search for the supervisor with the highest language measure in the space formed by supervisors obtained using approximated distinguishers. A search procedure based in Genetic Algorithms was implemented and a case study illustrates the results of the method.

Session 7: MBSA

2013-06-20T10:08:30+00:00

Session chair: Jean-Marc Faure

10:30 - 12:30 Friday 6th September 2013
10:30	The AltaRica 3.0 Project for Model-Based Safety Assessment
	Authors: Tatiana Prosvirnova, Michel Batteux, Pierre-Antoine Brameret, Leïla Kloul, Abraham Cherfi, Thomas Friedlhuber, Antoine Rauzy
	Abstract: The aim of this article is to present the AltaRica 3.0 project. "Traditional" risk modeling formalisms (e.g. Fault Trees, Markov Processes, etc.) are well mastered by safety analysts. Efficient assessment algorithms and tools are available. However, models designed with these formalisms are far from the specifications of the systems under study. They are consequently hard to design and to maintain throughout the life cycle of systems. The high-level modeling language AltaRica has been created to tackle this problem. The objective of the AltaRica 3.0 project is to design a new version of AltaRica and to develop a complete set of authoring and assessment tools for this new version of the language. AltaRica 3.0 improves significantly the expressive power of AltaRica Data-Flow without decreasing the efficiency of assessment algorithms. Prototypes of a compiler to Fault Trees, a compiler to Markov chains, a stochastic and a stepwise simulators have been already developed. Other tools are under specification or implementation.
11:00	A methodology for qualitative/quantitative analysis of weighted attack trees
	Authors: A. Bobbio, Lavinia Egidi, Roberta Terruggia
	Abstract: Attack and Defense Trees (ADT) constitute a formal modeling technique that has become dominant in recent years in the area of qualitative and quantitative cybersecurity analysis of ICT and digital control systems. A Weighted-ADT (WADT) is augmented with cost or impact attributes to evidence the most convenient attack sequence in term of investment budget and provoked damage and provide an indication on how to mitigate the located breaches by means of suitable countermeasures. The original analysis technique proposed in this paper, is based on the representation of a WADT by means of an extension of Binary Decision Diagrams (BDD), called Multi Terminal Binary Decision Diagrams (MTBDD). MTBDDs allow the modeler to evaluate the probability distribution function of the cost and impact related to any possible attack scenario. A running example illustrates the methodology.
11:30	Engineering Conditional Safety Certificates for Open Adaptive Systems
	Authors: Daniel Schneider, Mario Trapp
	Abstract: In recent years, we have witnessed a strong trend towards more openness and adaptivity in many application domains of computer-based systems. In this context, the assurance of a sufficient level of safety poses serious challenges because traditional engineering and assurance approaches are usually not applicable without further ado. In order to meet these challenges, we recently introduced a framework that enables runtime safety certification based on conditional safety certificates (ConSerts). Since the definition of ConSerts relies on an adequate safety engineering backbone, we now present an engineering approach for defining ConSerts based on established safety engineering processes and techniques. The presented approach has been evaluated in an industry project in form of a feasibility study in the agricultural domain.
12:00	An Interdisciplinary Perspective to the Design and Development of Integral Safety Systems
	Authors: Christian Berger, Panagiotis Katsaros, Mahdi Bohlouli, Lefteris Angelis
	Abstract: Next generation integral safety systems are expected to provide better protection against traffic accidents by interlinking sensors and actuators of active and passive safety. A series of advanced functions will be used to mitigate collisions and if they cannot be avoided they will at least reduce their severity. We explore the interplay between key technology areas towards a holistic approach in the design of integral safety systems. First, we refer to the main problems in the design of effective systems and the associated software engineering challenges. Recent advances in sensor data analytics are then explored and their integration with decision support for vehicle control is examined. Finally, we envision that rigorous design techniques are essential for achieving adequate performance and robustness of integral safety systems, but appropriate human-machine interaction models will have to be taken into account.

Session 8: DES Control

2013-06-20T10:08:30+00:00

Session chair: Tim Kelly

14:00 - 15:30 Friday 6th September 2013
14:00	Discrete Control for Reconfigurable FPGA-based Embedded Systems
	Authors: Xin An, Eric Rutten, jean-philippe diguet, Nicolas Le Griguer, Abdoulaye Gamatie
	Abstract: This work presents an application of discrete controller synthesis (DCS) techniques to a class of dynamically reconfigurable embedded computing systems, and contributes to the general approach of control for feedback computing. We propose a general model for applications defined as data-flow graphs of computing tasks, and target execution architectures that are dynamically partially reconfigurable Field Programmable Gate Arrays (FPGAs). We define our model in terms of parallel automata. Then, we encode relevant scheduling and control requirements in terms of a DCS problem w.r.t. multiple constraints and objectives. We take into account the system reconfiguration overhead, and the resulting controller is able to make decisions by foreseeing their impact on future requests. We validate our approach by using the BZR programming language and Sigali tool for modelling and simulations, with a video processing system implementation on a specific FPGA platform.
14:30	Abstraction-based Supervisory Control for Reconfigurable Manufacturing Systems
	Authors: Harith M. Khalid, Mustafa Sancay Kirik, Klaus Schmidt
	Abstract: Reconfiguration control for discrete event systems (DES) is concerned with the realization of different system configurations by modification of the supervisory control loop. In this paper, we study the reconfiguration supervisor design for reconfigurable manufacturing systems (RMS) that comprise multiple components. We construct a modular supervisor for each configuration and system component in order to realize each active configuration and to quickly change between configurations. Different from the existing literature that is focused on monolithic design, our method is abstraction-based, and, hence applicable to large-scale DES.
15:00	State-Stability Analysis of Discrete Event Systems using Petri-net Branching Processes
	Authors: Alberto Lutz-Ley, Ernesto Lopez-Mellado
	Abstract: This paper studies fault tolerance of concurrent discrete event systems (DESs) through the stability analysis of Interpreted Petri nets (IPN) models. An efficient method for determining state stability of safe IPN models is proposed. The method is based on the analysis of the sequentially secure branching process of the DES model, which is a finite representation of a PN unfolding: a sufficient condition for stability and an algorithm for deciding the property are presented.

Invited Speaker

2013-06-20T10:08:30+00:00

09:00 - 10:00 Wednesday 4th September 2013
09:00	Assessing the probability of failure of 1-out-of-2 software-based systems: now you can multiply two small numbers ...
	Author: Bev Littlewood, Centre for Software Reliability, City University, London, UK
	You can download the slides for this talk by clicking here.

09:00 - 10:00 Thursday 5th September 2013
09:00	Diagnosis and diagnosability of discrete event systems using Petri nets
	Author: Alessandro Giua, University of Cagliari, Italy
	You can download the slides for this talk by clicking here.

09:00 - 10:00 Friday 6th September 2013
09:00	Stochastic hybrid systems
	Author: Marc Bouissou, Électricité de France, France
	You can download the slides for this talk by clicking here.