Authors: Johnson, Timothy; Suhaib, Syed

Abstract: Existing standards for dependable systems, and in particular DO-178B for commercial flight software and DO-254 for flight hardware, are best suited to "clean sheet of paper" designs for entirely new systems. Yet, in industry - and in particular for safety-critical systems - entirely new designs are relatively rare, and generally entail very high risks in both financial and performance terms. This paper briefly surveys the state of the art in methods for certifying legacy (or COTS) systems, and proposes improved procedures for the future, including the increased use of formal verification methods to enhance dependability. As standards evolve, these procedures may ameliorate the very high current cost and risk associated with present compliance requirements.

Keywords: embedded systems,software,controls,legacy systems,standards,certification,safety

Identifier: 10.3182/20090610-3-IT-4004.00027

Conference: 2nd IFAC Workshop on Dependable Control of Discrete Systems (2009)

Location: École Normale Supérieure de Cachan, Italy

Start Date: Wed Jun 10 2009 - End Date: Fri Jun 12 2009

Authors: Pantelic, Vera; Lawford, Mark

Abstract: This paper considers optimal supervisory control of probabilistic discrete event systems (PDESs). PDESs are modeled as generators of probabilistic languages. The probabilistic supervisors employed enable/disable events with certain probabilities. We consider the case when there exists no probabilistic supervisor to match the behaviour of a plant to a probabilistic requirements specification. First, we define a notion of distance between two probabilistic generators. Then, given a plant and a desired probabilistic behaviour, we present an algorithm that minimizes the distance between the desired behaviour and the behaviour of the controlled plant achievable under probabilistic control.

Keywords: supervisory control,stochastic systems,discrete event systems,optimal control

Identifier: 10.3182/20090610-3-IT-4004.00018

Conference: 2nd IFAC Workshop on Dependable Control of Discrete Systems (2009)

Location: École Normale Supérieure de Cachan, Italy

Start Date: Wed Jun 10 2009 - End Date: Fri Jun 12 2009

Authors: Soliman, Doaa; Frey, Georg

Abstract: Functional Safety is a major concern in the design of automation systems today. Many of those systems are realized using PLCs programmed according to IEC 61131-3. PLCopen as IEC 61131 user organization specified a set of software Function Blocks to be used in Safety Applications according to IEC 61508 in 2006. The specification of Technical Committee 5 contains twenty Safety Function Blocks (SFBs) as a library together with some specifications of their use. A second part issued in 2008 demonstrates the use of the defined SFBs in real applications. In the presented work, formal models for the SFBs are derived from the semi-formal specification in the PLCopen documents. Those blocks are verified using model checking and the accordance of their temporal behavior with the PLCopen specification is further validated by simulation. The resulting library of formal models allows to build a formal model of a given safety application - built from SFBs - and to verify its properties. This is demonstrated using an example from the second part of the PLCopen specification.

Keywords: safety application,timed automata,PLC,safety function block,IEC 61508,IEC61131-3 verification and validation,model-checking

Identifier: 10.3182/20090610-3-IT-4004.00011

Conference: 2nd IFAC Workshop on Dependable Control of Discrete Systems (2009)

Location: École Normale Supérieure de Cachan, Italy

Start Date: Wed Jun 10 2009 - End Date: Fri Jun 12 2009

Authors: Marange, Pascale; Gouyon, David; Pétin, Jean-François; Riera, Bernard

Abstract: This paper deals with dynamic reconfiguration of DES control within the context of manufacturing system to answer product variability or production resources availability. More precisely, it focuses on product-driven control (PDC) that embeds decisional and adaptation capabilities within the product. PDC can be defined in a static or dynamic way: in the first case, all switchable manufacturing trajectories are predefined and implemented in the product control while, in the second case, PDC can be seen as a non-deterministic and "on the fly" choice among control trajectories to fit with the manufacturing system availability and the product state. In this last case, PDC safety is ensured thanks to a filtering approach that enables to maintain PDC within a state space that satisfy functional and safety constraints whatever the control generated by the reconfiguration process is. This paper focuses on the definition and verification of a minimal set of constraints that ensure the sufficiency and the non blocking properties of the constraints. A case study illustrates the approach.

Keywords: product driven control,model checking,reconfigurable manufacturing system

Identifier: 10.3182/20090610-3-IT-4004.00052

Conference: 2nd IFAC Workshop on Dependable Control of Discrete Systems (2009)

Location: École Normale Supérieure de Cachan, Italy

Start Date: Wed Jun 10 2009 - End Date: Fri Jun 12 2009

Authors: Saboori, Anooshiravan; Hadjicostis, Christoforos N.

Abstract: In this paper, we formulate, analyze, and devise methodologies to verify the notion of infinite-step opacity in discrete event systems that are modeled as (possibly non-deterministic) finite automata with partial observation on their transitions. Specifically, a system is infinite-step opaque if the entrance of the system state at any particular instant to a set of secret states remains opaque (uncertain), for the length of the system operation, to an intruder who observes system activity through some projection map. In other words, based on observations through this map (and complete knowledge of the system model), the intruder can never be certain (and will never be certain) that the system state at any point in time evolves (or has evolved) to the set of secret states. We show that infinite-step opacity can be verified via the construction of a set of appropriate state estimators. We also establish that the verification of infinite-step opacity is a PSPACE-hard problem.

Keywords: discrete event systems,system security,information flow,finite automata,state estimation

Identifier: 10.3182/20090610-3-IT-4004.00013

Conference: 2nd IFAC Workshop on Dependable Control of Discrete Systems (2009)

Location: École Normale Supérieure de Cachan, Italy

Start Date: Wed Jun 10 2009 - End Date: Fri Jun 12 2009

Authors: Wu, Naiqi; Zhou, MengChu

Abstract: With wafer residency time constraints, wafer sojourn time in a processing module should be carefully controlled such that it is in a permissive range. Activity time variation often results in wafer sojourn time fluctuation and makes an originally feasible schedule infeasible. Thus, it is very important to know how the wafer sojourn time changes when activity time varies. With proposed Petri net (PN) model and real-time control policy, this paper analyzes the effect of activity time variation on wafer sojourn time delay and presents its upper bounds in dual-arm cluster tools.

Keywords: Petri net,cluster tool,scheduling,automated manufacturing systems

Identifier: 10.3182/20090610-3-IT-4004.00007

Conference: 2nd IFAC Workshop on Dependable Control of Discrete Systems (2009)

Location: École Normale Supérieure de Cachan, Italy

Start Date: Wed Jun 10 2009 - End Date: Fri Jun 12 2009