Transcript charon-hs

System Design Research Lab
University of Pennylvania
CHARON
modeling language
2/8/2006
System Design Research Lab
University of Pennylvania
Outline
• Languages for hybrid systems
– Overview of design decisions
– Context for CHARON
• CHARON language: the user perspective
– Overview of language features
– CHARON by example
– Semantics
• CHARON toolset
2/8/2006
System Design Research Lab
University of Pennylvania
Languages for hybrid systems
• Design decisions
– domain-specific vs. domain-independent
– modeling style
– typed vs. untyped
• choice of type system
– compositionality vs. structuring
2/8/2006
System Design Research Lab
University of Pennylvania
Application domains
• Hybrid systems describe a variety of domains
– Control systems
• controllers, plants, sensors and actuators; feedback
– Electrical systems
• voltage and current; capacitors, transistors, etc.
– Mechanical systems
• mass and moment; rigid bodies, friction
– Biological systems
• species and reactions; promoters and inhibitors;
concentrations and rate laws
2/8/2006
System Design Research Lab
University of Pennylvania
Domain-specific languages
• Domain-specific languages use concepts of the
application domain
– Translated to mathematical models internally
• Domain-independent languages offer modeling
in terms of mathematical concepts directly
A
B
C
•Differential equations
•Switching conditions
•Reset maps
2/8/2006
System Design Research Lab
University of Pennylvania
Advantages and disadvantages
• Domain-specific languages
– are more intuitive to use
– easier to understand models – fewer errors
– may support domain-specific analysis
• Domain-independent languages
– usually more expressive
– wider applicability
– easier to extend
2/8/2006
System Design Research Lab
University of Pennylvania
What’s more important?
• Switch-centric
x<10
d(x) = -5*x
d(x) = 10*x
• Flow-centric
x>10
d(x)=k*x
x>10 x<10
k
2/8/2006
-5
10
System Design Research Lab
University of Pennylvania
Modeling styles
• High-level models
– System requirements
– Primarily captures
behavior
• Low-level models
– System design
– Behavior + structure
– Software vs. nature
– Code generation
x<10
x
d(x) = -5*x
d(x) = 10*x
k:=-5
x<10
d(x) = k*x
x>10
x>10
2/8/2006
k
k:=10
System Design Research Lab
University of Pennylvania
Types for hybrid systems
• A common programming language concept
– helps avoid common simple mistakes
– helps compiler produce executable
• Common elements of type systems
– type of stored value
– distinguish between input and output
• Types specific to hybrid systems
– is the variable updated continuously?
– can the variable be reset?
2/8/2006
System Design Research Lab
University of Pennylvania
Hierarchical modeling
• Construct system from components
– Composite components consist of primitive
components or other composite components
• Advantages:
– capture the structure of the problem
– hide details
mcp
brake
brake
controller
– reuse components
engine
controller
controller
2/8/2006
torque
engine
plant
System Design Research Lab
University of Pennylvania
Structuring and compositionality
• Hierarchy may be syntactic or semantic
• Syntactic hierarchy provides structuring and
modularization
– means to store large models in small chunks
– ensures that sub-models have compatible
inputs and outputs
• Compositional semantics for hierarchy allows to
compute behavior of the model from behaviors
of its sub-models
2/8/2006
System Design Research Lab
University of Pennylvania
CHARON
• Domain-independent
• Inspired by embedded/control applications
– switch-centric
– both requirements- and design-level models
• Strongly typed
• Has compositional semantics
2/8/2006
System Design Research Lab
University of Pennylvania
Language features: hierarchy
• Architectural hierarchy
– Autonomous agents can contain subagents
– Agents execute concurrently
– Communication via shared variables
• Behavioral hierarchy
– Each agent is described as a state machine
• modes and transitions
– Modes can contain submodes
2/8/2006
System Design Research Lab
University of Pennylvania
Language features: modularity
• Encapsulation
– Local (private) variables restrict
communication and hide details of behavior
• Instantiation
– An agent or mode defined in the model can
be instantiated multiple times
– Agents and modes can have parameters that
are given values at instantiation
2/8/2006
System Design Research Lab
University of Pennylvania
Agents: architecture and data flow
• Agents are autonomous concurrent components
in the model
• An agent consists of variable definitions and
may contain sub-agents
• Agent interfaces are global variables
private analog real leak
level
level
Pump
flow
flow
2/8/2006
inflow
level
leak
Tank
inflow
LTank
leak
Hole
System Design Research Lab
University of Pennylvania
Agents: definition and instantiation
// the tank agent with a hidden leak
agent LTank() {
private analog real leak;
agent tank = Tank();
agent hole = Hole();
}
// a leaky tank controlled by a pump
agent LeakyTank() {
private analog real level, flow;
agent tank = LTank( ) [ inflow := flow ]
agent pump = Pump( 5, 10 )
}
2/8/2006
definition
instantiation
parameterized
instantiation
System Design Research Lab
University of Pennylvania
Primitive agents
• A primitive agent does not have concurrent
structure
– single thread of control
• Behavior is given by a mode
agent Tank() {
write analog real level;
init { level = 6; }
mode top = TankMode( );
}
2/8/2006
System Design Research Lab
University of Pennylvania
Modes: behavior
• A mode is a hierarchical hybrid state machine
• A primitive mode is a single-state machine
• Behavior is given by constraints
mode TankMode() {
read analog real inflow;
read analog real leak;
write analog real level;
diff { d(level) == inflow-leak }
inv { 0 <= level and level <= 15 }
}
2/8/2006
inflow
leak
System Design Research Lab
University of Pennylvania
Modes: behavior + discrete control
• Composite modes have multiple submodes and
discrete transitions between them
PumpMode
private analog real clock
Maintain
on
clock >= 1
turnOff
{clock = 0}
start
Compute
adjust
off
inv { clock <= 1 }
diff { d(clock) == 1 }
2/8/2006
return
System Design Research Lab
University of Pennylvania
Modes: behavior + discrete control
• Modes have variable declarations, same as
agents
PumpMode
private analog real clock
Maintain
on
clock >= 1
turnOff
{clock = 0}
start
Compute
adjust
off
inv { clock <= 1 }
diff { d(clock) == 1 }
2/8/2006
return
System Design Research Lab
University of Pennylvania
Modes: behavior + discrete control
• Modes can have constraints at any level
PumpMode
private analog real clock
Maintain
on
clock >= 1
turnOff
{clock = 0}
start
Compute
adjust
off
inv { clock <= 1 }
diff { d(clock) == 1 }
2/8/2006
return
System Design Research Lab
University of Pennylvania
Modes: behavior + discrete control
• Transitions are instantaneous
• Transitions have guards and actions
PumpMode
private analog real clock
Maintain
on
clock >= 1
turnOff
{clock = 0}
start
Compute
adjust
off
inv { clock <= 1 }
diff { d(clock) == 1 }
2/8/2006
return
System Design Research Lab
University of Pennylvania
Modes: behavior + discrete control
• Transition can happen when its guard is true
• Transition must happen when invariant is false
PumpMode
private analog real clock
Maintain
on
clock >= 1
turnOff
{clock = 0}
start
Compute
adjust
off
inv { clock <= 1 }
diff { d(clock) == 1 }
2/8/2006
return
System Design Research Lab
University of Pennylvania
Control points
• Mode interface: entry and exit points
– Control enters mode via entry points and exits via
exit points
• Different paths through a mode correspond to
different qualitative behaviors
stop
slow
set=25
set=65
fast
alge { speed == set }
2/8/2006
crash
System Design Research Lab
University of Pennylvania
Named vs. default control points
• Default control points allow:
– preemption
– history
Maintain
on
clock >= 1
turnOff
{clock = 0}
start
Compute
adjust
inv { clock <= 1 }
2/8/2006
off
return
System Design Research Lab
University of Pennylvania
PumpMode text
mode PumpMode( int low, int high ) {
private analog real clock;
private discrete real rate;
write analog real flow;
read analog real level;
mode m = Maintain( 0.1, low, high );
mode c = Compute();
trans from default to m when true
do { clock = 0; rate = 0 }
trans from m to c.start when clock > 1 do { clock = 0; }
trans from c.return to m when true
do { }
diff { d(clock) == 1 }
} 2/8/2006
System Design Research Lab
University of Pennylvania
CHARON Semantics
• Similar to hybrid automata
• Two main differences:
– Mode hierarchy
– Asynchronous vs. synchronous semantics
• Synchrony vs. asynchrony
– asynchronous = pure interleaving
– synchronous = dependency-preserving
interleaving
2/8/2006
System Design Research Lab
University of Pennylvania
Active modes and history
• A mode can be active or inactive
• If a mode is active and has submodes
– One of the submodes is active
Maintain
on
clock >= 1
turnOff
{clock = 0}
start
Compute
adjust
inv { clock <= 1 }
2/8/2006
off
return
System Design Research Lab
University of Pennylvania
Active modes and history
• If a mode is preempted, its active submode
should be restored upon return
Maintain
on
clock >= 1
turnOff
{clock = 0}
start
Compute
adjust
inv { clock <= 1 }
2/8/2006
off
return
System Design Research Lab
University of Pennylvania
Active modes and history
•
•
•
•
A new private variable in each mode M: hM
Values for history variable: SM e
Transition actions manipulate history variables
Default exits keep h, non-default reset to e
Maintain
clock >= 1
{hM=turnOff}
on
turnOff
{hM=on}
adjust
inv { clock <= 1 }
2/8/2006
{clock = 0,
h=Compute}
{hM=off}
off
Compute
start
C1
{hC=C1}
{hC=C2}
{hC=e}
{h=Maintain}
return
C2
System Design Research Lab
University of Pennylvania
Mode semantics
• State of a mode:
– Type-correct valuation of all variables
– Variables of the mode and its submodes
V*=Vg ] Vp*, Vp*=Vl ] Vl*SM
• Continuous steps
– Given by flows
• Discrete steps
– Entry, exit and internal steps
2/8/2006
System Design Research Lab
University of Pennylvania
Continuous steps: all in due time
• Cannot let time pass at arbitrary moments:
– All modes need to be properly initialized
– All applicable constraints must be used
• Discrete steps must be “complete”
– Start and end in a primitive mode
•
{ v1 = f(v2) }
M11
2/8/2006
x1
M1
x2
e1 { v• = g(v ) }
1
2
e2 v2:=0
M2
M21
System Design Research Lab
University of Pennylvania
Discrete steps
• Internal steps: RD
– M1: <v1,v2,M11>→<v1,v2,M11> 2 RD
– M: <v1,v2,M1,M11,e><v1,0,M2,e,M21> 2 RD
• Entry steps: Re for each entry exit e
– M2: <v1,v2,e><v1,0,M21> 2 Re2
•
{ v1 = f(v2) }
M11
2/8/2006
x1
M1
x2
e1 { v• = g(v ) }
1
2
e2 v2:=0
M2
M21
System Design Research Lab
University of Pennylvania
Anatomy of an internal step
• Exit step of a submode
• Internal step of the
mode
M1: q1→q2 2 Rx2
M: q1→q4 2 RD
• Transition of the mode
M: q2q3 2 T
• Entry step of another submode
M2: q3q4 2 Re2
)
•
{ v1 = f(v2) }
M11
2/8/2006
x1
M1
x2
e1 { v• = g(v ) }
1
2
e2 v2:=0
M2
M21
Asynchrony: it’s a game
System Design Research Lab
University of Pennylvania
• The choice between discrete and continuous
steps is external to every component
• Discrete step of the system is a discrete step
of one component
Agent 1
Pass time
Agent 2
2/8/2006
System Design Research Lab
University of Pennylvania
Asynchrony: pros and cons
• Pros:
– Fits shared variable model well
– Very easy to implement
• Cons:
– Can be used to implement other
communication mechanisms
– Model becomes cumbersome
2/8/2006
System Design Research Lab
University of Pennylvania
Example: event counter
x
x == 1
{x = 0}
{y = y + 1}
{x = 1}
2/8/2006
y
System Design Research Lab
University of Pennylvania
Example: event counter
x
x == 1
{x = 0}
{y = y + 1}
{x = 1}
• Adding invariant does not help!
2/8/2006
y
System Design Research Lab
University of Pennylvania
Example: event counter
x
{x = 0}
z == true
{x == 0}
z == false
x == 1
{y = y + 1,
z = false}
{z = true}
{x = 1}
z
x == 0
• Model is more complex
• Code generation is problematic
2/8/2006
y
System Design Research Lab
University of Pennylvania
Synchrony: serious matter
• Discrete step of the system is made of one
discrete step of every component
– Schedule can be chosen by the environment
– Must preserve dependencies
Agent 1
Pass time
Agent 2
2/8/2006
System Design Research Lab
University of Pennylvania
Dependencies in agents
• Algebraic and discrete dependencies are
instantaneous:
x(t) = f(…, y(t),…)
• Differential dependencies are not
instantaneous
x(t) = x(t-dt)+f(…, y(t-dt),…)
• Circular instantaneous dependencies lead to
semantic problems
2/8/2006
System Design Research Lab
University of Pennylvania
Dependencies in agents
• Algebraic and discrete: instantaneous
• Differential dependencies: not instantaneous
x  f 11 ( y )
x
y  f 21 ( x)
Xy
X
g1 ( y ) 
z  f1 ( y )
x  f12 ( y )
z
g 2 ( z) 
y  f 2 ( z)
y  f 22 ( x)
• Circular instantaneous dependencies lead to
semantic problems
2/8/2006
System Design Research Lab
University of Pennylvania
Dependency graph
• Graph of dependencies between variables
• Projected on the agents that control the
variables
x  f 11 ( y )
x
g1 ( y ) 
y  f 21 ( x)
g 2 ( z) 
y
z  f1 ( y )
y  f 2 ( z)
x  f12 ( y )
x
z
y
2/8/2006
A1
A2
z
y  f 22 ( x)
System Design Research Lab
University of Pennylvania
Acyclic dependency graphs
• Easy to check and enforce
• Fairly restrictive
• Same evaluation order throughout execution
x  f 11 ( y )
x
g1 ( y ) 
y  f 21 ( x)
g 2 ( z) 
y
z  f1 ( y )
y  f 2 ( z)
x  f12 ( y )
2/8/2006
z
y  f 22 ( x)
System Design Research Lab
University of Pennylvania
Locally acyclic dependency graphs
• Dependency graph is acyclic in every reachable
global mode
x  f 11 ( y )
x
g1 ( y ) 
y  f 21 ( x)
y
z  f1 ( y )
x  f12 ( y )
z
y  f 22 ( x)
x  f 11 ( y )
g 2 ( z) 
g1 ( y ) 
y  f 2 ( z)
z  f1 ( y )
y  f 21 ( x)
g 2 ( z) 
y
y  f 2 ( z)
x  f12 ( y )
OK
x
x  f 11 ( y )
z
y  f 22 ( x)
x
g1 ( y ) 
y  f 21 ( x)
g 2 ( z) 
y
z  f1 ( y )
y  f 2 ( z)
x  f12 ( y )
2/8/2006
OK
z
y  f 22 ( x)
?!
System Design Research Lab
University of Pennylvania
Locally acyclic dependency graphs
• More models accepted
• More expensive execution model
– Different evaluation orders in different
modes
• One step further:
– Separate dependency
graphs for continuous
and discrete updates
• Two steps further: microstep semantics
x  f 11 ( y )
x
g1 ( y ) 
y  f 21 ( x)
y
z  f1 ( y )
x  f12 ( y )
2/8/2006
z
y  f 22 ( x)
g 2 ( z) 
y  f 2 ( z)
System Design Research Lab
University of Pennylvania
Back to CHARON
• Original semantics: asynchronous
– Tools implement asynchronous communication
• New version:
– Synchronous communication
– Mode-based dependencies
– Type system distinguishes shared variables
and signals
• Shared variables are discrete, do not introduce
dependencies, and allow multiple writers
2/8/2006
System Design Research Lab
University of Pennylvania
Charon toolset: visual editor
2/8/2006
System Design Research Lab
University of Pennylvania
Charon toolset: visual editor
2/8/2006
System Design Research Lab
University of Pennylvania
Charon toolset: control panel
2/8/2006
System Design Research Lab
University of Pennylvania
Charon toolset: simulation
2/8/2006
System Design Research Lab
University of Pennylvania
Charon toolset: simulation
2/8/2006