Transcript Diapositive 1

Requirement Refinement to Test Case Generation for
Embedded Railway Control Systems
by : Ying YANG
09/06/2011
Ph.D Student
French institute of science and technology for
transport, development and networks (IFSTTAR)
Lille, France
Intervenant - date
Content
• Introduction and background
• Formal specification
– Requirement refinement method
– A case study
• Formal verification
– Method of conformance testing - a framework
Intervenant - date
Content
• Introduction and background
• Formal specification
– Requirement refinement method
– A case study
• Formal verification
– Method of conformance testing - a framework
Intervenant - date
FERROCOTS project
Cabling technology
using relay panels
Railway commandcontrol systems
Cabling technology
Disadvantages
Use of electronic cards with simple logic gates,
Difficult to update the functions
transistors, diodes and analog circuits to perform logic
Weight
functions.
Cost
Intervenant - date
1
FERROCOTS project
Cabling technology
using relay panels
Railway commandcontrol systems
COTS-based
technology
FPGA
COTS-based technology
Use of Commercial-Off-The-Shelf (COTS) components
a COTS is a programmable piece of hardware called High
Speed Field-Programmable Gate Array (FPGA).
Space-, Weight-, Cost-saving,
Flexible
Easily maintained
Reuse of components
Intervenant - date
2
Content
• Introduction and background
• Formal specification
– Requirement refinement method
– A case study
• Formal verification
– Method of conformance testing - a framework
Intervenant - date
Transformation from informal to
formal requirement
What we want:
Formal specification
– Describe what the system should do
– By building a rigorous mathematical model
How to get formal models:
Transformation from informal to formal requirement
Requirement list
Rn:
R2:
R1: fonction
requirement
Intervenant - date
Transformation
Formal models
Traceability
3
Requirement refinement method
Objective and introduction
Requirement
document
Analyze
Requirement refinement method:
• A progressive transformation
• Assure the requirement traceability
Raw requirements
Refinement
Refined
requirements
Formalization
Intervenant - date
Verification
Properties
Formal verification :
• model-checking
• test/simulation
4
Process1: requirement refinement process
Three refinement patterns
• Refinement patterns:
– «Clarify»
– «Split»
[requirement directly formalizable]
[requirement need to be refined]
Choose refinement pattern
[ambiguity or fuzzy
information detected]
AND/OR/XOR
– «Modify»
«Add»
«Remove»
«Change»
[inconsistent information or
obvious errors detected]
[sub-requirements detected]
Clarify requirement
Choose split type
[and]
[xor]
Choose modification type
[missing information]
[Redundant
information]
[or]
Split AND
Split OR
Formalize requirement
Split XOR
Add
Remove
Change
Send to verification and validation
Activity diagram of requirement refinement process
Intervenant - date
[wrong information]
5
Process 1: requirement refinement process
Intro SysML
• SysML
– Modeling for system engineering
– Inspirited by UML 2
• Requirement diagram
Intervenant - date
6
Process1: requirement refinement process
New stereotypes defined
Stereotypes
Refinement
patterns
«ClarifyReq» «Clarify»
«SplitReq»
«Split»
AND/OR/XOR
AND/OR/XOR
«ModifyReq»
add/remove/
change
«Modify»
add/remove»/
change
SysML profile diagram with new stereotypes
and their attributes defined
Intervenant - date
7
Process 2: requirement formalization process
Formal framework-CTL*
• Formal framework: a temporal logic CTL*
– Classical logic + operators with time
– A superset of CTL (Computation Tree Logic) et LTL (Linear Time
Logic)
• Why?
– For formal verification
• Model checking / test
– “Intuitive” logic
Logic operators directly mapped to natural language words, like
“Globally”, “Finally”
Intervenant - date
8
Process 2: requirement formalization process
Formal framework-CTL*
• Path operators
X (next), F (future), U (until), G (globally)…
|= Gp
• State operators
A (always)
Aφ: the formula φ must hold on every path.
R: the train doors can be opened only when the train speed ≤ 2km/h
AG(dooropen → trainspeed ≤ 2km/h).
Intervenant - date
9
Case study
Train Door Control system
series of subsystems
Sensors
Alarms
Fire detection
Door (un)locking
…
Inputs
COTS
(FPGA)
General
command
General
command
central
console
Local
command
when a passenger push the button to
open one of the doors in the right side
of train, the COTS receives a local
command, then it verify whether
authorization of right-hand doors is
true…
Intervenant - date
10
Case study
Train Door Control system
•
The requirement of generating the authorization of door
opening is described as follows:
– 1) some buttons can allow the driver to generate the authorization for
door opening. a) A push button for cancelling the signal of closing the
right-hand doors, which is located on the console. b) A push button for
cancelling the signal of closing the left-hand doors, which is located on
the console. c) A push button for cancelling the signal of closing the
right-hand doors, which is located near the right side of the window in
the driving cabin. d) A push button for cancelling the signal of closing
the left-hand doors, which is located near the left side of the window in
the driving cabin.
– 2) When the train speed is ≤ 2km/h, if the doors are closed and
locked, the doors can be authorized to be opened.
Intervenant - date
11
Intervenant - date
1) some buttons can allow the driver to generate the
authorization for door opening. a) A push button for
cancelling the signal of closing the right-hand doors,
which is located on the console. b) A push button for
cancelling the signal of closing the left-hand doors,
which is located on the console. c) A push button for
cancelling the signal of closing the right-hand doors,
which is located near the right side of the window in
the driving cabin. d) A push button for cancelling the
signal of closing the left-hand doors, which is
located near the left side of the window in the
driving cabin.
2) When the train speed is ≤ 2km/h, if the doors are
closed and locked, the doors can be authorized to be
opened.
12
Case study
Train Door Control system
R1.1.3 is formalized by P1.1.3
its variables:
• PB(C-CD-R)_1: push button 1 for
cancelling the signal of closing the
right-hand doors
• PB(C-CD-R)_2 : push button 2 for
cancelling the signal of closing the
right-hand doors
• AU-OD-R : authorization for
opening right-hand doors
P1.1.3 :
AG((AU - OD - R) 
(PB(C  CD  R ) _ 1  PB(C  CD  R ) _ 2))
Intervenant - date
13
Case study
Train Door Control system
P1.1.4 similar to P1.1.3
AG((AU - OD - L) 
(PB(C  CD  L) _ 1  PB(C  CD  L) _ 2))
Intervenant - date
14
Case study
Train Door Control system
R1.3.1 is formalized by P1.3.1
its variables :
•
•
•
•
TS: the train speed is ≤ 2km/h
door_R: the set of all the right-hand
doors
close_R and lock_R: the state of righthand doors
AU-OD-R : authorization for opening
right-hand doors
P1.3.1 :
AG((AU - OD - R)  T B
 ((x  door _ R)
(close _ R( x)  lock _ R( x)))
P1.3.2 :
AG((AU - OD - L)  T B
 ((x  door _ L)
(close _ L( x)  lock _ L( x)))
Intervenant - date
15
Case study
Train Door Control system
AG((AU - OD - R)  T B
((x  door_R)(close _ R( x)  lock _ R( x))) 
( PB(C  OD  R) _ 1  PB(C  OD  R) _ 2))
AG((AU - OD - L)  T B
((x  door_L)(close _ L( x)  lock _ L( x))) 
( PB(C  OD  L) _ 1  PB(C  OD  L) _ 2))
Intervenant - date
16
Content
• Introduction and background
• Formal specification
– Requirement refinement method
– A case study
• Formal verification
– Method of conformance testing - a framework
Intervenant - date
Conformance testing
- a framework
EFSM
specification
s
test
generation
Specification
Phase
Verification
Phase
Testing process
conforms to
test suite
Ts
test suite
tranformation
Refined
requirements
Formalization
VDHL test bench
IUT (VDHL)
Tb
i
Testing
Properties
Modelchecking
test execution
via simultion
test verdict
log
Intervenant - date
17
JING YANG
IFSTTAR, ESTAS,
F-59650 Villeneuve d’Ascq, France
Email: [email protected]
Intervenant - date