Transcript Modelling Reactive Systems - School of Computing Science

Modelling Reactive Systems 4
Professor Muffy Calder
Dept. of Computing Science
University of Glasgow
[email protected]
Aims
To introduce and explore 2 different formalisms and
analysis techniques used in the design of reactive
systems.
To explore the practical issues raised by using these
formalisms and associated software tools, particularly
within the context of communications systems and
protocols.
Includes:
state-based modelling using Promela language
reasoning using model-checker SPIN
linear temporal logic
event-based modelling using LOTOS
communication mechanisms
lots of concurrency - in practice and some theory
Exercise:
model telephone system
reason about system using SPIN
References
My notes (on web)
Technical papers
Web pages (for both LOTOS and Promela)
Two (out of print!) books
Modelling Reactive Systems
Reactive system
•
event driven, internal or external stimuli
•
real-time, concurrent, or distributed
Examples
•
telephony
•
communications networks
•
operating systems
•
avionics
•
VLSI
•
HCI
•
railway signalling
• others (from biochemistry to cat flaps!)
Modelling Reactive Systems
Features
•
nondeterminism
•
concurrency
•
communication
Concerns
•
fairness
•
race-conditions
•
timing
•
safety properties
(something bad does not happen)
•
liveness properties (something good happens)
(Liveness is harder to prove than safety)
State or Event-Based Modelling?
What is a process?
How do processes interact?
• is communication synchronous
• is communication asynchronous
How do we model a process?
•
event based
•
state-based
Event based
a
Events label edges
b
stop
c
stop
a; ((b; stop) [] (c; stop))
LOTOS
State-based
ev== a
Variables label states
e== b
ev = a;
ev = b;
if :: ev= c
:: ev = d
fi
Promela
ev== c
ev= =d
Finite State Automata (informal)
FSA is conceptual machine
•
a given number of states (finite or infinite)
•
m/c is in exactly one state, at any time
•
state transitions are caused by (input) events
•
state transition may cause (output) events
•
typically, states represent visible modes of
behaviour.
STS structured transition system
•
graphical representation of an FSA
•
nodes represent states
•
edges represent events
Examples: a chocolate machine
Kripke Structures (informal)
A Kripke structure consists of
•
a given number of states
•
an initial state
• a set of final/accepting states
• a transition relation between states
•
a function labelling states with valuations of
the variables in states
A computation path is a sequence of states s0,s1,… such
that there is a transition between si and si+1.
A computation path may be infinite.
We are concerned with systems which have a finite
number of states, but computation paths may be finite or
infinite.
Example
•
A chocolate dispensing machine.
Process Diagrams
A channel is a directed communication link between 2
processes.
A message or signal may by sent and received to/from a
channel.
A process diagram:
Environment
Process a
message
message
message
Process b
A static description of system/network “topology”.
Do not confuse these with automata!