#### 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!