Project topics and materials
Get Complete Project Material File(s) Now! »
Safe design of hardware embedded systems based on COTS : State of the art
Introduction
This chapter assembles the background for the main axes of our work. It recalls the models and tools for the safe design of finite-state Discrete Event Systems (DES). Then, we sneak inside the box of a hardware embedded system and explain the discrete time behavior of such systems and the functional requirements needed to be taken in consideration during the design process. Then, we recall three among the most widespread design tools used for verifying the correctness of a design: (1) the theorem proving, (2) the guided simulation and (3) the model checking technique. The later is explicitly used in our contribution. Then we announce how our contribution can fill the gaps of those methods. After that, we tackle the issue of enforcing by Discrete controller synthesis approach (DCS) functional requirements. Then, we present the state of the art for the component-based method for hardware design.
Modeling hardware systems
The embedded systems’ design relies on the formal modeling of the dynamic behaviors. Several modeling techniques exist, and they differ according to their underlying formal model and their implementation technique. The formal language theory is the underlying framework formaliz-ing event-driven systems. In this framework, sequences of events are fundamental in modeling the dynamic behavior of the system and its functional requirements. On the other hand, sample-driven systems are inspired from electronic design techniques. Their behavior is expressed as sequences of system’s states, and functional requirements always refer to subsets of states, either desired or forbidden.
There exists a conceptual difference between the behavioral dynamics of event-driven on the one hand and sample-driven models on the other hand. Both are able to model reactivity. How-ever, event-driven models react upon an event, whenever it occurs, which is also known as an “event-driven” reaction. Sample-driven modeling assumes the existence of one special kind of events, generated by a clock. Whenever a clock event occurs, the inputs and the current state are sampled before reacting. Such systems run by the events generated by an external clock are also known as Sample-driven systems.
Such a variety of design models and techniques calls for a preliminary choice. In this work, DCS application is intended for hardware design. Besides, hardware systems are designed using Boolean synchronous finite state machines, which are sample-driven models. Thus, the most adequate modeling paradigm is the best suited for this work. This choice is detailed in the sequel.
Even though specific formal techniques have been developed on top of both event-driven and sample-driven models, we wish to highlight the fact that our results can be applied to both sample and event-driven models, through a simple transformation of event-driven into sample-driven models.
Event-driven modeling
Event-driven models consider the behavior of a discrete event system as a set of (possibly in-finite) sequences of events. The system has an initial state and evolves according to the events that arrive. An event can occur and cause a system pass from its current state to the next state. Only one event can occur at a time. The event-driven modeling of discrete event system is based on the theory of formal languages developed in [18] and presented extensively in [19].
Formal language
Definition 1.1 (Formal language). Consider the following items:
An alphabet is a set of possible events of a DES, denoted as ; A word is a sequence of events from An empty word is denoted « ;
j j denotes the cardinality of ;
denotes all the possible finite sequences of events from ;
A formal language defined over an event set is a subset of .
Example 1.1. Given the alphabet = {a,b,c}.
a, ab, abc, abb, bcc are words over the alphabet;
L = f »; a; ab; abb; bccg is a language over the alphabet.
Regular languages are an interesting particular class of formal languages. They are able to rep-resent dynamic behaviors as sets of words where some subsets of these words can be expressed as regular expressions. Regular expressions over a finite alphabet describe sets of strings by using particular operations such as: grouping, alternate expression, symbol concatenation and cardinality. A relation of bijection exist between regular languages and event-driven finite state machines: i,e. every regular language could be generated by a finite state machine and vice versa. This fact allows the designers to model the dynamics of a system following two distinct ways.
Definition 1.2 (Event-driven Finite state machine). An event-driven finite state machine (FSM) is a 5-tuple: M = hq0; ; ; Q; Qmi (1.1)
where:
q0 is the initial state;
is the set of events, is an event where 2 ;
: Q f g ! Q is the transition function, through which the system changes its current state;
Q is the set of states, i.e; the state space;
Qm is the set of desired states to be reached.
Notice. The desired states Qm are those which represent an achievement of a mission, such as the end of a task. This mechanism is not used in our work. As explained in the sequel, desired states are pointed out through formal specifications. Thus, in the sequel, when Qm is not mentioned explicitely this means Qm = ;.
Common notions in event-driven modeling
Execution path: A sequence of visited states (q0q1q2:::). Noticing that a sequence is or-dered set.
Reachable state: a state (q) is called reachable if it is possibly visited starting from the initial state q0 if there exist an execution path leading to it.
Next state: given a current state (q) the next state (q0) is the state visited when an event 2 occurs. We can denote: (q f g ! q0)
Marked state: a state qm is a marked state, which represents a state that must be visited, starting from the initial state, i.e., there must be an execution path, which leads to this state.
The notion of reachable and marked states helps designers of discrete event systems to represent some required, inadmissible and possibly reached behavior of a system. A familiar example that we can find in our everyday life is microwave machine; the designer of a the control part of the microwave system can define a list of marked states that should be visited through the system life cycle like the “finished state”.
Thus, the state marking adds a requirement expression mechanism to the event-driven FSM. In this work however, requirements are dissociated from the dynamic FSM model, and expressed separately. This choice is not fundamental, it is only based on the current practice in hardware design engineering. Thus, in the sequel, all the models we manipulate have Qm = ;.
For a given system, modeled by an event-driven FSM, The event-driven execution mechanism can be expressed by the following algorithm [20]:
Algorithm.1 Algorithmic description of the Event-driven paradigm
1: current state: q 2 Q
2: next state: q0 2 Q
3: initialization: let q = q0
4: Begin loop
5: wait for an event 2
6: compute the reaction (next state computation): let q0 = (q; )
7: finalize the transition: let q = q0
8: End loop
The main restriction that applies when using event driven modeling to model hardware systems is the fact that it supposes that only one event can occur at a time, which is inadequate with the concurrent nature of a physical environment. Besides, hardware systems are inherently concurrent. They are made of building blocks that run in parallel and possibly communicate with each other. Building a global finite state machine model which represents the simultaneous behavior of all considered individual finite state machines is known as a parallel composition. More specif-ically, we focus on the broadcast composition. This notion is looser, because it does not add blocking phenomena to the composition. It is also conceptually close to the synchronous prod-uct [21] which is widely used in hardware design. The broadcast compositon requires the defi-nition of the active event set for a given state.
Sample-driven modeling
Sample-driven models handle values, instead of events. The main difference comes from the abstraction level between these two notions. Events are considered abstract modeling artifacts, and one possible implementation of an event synchronization mechanism is the continuous sam-pling of a value. Sampling requires a clock, and a sampling frequency. In the sample-driven modeling there exist only one event which is a hardware clock tick. At each clock tick, all system’s inputs are sampled and their values are read and all transitions are triggered. The next state is calculated with respect to the current state and the values read from the environment. An implicit transition is modeled if no change of state is needed regarding the input sampling as shown in figure 1.5. The actual clock frequency remains abstract and remains to be subsequently determined at a physical implementation step. It is assumed, and this assumption remains to be physically validated, that the clock frequency is sufficient for an accurate observation of the environment dynamics.
Definition 1.6 (Sample-driven finite state machine). A sample-driven model of a discrete event system can be presented as a FSM of a 4-tuple hq0; X; ; Q; Qmi where:
q0 is the initial state;
X is set of Boolean input variables;
Q is set of states, represented by state variables; is the transition function: : Q Bjxj.
The behavior of a discrete-event system modeled by a sample-driven finite state machine can be expressed by the algorithm [20]
Algorithm 2: algorithmic description of the Sample-driven paradigm
1: initialization: i = 0; qi = q0
2: forever, at each clock tick i do
3: read input variables xi
4: calculate the next state: qi+1 = (qi; xi)
5: update state q = q0
6: end
Translating event-driven into sample-driven models
We use in the following the common notation for the classical Boolean operators, such as : “ ^ ” for the logical “and”, “ _ ” for the logical “or”, :a for the logical negation of a, “!” for the logical implication and “,” for the Boolean equivalence. To simplify the figures we use “ : ” instead of “ ^ ”
In this work we focus on hardware systems, which are modeled using sample-driven finite state machines. However, we argue that the results presented in the sequel can also apply to event-driven models. These can be systematically translated into sample-driven representations [23]. The transformation method we consider, between an event-driven model into a sample-driven model, is quite straightforward, and simply recalled here.
As the machine receives j j = 4 events, then, log2(4) = 2, two Boolean variables are needed and sufficient to encode the events and translate them into Boolean input variables. Let X = fx; yg. Let enc( ) be an encoding function computing values for the vector (x,y) and defined as: enc(e1) = (1; 1);
enc(e2) = (0; 1);
enc(e3) = (0; 0);
enc(e4) = (1; 0)
The translation of M from event-driven into a sample-driven model MT is illustrated in figure 1.6 (a) and (b) respectively. All the remaining combinations of (x) and (y) not corresponding to e1 : : : e4 are self-loop transitions in MT , left unrepresented for more clear readability of the figure. Through application of enc 1 they would fall into the abs event labeling a supplementary self-loop transition. Notice that the inverse process of building an event-driven model from a sample-driven one through enc 1 does not necessarily yield the initial event-driven model. This happens because enc is not bijective; it is forced in that sense through the addition of the abs event, whose presence is not natural in an event-driven model.
Table of contents :
Introduction
1 Safe design of hardware embedded systems based on COTS : State of the art
1.1 Introduction
1.2 Modeling hardware systems
1.2.1 Event-driven modeling
1.2.1.1 Formal language
Notice
1.2.1.2 Common notions in event-driven modeling
1.2.2 Sample-driven modeling
1.2.2.1 Translating event-driven into sample-driven models
1.2.2.2 Modeling interaction
1.2.3 Synchronous product with interaction
1.2.4 Efficient manipulation of symbolic models
1.3 Behavior requirements specification
1.3.1 Logic specifications
1.3.1.1 Linear-time temporal logic (LTL)
1.3.1.2 Computation tree logic (CTL)
1.3.2 Operational specifications
1.3.3 The Property Specification Language (PSL) standard
1.4 Verification of hardware embedded systems
1.4.1 Theorem proving
1.4.2 Guided simulation
1.4.3 Model checking
1.5 Supervisor synthesis
1.5.1 Supervisory control
1.5.2 Controllability in hardware systems
1.5.3 Symbolic supervisor synthesis
1.5.4 DCS for hardware designs
1.6 COTS-based design
1.6.1 COTS definitions
1.6.2 COTS integration in a design process, difficulties and solutions
1.6.3 Safety preserving formal COTS composition
1.6.4 Safety in component-based development
1.7 Conclusion
2 The COTS-based design method
2.1 Introduction
2.2 Building COTS-based control-command systems
2.2.1 Stand-alone COTS
The need for environment assumptions
2.2.2 COTS assembly
Structural assessment of COTS interconnections
2.2.3 Compositional reasoning
Incompatibility between environment assumptions
Contradiction between guarantees and environment assumptions
Compatibility between guarantees and environment assumptions
Cyclic reasoning
2.2.4 Adding context-specific requirements
2.2.5 Design errors
2.2.6 Global design error
2.2.7 Enforcing local/global properties
2.2.7.1 Computing the controllable input set
2.2.7.2 Environment-aware DCS
2.2.7.3 Environment modeling
2.2.7.4 The environment aware DCS algorithm
2.2.7.5 Applying EDCS to COTS-based designs
Specific terminology for a EDCS-corrected COTS: Glue and
Patch controllers
2.2.8 Implementing the control loop
The general control loop
Controllable inputs with hard reactive constraints
Controllable inputs with soft reactive constraints
2.2.9 The “event invention” phenomenon
2.2.10 Detection of “event inventions”
2.3 The safe COTS-based design method
Step 1: Modeling
Step 2: Automatic error detection
Step 3: Automatic error correction
Step 4: Formal verification
Step 5: Simulation
2.4 Running example : the generalized buffer design
The GenBuf functional behavior
2.5 Step 1. Modeling
2.5.1 From text to formal requirement expressions
2.5.2 Example: modeling components of the GenBuf design
2.5.3 Exemple : writing global properties for the GenBuf design
2.6 Step 2. Automatic error detection
2.6.1 Local verification of local properties
2.6.2 Global verification of local properties
2.6.3 Global verification of global properties
2.7 Step 3. Automatic error correction
2.7.1 Automatic synthesis of a correcting controller
2.8 Step 4. Verification of the corrected/controlled system
The guarantee is a safety property with no assumptions
The guarantee is a safety property relying on assumptions
2.9 Step 5. Simulation
2.10 Conclusion
3 Application on an industrial system
3.1 Introduction
3.2 FerroCOTS: Presentation and Goal
3.3 The Passengers Access System
3.3.1 Design objectives
3.3.2 Structural description of the available COTS
3.3.3 Behavioral description of the COTS assembly
3.3.4 Modeling and formal specification
3.3.4.1 The stand-alone door component
3.3.4.2 Stand-alone filling-gap component
3.3.4.3 The Door / Filling-gap assembly
3.3.4.4 Functional requirements of the door – filling-gap assembly
3.3.5 Error detection
3.3.6 Error correction
3.3.6.1 Controllable variables
3.3.6.2 Correcting controller generation
Overview of the generated controller
3.3.7 Verification of controlled passenger access system
3.3.8 Simulation
3.4 Comparison: assembly controlled synthesis vs. the initial assembly
3.5 Implementation
3.6 Conclusion
A Cahier des charges fonctionnel Système d’accès voyageurs
1 Le système accès voyageur
2 Choix techniques et interfaces fonctionnelles
2.1 Porte
2.2 Emmarchement mobile
2.3 Cabine/train
B Notation table
Bibliography
