PROMELA and SPIN:
Verification of Parallel Programming Models
(http://cm.bell-labs.com/cm/cs/what/spin/Man/promela.html)
Definitions:
- Validation - doing the right thing (do the specifications
meet user requirements)
- Verification - doing it right (does it properly
implement specifications)
SPIN: a generic verification
system that supports the design and verification of asynchronous process
systems
- focus is on proving the correctness of process
interactions
- typically must abstract-out many internal states
to reduce verification time
- must reduce the number of states that must be
investigated
- must make sure the model is still valid after
abstraction
SPIN as a formal methods
tool:
- an intuitive, program-like notation for
specifying design choices unambiguously, without implementation detail
- a powerful, concise notation for expressing
general correctness requirements
- a methodology for establishing the logical
consistency of the design choices and matching correctness criteria
SPIN
- accepts design specifications written in the
verification language PROMELA (a PROcess MEta LAnguage)
- accepts correctness claims specified in the
syntax of standard Linear Temporal Logic (LTL)
- must have countably
many distinct behaviors (states)
PROMELA Example: A model of
the mars lunar lander Sojourner
PROMELA Example: A model of an Alarm Clock
PROMELA: Elements
- Lexical Conventions: five classes of
tokens-identifiers, keywords, constants, operators, and statement
operations
- Comments (/*.....*/)
- Identifiers: single letter, period, or underscore
followed by zero or more letters, digits, periods, or underscores
- Keywords: active, assert, atomic, bit, bool, break, byte, chan, proctype, do, if, goto,
never, provided, proctype, run, skip, short,
timeout, xr, xs,
unless,...
- Labels: identifier":"- with special use
of end..., progress..., and accept
- Constants: #define name 5
- Expressions: binary and unary: things like != for
not equal, or >= for greater than or equal
while(a!=b)
-> skip is same semantics as (a==b) ->
- Conditional Expressions: (expr1->expr2:expr3)
takes on expr2 if expr1 evaluates to "0", and expr3 otherwise
- Declarations: processes, variables, channels can
be declared locally within a process or globally
- Variables: byte name1, name2 = 3, name3[4] = 3;
- Symbolic Constants: mtype
= {OK, READY, ACK} with use as: mtype
Status = OK;
- Message Channels: synchronous (unbuffered) or asynchronous (buffered): use ! for output and ? for
input
chan Transfer = [2] of (mtype,
bit, short, chan),
Device[3] = [0] of (byte),
Channel
q!var1,const,var2,...
or, equivalently q!var1(const,var2,...)
q?var1,const,var2,... or, equivalently
q?var1(const,var2,...)
- Exclusive receive and send: xr
Transfer; xs Channel
- Structures: typedef Msg {byte a[3],b; chan p}
Msg foo;
chan stream = [0] of {mtype, Msg}
"accessed as"
foo.a[1]
proctype pname{ chan
In, Out; byte id)
{statements}
run pname(Transfer,
Device[0], 0)
OR
active [N] proctype pname(...) provided (E) priority M, where E is enabling
expression(condition)
init{....}
- Statements: assert, assignment, atomic, break,
declaration, d_step, else expression, goto, receive, selection, skip, repetition, send,
timeout, unless
- Executability: statements are separated by ; or -> (->
used typically used when guards are indicated):
Statements
are executed if enabled: assignments, declarations, assert,
skip, goto, and break are always enabled.
- Assert: assert(expression) is executed if
expression returns a 1 (used to check correctness conditions) If
expression is false, then assertion is false and execution stops;
otherwise, it continues
- Atomic: atomic{statements}
attempts to execute the statements in one indivisible step.
- Selection:
if
:: statements
:: statements
fi
do
:: statements
:: statements
od
- timeout: it becomes enabled only when all other statements
in the system are not enabled (deadlock condition)
- unless: {statments-1} unless {statements-2}
checks enabled-ness of statements-2 before every statement in statments-1
and transfers control to statements-2 when it is enabled (while aborting
statements-1 execution)