Authors: None

Abstract:

Keywords:

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.90001

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

Page Numbers: ---

Authors: Zhou, MengChu

Abstract: Cluster tools provide a flexible, reconfigurable, and efficient environment for semiconductor manufacturing. They become difficult to operate because of residency time constraints and process time variation. This talk addresses their real-time scheduling and control issues. A generic Petri net model is developed to model them. It describes the robot activity sequence with robot waits included. Hence, to operate a cluster tool is to determine robot wait times. A two-level operational architecture is proposed and discussed. It includes an off-line periodic scheduler and real-time controller. This proposed approach allows a cluster tool to adapt to activity time variation while operate at its highest throughput at the steady-state.

Keywords:

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00003

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

Page Numbers: 1-1

Authors: Flammini, Francesco

Abstract: In order to master the increasing complexity of modern railway control systems, novel model-based approaches are needed to allow engineers to evaluate such systems against strict system-level dependability requirements. In this talk, we provide an overview of the experience of Ansaldo STS in using model-based approaches for railway safety, reliability and security. Dependability requires assessment both at the software and at the hardware levels. At the software level, models have proven useful to support both static and dynamic functional analyses in order to discover systematic faults in the code. At the hardware level, we have experimented that compositional multi-formalism modeling approaches well suit the evaluation of system safety and reliability against random faults. The use of models has allowed engineers to improve both the effectiveness and the efficiency of system verification. Views of the Unified Modeling Language have been adopted to perform informal or semi-formal analyses, while Stochastic Petri Nets, (Repairable) Fault Trees, Continuous Time Markov Chains and Bayesian Networks have been employed for formal and quantitative analyses. Analytical risk and vulnerability models have also been experimented for security assessment with respect to intentional threats and natural hazards. Due to the wide range of possible applications, we are currently studying in depth both the theoretical and the technological issues related to the multi-paradigm dependability modeling using appropriate frameworks.

Keywords:

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00004

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

Page Numbers: 2-2

Authors: Reif, Wolfgang

Abstract: In safety critical applications, the growing complexity and risk associated with embedded software intensive systems demands for reliable safety assessments. Additionally, in many application areas standards and norms require the usage of model based techniques to guarantee the quality of safety critical systems. Model based safety analysis is a formally grounded approach to compute reliable safety properties from system models. In this context the term safety covers functional correctness, failure tolerance, safety optimisation as well as balancing antagonistic safety concerns. The analysis has both qualitative and quantitative aspects. Systems under consideration are discrete reactive systems. An extension also applies to self-organising systems. The talk presents the approach as well as some interesting applications.

Keywords:

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00005

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

Page Numbers: 3-3

Authors: Liu, Ding; Li, Zhiwu; Zhou, Mengchu

Abstract: Most existing prevention methods tackle the deadlock issue arising in flexible manufacturing systems modeled with Petri nets by adding monitors and arcs. Instead, this paper presents a new deadlock prevention method based on a characteristic structure of WS3PR, an extension of System of Simple Sequential of Processes with Resources (S3PR) with weighted arcs. The numerical relationships among weights, and between weights and initial markings are investigated based on simple circuits of resource places, which are the simplest structure of circular wait, rather than siphons. A WS3PR satisfying a proposed restriction is inherently deadlock-free and live by conffiguring its initial markings. A set of polynomial algorithms are developed to implement the proposed method. Several examples are used to illustrate them.

Keywords: flexible manufacturing system (FMS),Petri nets,deadlock prevention,polynomial algorithms,circular wait,simple circuit

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00006

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

Page Numbers: 4-9

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

Digital Object Identifier (DOI): 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

Page Numbers: 10-15

Authors: Schmidt, Klaus; Cury, José E. R.

Abstract: This paper addresses the control of multitasking DES that allow for dealing with liveness properties in the case where multiple classes of tasks have to be independently completed by the system. Colored marking generators (CMG) have been previously introduced as a model to consider multitasking control. The computational cost of the supervisor synthesis for multitasking DES grows with the number of classes of tasks. In this paper we investigate conditions under which removing tasks of the DES model does not affect the result of supervisory control in the sense that their completion is guaranteed as a consequence of the completion of the other tasks in the DES model. Conditions are derived under which tasks of a class or a set of classes can be removed from the model, and the results are extended to the case of abstracted models in a hierarchical and decentralized control architecture. Those conditions, which can be verified in polynomial time, are stated as properties of strongly connected components of the automata models in different levels of the control hierarchy. The results of the paper are illustrated by a manufacturing system example, showing the potential gains of the approach.

Keywords: discrete-event systems,hierarchical systems,multitasking supervisory control

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00008

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

Page Numbers: 16-21

Authors: Hicheur, Awatef; Barkaoui, Kamel; Boucheneb, Hanifa

Abstract: When dealing with workflow security requirements, the compliance of information flow with the adopted security policies needs to be analyzed. For this purpose, we adopt in this paper a two-step verification approach. While the first step is concerned by the verification of the soundness of the workflow, the second one is concerned by the control of access rights on information under both time constraints and security requirements (through multilevel security policies such as Bell-LaPadula). We propose a model for such workflow specification based on the Time ECATNet formalism. This latter offers means to incorporate the security and time constraints on information flow into an initial WF-net modeling the control flow of a workflow specification. We then show how to analyze the impact of the introduced security rules on the workflow execution, using the Maude LTL model checker, and show how to relax them to derive a correct workflow specification.

Keywords: workflow,data flow,mandatory access control,multilevel security,time constraints,ECATNet

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00009

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

Page Numbers: 22-27

Authors: Schlich, Bastian; Brauer, Jörg; Wernerus, Jörg; Kowalewski, Stefan

Abstract: While there are several approaches applying model checking to PLC programs, it is still not used in industry. This is due to the limited applicability of the existing approaches, which all translate PLC programs into the input languages of existing model checkers and thus suffer from certain problems. This paper presents a new approach that applies model checking directly to PLC programs written in IL without using translations. This has some advantages: domain-specific information is available during verification, users can make propositions about all features of the PLC, and counterexamples are given in the same language as the program, thus, simplifying the process of locating errors. In the described approach, a tailored simulator builds the state space for verification. Within this simulator, different abstraction techniques are used to tackle the state-explosion problem. A case study shows the applicability of this approach.

Keywords: programmable logic controllers,instruction list programs,formal verification,model checking

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00010

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

Page Numbers: 28-33

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

Digital Object Identifier (DOI): 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

Page Numbers: 34-39

Authors: Fischer, S.; Lohmann, S.; Engell, S.

Abstract: A structured and meaningful data format serves as a neutral representation that can be used to generate different visualizations from a mutual data pool. The structured data in this paper is stored as extensible markup language and used to generate the following data formats: a cause & effect matrix, a control program as function block diagram and a set of finite state automata. These tasks are crucial, especially in the context of highly dependable systems. Each data format is used for different tasks during the life cycle of a logic control program, which are typically: migration, (re-)documentation and analysis. This paper provides a model solution to each task and draws conclusions on their interrelation and use.

Keywords: logic design,industrial control,safety-critical,automata,formal verification

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00012

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

Page Numbers: 40-45

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

Digital Object Identifier (DOI): 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

Page Numbers: 46-51

Authors: Cabasino, Maria Paola; Giua, Alessandro; Seatzu, Carla

Abstract: In this paper we provide an approach to on-line diagnosis of discrete event systems based on labeled Petri nets. The proposed procedure is based on our previous results on unlabeled Petri nets and allows us to also consider events that are undistinguishable, namely events that produce an output signal that is observable, but that is common to other events. Our approach is based on the notion of basis markings and j-vectors and it is shown that, in the case of bounded Petri nets, the most burdensome part of the procedure may be moved off-line, computing a particular graph that we call Basis Reachability Graph.

Keywords: fault diagnosis,discrete event systems,Petri nets,labeled Petri nets

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00014

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

Page Numbers: 52-57

Authors: Pazzi, Luca; Pradelli, Marco

Abstract: The paper examines current trends in autonomic space software systems and proposes the adoption of a hierarchical state based formalism which allows the different paradigms employed in the field to meet seamlessly. It is not clear, for example, how goal-based on-board autonomy, originally conceived for deductive-flavored systems which may not be ground controlled for indefinite portions of time, be able to combine with model based engineering, which best fits current industrial design strategies. Other aspects, such as closed loop discrete control and fault tolerance do not easily lend themselves to modularity. The paper shows that, by employing the proposed formalism, goals can be decomposed and distributed in a very natural way among different modules. Each module is, at the same time, both a controller and a controllable part of the whole system, allowing to partition the closed loop control flow at different levels of complexity. Formal verification is also possible by employing goals as state based constraint in the implementation phase.

Keywords: device degradation,dependable systems,part-whole statecharts,goal-based approach,reusable subsystems,constraint-based control,model-based

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00015

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

Page Numbers: 58-62

Authors: Ghaze, Mohamed; Masmoudi, Malek; Toguyeni, Armand

Abstract: Works in the field of verification systems have shown the critical importance of time. The nonsatisfaction of time may have important consequences for both security and performance points of view. For automated systems with level of security, the verification of time requirements is an essential part of the process validation system. In this paper, we are laying the foundations for a new and systematic approach for the verification of discrete event systems with time constraints. The contribution of this approach is threefold: first, unlike existing approaches, it allows for the verification of several requirements at once. Therefore, the approach is generic because we focus on developing mechanisms that take into account different types of requirements rather than the system to be verified. Finally, the implementation of the approach is almost as systematic because the verification tools we are developing are based on the instantiation of patterns. These patterns are designed on the basis of a classification of temporal requirements that we have established. The concepts of parallelism and hierarchy which characterize the Stocharts formalism compared to other state-transitions models help us build the foundations of our approach. An example of application to the control-command in the railway field is presented to illustrate the key concepts of our approach and its implementation.

Keywords: monitoring,complex systems,temporal requirements,observers,UML,Stocharts,railway control

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00016

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

Page Numbers: 63-68

Authors: Philippot, A.; Sayed-Mouchaweh, M.; Carré-Ménétrier, V.

Abstract: This paper presents a discrete event model-based approach for Fault Detection and Isolation of manufacturing systems. This approach considers a system as a set of independent plant elements. Each plant element is composed of a set of interrelated Parts of Plant (PoPs) modeled by a Moore automaton. Each PoP model is only aware of its local behavior. The degraded and faulty behaviors are added to each PoP model in order to obtain extended PoP ones. An extrapolation of Gaussian learning is realized to obtain acceptable temporal intervals between the time occurrences of correlated events. Finally based on the PoP extended models and the links between them, a fault candidates' tree is established for each plant element. This candidates' tree corresponds to a local on-line fault event occurrence observer, called diagnoser. Thus, the diagnosis decision is distributed on each plant element. An application example is used to illustrate the approach.

Keywords: discrete-event systems,decentralised/distributed models,diagnosis,automata,manufacturing systems

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00017

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

Page Numbers: 69-74

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

Digital Object Identifier (DOI): 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

Page Numbers: 75-80

Authors: Schmidt, Klaus

Abstract: In our previous work, a communication protocol for the reliable communication of discrete event supervisors that are implemented on physically distinct controller devices on a shared-medium network was developed. Here, the required data exchange is captured by communication models that are algorithmically computed from an underlying hierarchical and decentralized supervisor synthesis. These communication models are particularly efficient if all synthesized supervisors are implemented on distinct controller devices. In this paper, the general case is considered, where multiple supervisors can be aggregated on each controller device. To this end, the algorithmic communication model computation is adapted in order to remove communication among supervisors on the same controller device. The benefit of the controller aggregation is illustrated by a manufacturing system case study.

Keywords: hierarchical discrete-event systems,distributed control,shared-medium networks

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00019

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

Page Numbers: 81-86

Authors: Komenda, Jan; Lahaye, Sébastien; Boimond, Jean-Louis

Abstract: Controllability of (max,+) automata and formal power series is studied within a behavioral framework. An extension of classical tensor product of their linear representations as a parallel composition of controller with the plant (max,+) automaton is used. Controllability is studied using residuation theory of (multivariable) formal power series and (max,+)-counterpats of supremal controllable behaviors are derived.

Keywords: controllability,(max,+) automata,(max,+) formal power series,Hadamard product

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00020

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

Page Numbers: 87-92

Authors: Brunsch, T.; Raisch, J.

Abstract: In this paper, we present a max-plus algebraic model for cyclically operated highthroughput screening plants. A max-plus algebraic representation of the system, derived directly from a discrete-event systems model of the predetermined globally optimal solution, contains negative order arcs, forcing certain events in previous cycles to occur after events in the current cycle. With respect to the cycle index, though of course not in terms of time, the model is acausal. However, the model can be transformed into a system representation without negative order arcs. The obtained max-plus algebraic model can then be applied as a controller to handle unexpected deviations from the predetermined cyclic operation during runtime.

Keywords: cyclic systems,discrete-event systems,max-plus algebra,high-throughput screening

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00021

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

Page Numbers: 93-98

Authors: Dotoli, Mariagrazia; Fanti, Maria Pia; Mangini, Agostino M.; Ukovich, Walter

Abstract: The paper addresses the problem of the on-line identification of Petri Nets (PN) modelling the unobservable behaviour of Discrete Event Systems (DES). Starting from a previous specification of an identifier that monitors the DES events and the corresponding available place markings, the paper proves some results that make the on-line identification of reasonable complexity. Assuming that the PN system modelling the observable events is known, at each event occurrence an identification algorithm recursively updates and provides as an output the complete PN system describing both the observable and unobservable DES behaviour. An example shows an application of the proposed technique.

Keywords: discrete event systems,Petri nets,identification algorithms,integer programming,modelling

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00022

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

Page Numbers: 99-104

Authors: Lunze, Jan

Abstract: The paper deals with the determination of input sequences for which the faults occurring in discrete-event systems described by deterministic I/O automata can be detected and identified. The basis for this method is provided by diagnosability criteria that show that faults can be found whenever the automata describing the faultless and the faulty system do not have equivalent initial states. The absence of equivalent states implies that there exist finite input sequences for which the output sequences distinguish for all faults. The paper describes a method to find these input sequences.

Keywords: fault diagnosis,discrete-event system,diagnosability,automata,equivalence

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00023

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

Page Numbers: 105-110

Authors: Basile, F.; Chiacchio, P.; De Tommasi, G.

Abstract: The fault diagnosis in Petri net systems is usually performed by using a compiled diagnoser, which is a system built offline but usually having a big state space. In this paper it is shown that under certain assumptions two vectors, whose value is updated online after each observed event, can be used to develop an interpreted diagnoser, which is an algorithm based on mathematical programming to be executed online. In particular the first vector records the observations, while the second stores observations not enabled under the actual net marking. The proposed algorithm is able to distinguish between "a fault has occurred for sure" and "a fault has not occurred".

Keywords: Petri nets,fault diagnosis

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00024

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

Page Numbers: 111-116

Authors: Merle, Guillaume; Roussel, Jean-Marc; Lesage, Jean-Jacques; Bobbio, Andrea

Abstract: This paper focuses on a subclass of Dynamic Fault Trees (DFTs), called Priority Dynamic Fault Trees (PDFTs), containing only static gates and Priority Dynamic Gates (PAND and FDEP) for which a priority relation among the input nodes completely determines the output behavior. We define events as temporal variables and we show that, by adding to the usual Boolean operators new temporal operators denoted BEFORE and SIMULTANEOUS, it is possible to derive the structure function of the Top Event with any cascade of Priority Dynamic Gates and repetition of basic events. A set of theorems are provided to express the structure function in a sum-of-product canonical form. We finally show through an example that the canonical form can be exploited in order to determine directly and algebraically the failure probability of the Top Event of the PDFT without resorting to the corresponding Markov model. The advantage of this approach is that it provides a complete qualitative description of the system and that any failure distribution can be accommodated.

Keywords: dynamic fault tree,algebraic approach,qualitative analysis,quantitative analysis

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00025

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

Page Numbers: 117-122

Authors: Changey, S.; Pecheur, E.; Wey, P.

Abstract: The goal of ISL's project GSP (Guided Supersonic Projectile) is to change the flight path of an air-defence projectile in order to correct the aim error due to the target manoeuvres. The originality of the concept is based on pyrotechnical actuators and onboard sensors which control the angular motion of the projectile. First of all, the control of the actuators requires the precise control of the roll angle of the projectile. To estimate the roll angle of the projectile, two magnetometers are embedded in the projectile to measure the projection of the earth magnetic field along radials axes of the projectiles. Then, an extended Kalman filter is used to compute the roll angle estimation. As the rolling frequency of the GSP is about 22 Hz, it is easy to test the navigation algorithm in laboratory. Two magnetometers and a LED are rotated using an electrical engine; then an electronic station based on a DSP runs an extended Kalman filter and runs a guidance algorithm to compute the trigger times of the LED. By using a high speed camera, we can observe and improve the accuracy of the method.

Keywords: extended Kalman filters,estimation algorithms,real-time systems,guidance systems,navigation systems,embedded systems,angular position,automated guided vehicles

Digital Object Identifier (DOI): 10.3182/20090610-3-IT-4004.00026

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

Page Numbers: 123-127