Transcript Safety-Critical Systems

Safety-Critical Systems 5
Testing and V&V
T 79.232
V - Lifecycle model
Requirements Model
Requirements
Document
Test Scenarios
Knowledge Base *
Test Scenarios
Requirements
Analysis
Functional /
Architechural - Model
Systems
Analysis &
Design
Specification
Document
Software
Design
System
Acceptance
System
Integration & Test
Module
Integration & Test
Software
Implementation
& Unit Test
* Configuration controlled Knowledge
that is increasing in Understanding
until Completion of the System:
• Requirements Documentation
• Requirements Traceability
• Model Data/Parameters
• Test Definition/Vectors
Testing
Testing is a process used to verify or validate
system or its components.
Testing is performed during various stage of
system development. V-lifecycle diagram.
- Module testing – evaluation of a small
function of the hardware/software.
- System integration testing – investigates
correct interaction of modules.
- System validation testing – a complete system
satisfies its requirements.
Testing forms
Dynamic testing - execution of the system or
component in the natural/simulated environment.
- Functional – test all functions
- Structural – test signal/test cases (glass-box)
- Random – n-dimensional input space
Static testing - reviews, inspections and
walkthroughs. Static code analysis for software.
Modelling - mathematical representation of the
behaviour of a system or its environment.
Testing methods
Black-box testing – requirements-based,
no information of the system, what is
inside.
White-box testing – more information
about the system design to guide testing.
Open view glass box.
Dymanic testing techniques
Dynamic testing standards IEC1508, BCS
(British Computer Society) and DO-178B.
- Process simulation
- Error seeding/guessing
- Timing and memory tests
- Performance/stress testing
- Probabilistic testing – values for failure
rates
Test planning
Lifecycle Phase
Requirements
Test planning
Req/Design/Test
Req/Design
Activity
Hazard identification
Identify tests integrity
Trace hazards to specs.
Define specs
Safety case
Analysis results
Strategy for V/V
Risk reduction
Design analysis
• Safety Functional Requirements are the actual safetyrelated functions which the system, sub-system or item of
equipments required to carry out. (Cenelec)
Development Process for V & V
• Operational Thread:
• Safety Thread:
– Elaboration of operational requirements in
textual form
– Elaboration of requirements model based on
operational requirements
– Until validated:
• Validate requirements model against
operational requirements
• Update model as needed
– Transformation of the requirements model
into a verifiable form
– Identification of safety requirements
based on hazard analysis
– Formalization into a safety model based
on safety requirements
– Until validated:
• Validate safety model against
hazard analysis
• Update model as needed
– Transformation of the safety model into
a verifiable form
 Until verified:
Model verification based on safety an liveness requirements
Update model as needed
Development Process for V & V
Validation
Textual requirements
Operational
requirement
s
Validation
Terms &
definitions
Safety
requirement
s
Informal
Verification
Use cases &
control
cases
Important
interactions
(Initial) Requirements model
Domain
objects
Dynamic
behavior
Validation
Informal
Verification
Safety
properties
Formal
Verification
(Final)
Requirement
s model
Model Validation
e.g.
„What use cases
are available to
the signaler?“
Requirements
Modeling
Language
Validation
RequirementsSupport Tool
Model
Question
Confirmer
Domain Expert
Validator
e.g.
•prepare to train arrival
•set reserved path
•monitor situation
Validation/Confirmers
• Confirmer: A property of a system derived from a model
and subject to human evaluation.
• Types of confirmers:
– Static, derived (i.e. implicit) model information (e.g. implicit use
cases or required conditions for a transition/action)
– Dynamic state requests („is the model now in the right state?“)
– Dynamic event responses („does the model react correctly?“)
• Possible representations for confirmers:
– Natural language sentences
– Algebraic expressions
– Traces / sequence diagrams
– Dynamic simulation
Model Verification
e.g.
„A point may never
move when a route
is locked.“
Requirements
Modeling
Language
Verification
RequirementsSupport Tool
Model

Challenger
Domain Expert
Proof
Verifier
e.g. challenger is false in the
following case:
•User: set route A
•System: steer point 1 left
•HW: point 1 at left
•User: set point 1 right
•System: steer point 1 right
CONFLICT!!!
Languages of Logic
– Propositional Logic
Statements
– (1st Order) Predicate Logic (FOPL)
Statements quantified (, ) over things (objects!)
– Linear Temporal Logic (LTL)
Statements quantified (, , G, F, H, P) over things
and time
– Computational Tree Logic (CTL)
Statements quantified (, , G, F, H, P, , ) over
things, time and worlds (modal logic)
– Enhanced Regular Expression Logic (ERE)
Statements about occurrence patterns (seq, sel, itr,
par) of events and conditions causing actions
S
S
S
t
S
t
S
S S
S
•Note: The list above is neither complete nor it does necessarily imply any
hierarchy!
t
(Some) Languages of Logic
CTL
ERE?
Time
G, F, H, P
Temporal
Logic
(LTL)
Modal
Logic
Propositional
Logic
Worlds
, 
DL
Objects
, 
Predicate
Logic
Verification Technologies
Model Checking
Theorem Proving
CTL
ERE?
Time
G, F, H, P
Temporal
Logic (LTL)
Worlds
, 
Moda
l
Logic
Propositiona
l
Logic
D
L
Objects
, 
Predicate
Logic
Testing and V&V
Home assignments:
- 12.7 Dynamic testing
- 12.20 Constructed environment
Please email to [email protected] by
12 of May 2005
References: KnowGravity, I-Logix