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