(Downloads - 0)
For more info about our services contact : help@bestpfe.com
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
