Project Topics
Get Complete Project Material File(s) Now! »
The COTS-based design method
Introduction
The former chapter provides an overview of the state of the art in the domain of designing critical hardware systems; (1) modeling the behavior of hardware systems, (2) the formal verification of hardware systems and and its utility in finding design errors (3) the discrete synthesis tool and its capacity to automatically generating a correcting component named controller which once combined to the original system, it makes the resulting assembly satisfy safety properties, (4) the COTS-based design of embedded systems and the safety notion in COTS-based systems.
This chapter presents a novel COTS-based safe design method. Its novelty comes from the synergy between the formal verification and the Discrete Controller Synthesis techniques for building correct COTS-based designs. While formal verification is a mature technique in in-dustry, DCS has never been previously in an industrial hardware design project. Besides the specific methodological aspects related to COTS design, the key issues in applying DCS to hardware designs are explained and solved.
The COTS components considered here are described by a behavioral model built by their original designer. The actual user has no knowledge about their implementation details, as sometimes the design code provided is not even readable. The user side perception of a COTS is a documented black box. The requirement specifications are formally expressed PSL language. These formal specifications are either given by the COTS provider, or built a posteriori by the COTS user, from the textual documentation.
The method proposed here encompasses all stages, from the initial specification to the target implementation prior to hardware synthesis. It is illustrated through a non-trivial yet pedagogic example: the generalized buffer system abbreviated as GenBuf [91].
The rest of the chapter is organized as follows : section 2.2, defines the notion of COTS, as used throughout this work. Basic reasoning steps in COTS-based design are presented in section 2.3, followed by the articulation with the Discrete Controller Synthesis technique.
DCS application to hardware designs needs a user-specified partition of the input signals set, in order to designate controllable inputs. As explained previously, this step is unnatural to hardware design engineers. A technique is developed in order to determine a set of candidates to controlability, automatically providing designers with a set of controllable candidates. These elements are aggregated within a global design method. Section 2.4 presents the example of a COTS-based hardware design. The application of the method developed here is illustrated on this example. We have presented this work in [92], [93].
Building COTS-based control-command systems
Stand-alone COTS
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.
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 need for environment assumptions. COTS are logical building blocks which are intended to be assembled in order to build the final control-command system driving an operative part, as shown in figure 2.1. Hence, the environment of a COTS is rarely physical, but most often logical, made of other COTS. Complex interactions may occur between COTS through commu-nication. In order to handle this complexity within a design team where COTS components can be developed separately, a contract-based approach is generally used [95]. Consider the COTS
C and C′, developed separately by two designers. They each implement a specific function, and they interact with each other through inputs and outputs.
At the moment of designing C, the designer reasons as follows: the design at hand assign outputs according to the values of the inputs and possibly an internal state. It often happens that some (sequences of) inputs only make sense in some given configurations. There are three possible choices:
• an input value is unexpected. It should be processed and this should result in an error code;
• an input value or sequence comes at the wrong moment. Either answer with an error code, or memorize it till it can be processed.
Either possibilities require adding additional, often very complex code, making sure that inputs are just as expected. Testing every possible situation is time-costly and error-prone.
• assume that the input values cannot be erroneous. Document this assumption.
The designer of C′ follows the same reasoning. Hence, either both designers should add extra heavy code for testing the validity of the inputs, or they both assume that invalid inputs cannot occur. This is also known as “assume-guarantee” reasoning: when designing C, it is assumed that C′ behaves correctly. The designer of C′ should guarantee this correction. This approach is very cost effective even though this reasoning is not always valid: typically, if the correction of C depends on the correction of C′ and vice-versa, the assume-guarantee reasoning cannot be applied. This issue is illustrated later in this document.
This work mainly addresses designs made of interconnected COTS, which is why the method we propose needs to reason about the environment behavior of a given COTS (or COTS assembly).
The construction of the functional behavior formal model M is not mentioned in this document, as it is generally systematically and automatically extracted from the design code (VHDL or other). This is why, by an abuse of language, pieces of code are referred to as models.
The FSM model MC satisfies the requirement gC provided that all the assumptions aC1 . . . aCk ∈ AC are satisfied by the environment of MC . This dependency |= between assumptions and guarantees does not necessarily mean a logical implication. It happens that hardware designers express environment assumptions either as sufficient conditions or as necessary conditions, or sometimes both. Most often, they are perceived as necessary conditions. The difficulty of dis-tinguishing between these two situations comes from the sequential complexity of the COTS’ behavior. It would be theoretically very interesting to automatically “extract” the set of neces-sary environment assumptions a COTS needs in order to operate correctly; however, such an operation is not possible to the best of our knowledge.
The satisfaction relation |= has the following signification:
• if gC is a logical specification, then the satisfaction is established by model checking MC against gC by assuming aC1 . . . aCk ;
• if gC is an operational specification, then there are two possibilities:
– gC is a monitor. It has the form (I, MgC , ∅, φErr), where Err is the single output of MgC and asserted true if the behavior observed by MgC violates the desired require-ment. The predicate φErr is of the form “always (¬Err)”. In this case, M C ||MgC is model checked against φErr;
– gC is a “golden” , or reference FSM model. MC should be sequentially equivalent to gC . In other words, MC should have exactly the same behavior as gC . This can also be established formally, by model checking.
It is important to note that the sets AC and GC contain two kinds of requirements: those ex-pressed by the designers, which are considered as the most important, but also, in a large num-ber, those left implicit; their exhaustive expression is both practically impossible and useless. However, some assumptions and/or guarantees which have been left implicit can simply char-acterize design errors, left uncovered. Indeed, uncovering a bug requires asking the “right question”, and translate it logically or operationally. This totally depends on the verification engineer’s skill, and thus, the chances of success are random. Hence, a COTS is not a “perfect” component; it can (and probably) have hidden bugs, and building designs out of existing COTS elements also amounts to mixing unwanted behaviors from each building block.
In the context of this work, COTS behaviors are usually specified using the VHDL hardware description language. For the specific needs of the Ferrocots project, the ControlBuild [96], [97] graphical design environment has been used, as it provides designers with a more user-friendly design framework. ControlBuild models are assumed, without loss of generality, to have a synchronous semantics, compliant to the models defined in Chapter 1 of this document. Moreover, all ControlBuild designs are translatable into synchronous VHDL, compliant with the IEEE standard “RTL synthesis subset level 1” [98]. This compliance provides an informal guarantee that a synchronous FSM semantics can be associated to any ControlBuild design.
COTS assembly
A COTS assembly is the act of combining components together, in order to produce a new be-havior, which cannot be produced by any COTS, considered alone. The approach for assembling COTS proposed in this document relies on a rather classical conception of the component-based design: components have a behavior, a set of guarantees and and a set of assumptions, also known sometimes as contracts. The guarantees hold provided that their corresponding contracts are fulfilled. The act of composing two components amounts to finding a matching between the guarantees of one component and the contracts of the other. An interaction is thus established, and some other guarantees may find themselves satisfied by simple component composition. These mechanisms are quite classical in software programming. This design approach is quite natural, and has proven its robustness. Most recent developments we are aware of, conducted within the AFSEC1 research community, define contracts for reactive timed models [99] and the corresponding compositional reasoning with contracts. Other relevant contributions close to our work have been presented in 1.6.3; they are related to software COTS-based design, where COTS are communicating tasks, modeled by finite state machines and composed together by a synchronous product. The correctness of a COTS-based design is established by model check-ing.
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.
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
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
