close

Вход

Забыли?

вход по аккаунту

?

ppt version - Carnegie Mellon University

код для вставкиСкачать
Model Checking for
Hybrid Systems
Bruce H. Krogh
Carnegie Mellon University
Hybrid Dynamic Systems
Dynamic systems with both
continuous & discrete state variables
Continuous-State
Systems
Discrete-State Systems
Models
differential equations,
transfer functions, etc.
automata, Petri nets,
statecharts, etc.
Analytical
Tools
Lyapunov functions,
eigenvalue analysis, etc.
Boolean algebra, formal
logics, recursion, etc.
Software Tools
MATLAB, MatrixX,
VisSim, etc.,
Statemate, Design CPN,
Slam II, SMV, etc.
Carnegie Mellon: The Rare Glitch Project
2
Bruce H. Krogh
Three Main Thrusts of Our Project
system
environment
пЃ¬ Verifying system integrity
Synchronization constraints
 Resource constraints
 Real-time constraints

пЃ¬ Modeling the environment
Hybrid dynamics
 Stochastic models

пЃ¬ Usability
Extracting models
 Explaining tool feedback

Carnegie Mellon: The Rare Glitch Project
3
Bruce H. Krogh
Embedded systems with significant
hybrid dynamics
C o m m u n ic a tio n s /
T e le c o m m u n ic a tio n s /
N e tw o rk in g
In d u s tria l C o n tro l
A u to m o tive /T ra n s p o rta tio n
S ys te m s & E q u ip m e n t
C o m p u te rs /P e rip h e ra ls
O ffic e A u to m a tio n
C o n s u m e r E le c tro n ic s /
E n te rta in m e n t/M u ltim e d ia
M e d ic a l E le c tro n ic
E q u ip m e n t
G o ve rn m e n t/M ilita ry
E le c tro n ic s
A e ro s p a c e /
S p a c e E le c tro n ic s
E le c tro n ic In s tru m e n ts /
A T E /D e s ig n &
T e s t E q u ip m e n t
O th e r
Source: ESP, Dec, 1998
Carnegie Mellon: The Rare Glitch Project
4
Bruce H. Krogh
Opportunity to Apply
Formal Verification Techniques
Computer-Aided Control System Design
feature specification
executable spec.
model checking
code
test on engine/
vehicle
production
Carnegie Mellon: The Rare Glitch Project
simulation
code generation
Objective:
Verify feature
behavior for the
entire range of
operating conditions.
hardware in the loop
5
Bruce H. Krogh
Example: Variable CAM Timing
operating look-up
state
table
2-mode
PID/
saturation
controller
cam angle
actuator command
Carnegie Mellon: The Rare Glitch Project
6
Bruce H. Krogh
Example: Variable CAM Timing
Controller
Verification Problem: Determine whether the
controller will switch only once from saturation
to PID mode.
Carnegie Mellon: The Rare Glitch Project
7
Bruce H. Krogh
Continuous-Time Model
Carnegie Mellon: The Rare Glitch Project
8
Bruce H. Krogh
Switching Rule
Discrete-time rule
Switch on magnitude of the
error and the sign of this filter
пЂ­1
H (z) пЂЅ
0 . 7 (1 пЂ­ z )
1 пЂ­ 0 .3 z
пЂ­1
Continuous-time rule
Switch on magnitude of the
error and the sign of this filter
H (s) пЂЅ
150 . 5 s
s пЂ« 150 . 5
error
Carnegie Mellon: The Rare Glitch Project
9
Bruce H. Krogh
Finite-State Analysis
пЃ¬ Assign discrete states to each switch boundary and
the initial condition set
пЃ¬ Determine reachability from each discrete state to
the other discrete states
пЃ¬ Analyze the resulting finite state system
Carnegie Mellon: The Rare Glitch Project
10
Bruce H. Krogh
Reachability Analysis
Carnegie Mellon: The Rare Glitch Project
11
Bruce H. Krogh
Finite-State Model
Switching back to the
saturation controller
is certain from some
initial states
(i.e., specification is not satisfied)
Carnegie Mellon: The Rare Glitch Project
12
Bruce H. Krogh
Applying Model Checking
to Hybrid Systems:
пЃ¬ interpret a hybrid system as a transition system (with
an infinite state space)
пЃ¬ find an equivalent finite-state transition systems
(bisimulation)
пЃ¬ perform verification using the bisimulation
Can this approach be generalized to
higher-order systems?
Carnegie Mellon: The Rare Glitch Project
13
Bruce H. Krogh
Simulink/Stateflow Front End
(graphical editing, simulation)
Threshold-event-driven
Hybrid Systems (TEDHS)
Conversion
Flow Pipe
Approximations
Polyhedral-Invariant
Hybrid Automaton (PIHA)
Quotient
Transition System
Initial Partition
ACTL Verification
Carnegie Mellon: The Rare Glitch Project
14
Partition
Refinement
Bruce H. Krogh
Simulink/Stateflow Front End
(graphical editing, simulation)
Threshold-event-driven
Hybrid Systems (TEDHS)
SWITCHED
CONTINUOUS
DYNAMICS
Conversion
dx/dt = fu(x)
Polyhedral-Invariant
Hybrid Automaton (PIHA)
T
Flow Pipe
Approximations
Quotient
Transition System
STATEFLOW
FSMs
T/P
Partition
Refinement
POLYHEDRAL
REGIONS
Initial Partition
Carnegie Mellon: The Rare Glitch Project
ACTL Verification
15
Bruce H. Krogh
CheckMate Block Diagram
x1
Switched Continuous
Dynamics
Mux
Mux2
Switched
Continuous System 1
Switching
Hyperplanes
th1
Mux
C*x <= d
Mux
Polyhedral
Threshold 1
x2
th2
C*x <= d
Switched
Continuous System 2
Polyhedral
Threshold 2
x3
OR
Logical
Operator
th3
C*x <= d
Switched
Continuous System 3
Mux1
Polyhedral
Threshold 3
q1
Mux
c1
q
c2
Finite
State Machine 1
Discrete-State
Dynamics
Carnegie Mellon: The Rare Glitch Project
q2
c1
q
c2
Finite
State Machine 2
16
Bruce H. Krogh
Simulink/Stateflow Front End
(graphical editing, simulation)
Threshold-event-driven
Hybrid Systems (TEDHS)
T
flow
constraints
Flow Pipe
integrator
Approximations
F1
Conversion
xdot(t)
F2
e(t)
F3
1 x(t)
S
x(t)
Polyhedral-Invariant
m(t)
Hybrid Automaton
(PIHA)
mode
select
X0
initial
condition
cont.
state
discrete m(t)
state
discrete
event
Quotient
Transition System
x(t)
e(t)
T/P
threshold-driven
discrete dynamics
Partition
Refinement
Je
Initial Partition
Carnegie Mellon: The Rare Glitch Project
jump e(t)
mapping
ACTL Verification
17
Bruce H. Krogh
Elements of
CheckMate
Simulink/Stateflow Front End
(graphical editing, simulation)
Threshold-event-driven
Hybrid Systems (TEDHS)
Conversion
Flow Pipe
Approximations
Polyhedral-Invariant
Hybrid Automaton (PIHA)
Quotient
Transition System
Initial Partition
ACTL Verification
Carnegie Mellon: The Rare Glitch Project
18
Partition
Refinement
Bruce H. Krogh
Simulink/Stateflow Front End
(graphical editing, simulation)
Threshold-event-driven
Hybrid Systems (TEDHS)
u’
ei : gi(x)п‚і0
Conversion
u
x пѓЋ INVu
dx/dt = Fu(x)
x пѓЋ Xo
Polyhedral-Invariant
Hybrid Automaton (PIHA)
Initial Partition
Carnegie Mellon: The Rare Glitch Project
x  INVu’
Flow Pipe
dx/dt = Fu’ (x)
Approximations
xu’Ji(xu)
Quotient
Transition System
Partition
Refinement
ACTL Verification
19
Bruce H. Krogh
Elements of
CheckMate
Simulink/Stateflow Front End
(graphical editing, simulation)
Threshold-event-driven
Hybrid Systems (TEDHS)
Conversion
Flow Pipe
Approximations
Polyhedral-Invariant
Hybrid Automaton (PIHA)
Quotient
Transition System
Initial Partition
ACTL Verification
Carnegie Mellon: The Rare Glitch Project
20
Partition
Refinement
Bruce H. Krogh
Simulink/Stateflow Front End
(graphical editing, simulation)
Threshold-event-driven
Hybrid Systems (TEDHS)
Conversion
Flow Pipe
Approximations
Polyhedral-Invariant
Hybrid Automaton (PIHA)
Quotient
Transition System
Initial Partition
ACTL Verification
Carnegie Mellon: The Rare Glitch Project
21
Partition
Refinement
Bruce H. Krogh
Simulink/Stateflow Front End
(graphical editing, simulation)
Threshold-event-driven
Hybrid Systems (TEDHS)
T
Conversion
Flow Pipe
Approximations
Polyhedral-Invariant
Hybrid Automaton (PIHA)
Quotient
Transition System
Initial Partition
ACTL Verification
Carnegie Mellon: The Rare Glitch Project
22
T/P
Partition
Refinement
Bruce H. Krogh
Computing Transitions
q
q'
p
p'
пЃ°'1
пЃ°'2
пЃ°
(пЃ°'1,p',q')
(пЃ°,p,q)
(пЃ°'2,p',q')
Carnegie Mellon: The Rare Glitch Project
23
Bruce H. Krogh
Approximating reachable sets
E.K. Kornoushenko. Finite-automaton approximation to the
behavior of continuous plants, Automation and Remote Control,
1975
J. Reisch and S. O’Young, A DES approach to control of hybrid
dynamical systems, Hybrid Systems III, LNCS 1066, Springer,
1996
A. Puri, V. Borkar and P. Varaiya, пЃҐ-Approximation of differential
inclusions, Hybrid Systems III, LNCS 1066, Springer, 1996
M.R. Greenstreet, Verifying safety properties of differential
equations, CAV’96
M.R. Greenstreet and I. Mitchell, Integrating projections, HSCC98
T. Dang and O. Maler, Reachability analysis via face lifting,
HSCC98
A. Chutinan and B. H. Krogh, Verification of polyhedral-invariant
hybrid systems using polygonal flow pipe approximations,
HSCC99
Carnegie Mellon: The Rare Glitch Project
24
Bruce H. Krogh
Polyhedral flow pipe approximation
t4
t5
t6
t7
t3
t8
t2
t1
X0
t9
• divide R[0,T](X0) into [tk,tk+1] segments
• enclose each segment with a convex polytope
• RM[0,T](X0) = union of polytopes
A. Chutinan and B. H. Krogh, Computing polyhedral approximations to dynamic flow pipes,
IEEE CDC, 1998
Carnegie Mellon: The Rare Glitch Project
25
Bruce H. Krogh
Flow Pipe Segment Approximation
Vertices(X0) at tk
Step 2.
Solve
optimization
for di
Step 1.
a. Simulate trajectories
from each vertex of X0.
b. Take the convex hull
and identify outward
normal vectors.
flow pipe segment
approximated by
{ x | ciTx п‚Ј di, пЂўi }
Vertices(X0) at tk+1
Carnegie Mellon: The Rare Glitch Project
26
Bruce H. Krogh
Flow Pipe Approximation
for a Linear System
пѓ© 0
пѓЄ
A пЂЅ 0
пѓЄ
пѓЄпѓ« пЂ­ 1
1
0
пЂ­2
0 пѓ№
пѓє
1
пѓє
пЂ­ 2 пѓєпѓ»
Vertices for X0
пѓ©1пѓ№
пѓЄ пѓє
1 ,
пѓЄ пѓє
пѓЄпѓ«1пѓєпѓ»
пѓ©2 пѓ№
пѓЄ пѓє
1 ,
пѓЄ пѓє
пѓЄпѓ« 1 пѓєпѓ»
пѓ©2 пѓ№
пѓЄ пѓє
2 , an d
пѓЄ пѓє
пѓЄпѓ« 1 пѓєпѓ»
пѓ©1 пѓ№
пѓЄ пѓє
2
пѓЄ пѓє
пѓЄпѓ« 1 пѓєпѓ»
Uniform time step
Dtk = 0.1
Carnegie Mellon: The Rare Glitch Project
27
Bruce H. Krogh
Flow Pipe Approximation
пЃ¬ Applies to nonlinear dynamics
пЃ¬ Applies in arbitrary dimensions
пЃ¬ Approximation error doesn't grow with time
пЃ¬ Estimation error (Hausdorff distance) can be made
arbitrarily small with Dt < d and size of X0 < d
пЃ¬ Integrated into CheckMate
Carnegie Mellon: The Rare Glitch Project
28
Bruce H. Krogh
Simulink/Stateflow Front End
(graphical editing, simulation)
Threshold-event-driven
Hybrid Systems (TEDHS)
Conversion
Flow Pipe
Approximations
Polyhedral-Invariant
Hybrid Automaton (PIHA)
Quotient
Transition System
Initial Partition
ACTL Verification
Carnegie Mellon: The Rare Glitch Project
29
Partition
Refinement
Bruce H. Krogh
Simulink/Stateflow Front End
(graphical editing, simulation)
Threshold-event-driven
Hybrid Systems (TEDHS)
Conversion
Flow Pipe
Approximations
Polyhedral-Invariant
Hybrid Automaton (PIHA)
Quotient
Transition System
Initial Partition
ACTL Verification
Carnegie Mellon: The Rare Glitch Project
30
Partition
Refinement
Bruce H. Krogh
Application Case Studies
пЃ¬ F 16 auto-land system (Lockheed-DARPA)
пЃ¬ Batch process shut down controller (ESPRIT VHS
Project)
пЃ¬ Automotive powertrain
 Engine
shut-off mode (PARADES)
 Idle speed control (CADENCE)
 Transmission shift controller (Ford-DARPA)
Carnegie Mellon: The Rare Glitch Project
31
Bruce H. Krogh
CheckMate - Current Work
пЃ¬ Sampled-data systems
 clocked
+ unclocked events
пЃ¬ Resets (jumps in the continuous state)
пЃ¬ Efficient hybrid automata generation
Carnegie Mellon: The Rare Glitch Project
32
Bruce H. Krogh
The Rare Glitch Project
пЃ¬ Hybrid system abstractions composable with
independent embedded software models
пЃ¬ Generation of requirements from hybrid system
models (timing and resource constraints)
пЃ¬ Improved technology
 order-reduction
 focused
refinement
 automatic model abstraction
 usability
Carnegie Mellon: The Rare Glitch Project
33
Bruce H. Krogh
Документ
Категория
Презентации
Просмотров
4
Размер файла
755 Кб
Теги
1/--страниц
Пожаловаться на содержимое документа