Project Topics
Get Complete Project Material File(s) Now! »
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.
Events can be translated to vectors of values, one vector per event. Thus, each event is mapped to a unique Boolean encoded value according to a function: enc : ! Blog2(j j) (1.11).
Synchronous product with interaction
When finite state machines work concurrently and interact, a synchronous product of the two machines M1jjM2 is calculated under the assumption that the outputs of the product are uniquely assigned by either M1 or M2.
Interacting FSMs are composed according to the synchronous paradigm defined in [21]. This operation requires a preliminary input/output mapping, usually performed by the design engi- neer Let Mi; i = 1; 2 be two communicating finite state machines, where Mi = hq0i; Xi; Qi; i; P ROPi; ii. The set of inputs Xi of Mi is divided into 2 disjoint subsets : Xi = Li[Ii. The machines M1; M2 communicate through P ropout1; P ropout2 where P ropout1 P ROP1 is a subset of Boolean propositions which connects M1 to M2 via L2 and P ropout2 P ROP2, is a subset which connects M2 to M1 via L1. This interconnection is illustrated in figure 1.9 The synchronous product M1jjM2 is represented as: M1jjM2 = h(q01; q02); X12; 12; Q12; P ROP12; 12i (1.17).
Efficient manipulation of symbolic models
Binary Decision Diagrams, that we abbreviate BDDs [24] have shown their efficiency in manip-ulating Boolean expressions. They have been successfully used for efficient FSM representation and state exploration [16, 25, 26]. A BDD represents a Boolean expression as a direct acyclic graph, having two terminal nodes: true (1) and false (0). Their key advantage is the ability to provide a compact and canonic representation of a Boolean expression. Thus, constructing a BDD implicitly assess the satisfiability of the Boolean expression which is represented: a tau-tology is always represented by the terminal node (1), and a contradiction by the terminal node (0). Besides, all Boolean operations have a corresponding efficient BDD implementation.
For a given Boolean expression defined over a set of Boolean variables, building a BDD in-volves choosing an a priori total variable order. The key measure of BDD efficiency is the size of a BDD: the number of graph nodes required to build the diagram. The theoretical spatial complexity of a BDD is exponential in the number of Boolean variables contained.
The size of a BDD strongly depends on the initially chosen variable ordering. In practice, “good” variable orders can often be found, but unfortunately there is no tractable way to com-pute the best variable ordering. However, BDD packages implement interesting heuristic tech-niques for handling variable orderings dynamically yielding fairly good performance. Besides, for some known Boolean expressions, good variable orderings simply do not exist.
BDD-based formal techniques have reached their limits in terms of performance this is why most industrial and research efforts focus on the synergy between several techniques. Thus, BDDs are combined with SAT-based approaches (Satisfiability formal verification) [27] in or-der make the handling of large systems more tractable. Given a propositional formula ’, the Boolean Satisfiability problem posed on ’ is to determine whether there exists a variable assign-ment under which ’ evaluates to true in certain part of the total state space. If such assignment exists the ’ is called satisfiable. Otherwise ’ is said to be unsatisfiable.
In this work, an important part of our results rely on the symbolic Discrete Controller Synthesis technique, with a BDD-based implementation.
Behavior requirements specification
Modeling the behavior of hardware systems is usually achieved using hardware description languages like VHDL [28] and Verilog [29] or even system-level languages such as SystemC [30]. These are standard (IEEE) languages; they are dedicated for embedded hardware modeling and can be exploited by design tools for simulation, hardware synthesis, or formal verification. However, any design process is a part of a more complex design flow, starting with requirement specifications. This process starts with functional requirements asserted informally (natural lan-guage). These requirements are first formalized, and then progressively refined, using UML or SysML. Through such a process, a functional architecture (system-level) is refined into an or-ganic architecture, and functional requirements are progressively mapped to behavioral require-ments. These relate to the sequential behavior of a component, modeled as a communicating Boolean finite-state machine. Such requirements can be expressed formally either logically, using propositional and/or temporal logic, or operationally, by describing the desired behavior as a program.
COTS integration in a design process, difficulties and solutions
The lack of formal specification of pre-built components behavior was an obstacle against using COTS in critical systems, thus, a formal definition of COTS interface was proposed in 1999 [76]. Formalizing contracts over the COTS interface isolates the system under construction of the COTS internal software and makes the interaction between the original system and the integrated COTS verified and controlled through the interface contracts.
In 2005 A formal definition of Component-based embedded system was proposed in [2]. A communication level specification of components, based on extended finite state machines (EFSM), was used. The studied embedded system is divided into three sorts of communicating blocks (1) sensors, (2) a controller and (3) actuators as shown in figure 1.15. Components are connected by communication points, i.e., inputs and outputs. sensor’s outputs are input events for the controller, the controller’s outputs are the inputs of the actuators. The system components are black boxes specified and tested using formal description technique, Estelle [77], [78]. The specification approach reuses an already existing methods to formally define embedded systems and profits of methods like automatic analysis, test data generation, validation and formal fault models, to enhance the components based development and follow the growing complexity of embedded system requirements especially safety and real-time properties.
Using COTS in a design, although it facilitates the cost of initializing a system design, it raises the risk of component maintenance, since the original developer may not be available for check-ing the components. If the vendor is not capable to keep up with the customer problems or prod-uct bugs, or even the shop is closed or stopped producing such COTS, negative consequences will affect the customer design and extra unexpected expenses will be needed for any system upgrading. Thus, maintenance costs increases exponentially when integrating COTS inside the design, [79]. Thus, researchers worked to provide some heuristics in order to balance between the use of COTS in a design and the negative consequences of such use [79], [80].
Safety preserving formal COTS composition
Formal representation of components’ composition has been evoked in the literature of software engineering of embedded systems. In [81], [82] a formal method for developing trustworthy real-time reactive systems is proposed. The system components are a set of communicating tasks modeled as communication finite state machines, and the system’s trustworthy is evaluated by the system’s preservation of some formal safety and security properties. The model checking is used to verify these properties over the studied system.
In [83] software components are modeled as communicating finite state machines and the safe communications are represented by LTL assertions. Informal lexical compatibility study is made over the components to conclude the system’s safety represented by compatible compo-nents. In [84] a monitoring data flow service is proposed to supervise the communication between some tasks modeled as FSMs. The system is composed by a synchronous product of the tasks FSMs, and the service can detect any unexpected communication over the system and signalize it as an error. Monitors are automatically generated using a particular tool named (Enforcer).
Building COTS-based control-command systems
In this work, the notion of COTS is mainly related to reusability. This means that a COTS is a mature building block, implementing a non-trivial behavior, for which a certain amount of design and verification efforts have been spent. This is why a COTS is not only a component having a behavior, but is also documented: this documentation states both how the COTS should be used, and what it achieves. In practice, these elements are provided informally, as text. Even though this approach is familiar to design engineers, we highlight the need for formalizing them and associating them to the COTS behavior. Building new complex functions out of COTS calls for formal tools in order to achieve a safe design. COTS are usually structured into libraries, when developed and reused by the same team.
A stand-alone control-command COTS is the basic building block considered in this work. It is characterized conventionally by four elements [94] :
1. COTS interface I.
2. a set of preconditions A.
3. a set of post-conditions G.
4. COTS functional behavior M.
The set of post-conditions are satisfied by the COTS behavior if and only if the set of precondi-tions are respected by the environment A stand-alone COTS is atomic: no structural decomposition into other elementary COTS is possible.
The COTS interface designates its set of inputs and output variables. The COTS preconditions A is a set of requirements expressed on the COTS’ environment.
The environment aware DCS algorithm
The supervisor construction relies on a similar fixed point computation as in DCS. However, a supplementary constraint needs to be integrated in the DCS basic step CP RED: the con-trollable predecessors are computed under the assumption that the monitor Ma representing the environment assumption stays within the a 1 set of states. CP REDenv(E; ; a 1) = fs 2 BjSj j 8xuc 2 BjXucj; ; 9xc 2 BjXcj; 9s0 2 BjSj : (2.13) s0 = (s; xuc; xc) ^ a 1(s0) ! s0 2 Eg (2.14).
The environment aware discrete controller synthesis (EDCS) performs the same greatest fixed point computation as DCS, except that CP REDenv is used instead CP RED. Notice that if no environment assumption is specified, a 1 = 1.
The resulting controller is a Boolean function vector, as previously explained in 1.5.4.
The control architecture obtained is represented in Figure 2.11. Notice that EDCS operates on the composition between several models: the original design, the uncontrollable environment assumption, and the safety requirement to be enforced (since EDCS cannot enforce liveness requirements). These become part of the corrected design. Besides, the controller needs to observe their internal state.
Table of contents :
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
