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]

• Processes

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 Process:

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

• Repetition

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)