¡¤ Introduction
o Global definitions:
¡ì Constants
¡ì Channels
¡ì Propositions
¡ì Stop
¡ì Skip
¡ì Assignments
¡ì Case
¡ì Interleaving
¡ì Interrupt
¡ì Hiding
¡ì Selecting
¡ì Recursion
o Assertion
¡ì Reachability
¡ì LTL
¡¤ Appendix
Critical system requirements like safety, liveness and fairness play important roles in software specification, development and testing. It is desirable to have handy tools to simulate the system behaviors and verify critical properties. Process Analysis Toolkit (also known as PAT) was initially design to investigate system (specified using the classic process algebra Communicating Sequential Processes) verification under fairness assumptions [SUNLDW08a]. The motivation is that fairness assumptions are often necessary in system verification practice in order to prove desirable system properties, whereas existing languages and tools have limited support for fairness modeling as well as verification. We have successfully demonstrated PAT as an analyzer for process algebras in the 30th International Conference on Software Engineering (ICSE 2008) [LiuSD08]. Since then, PAT has been evolved to be a self-contained framework to support fully automated concurrent system analysis.
PAT supports an expressive modeling language, which combines high-level specification language constructs like external/internal choice, parallel composition, interrupt, etc with programmer favored constructs like shared variables, arrays, if-then-else, while, etc. Users thus may use variables, assignment to capture primitive operations of the system and the combine the primitive operation with high-level compositional constructs. Once a system is modeled, users may grasp the behaviors of the system by the means of simulation. PAT supports a powerful simulator, which allows the user to interactively explore the system behaviors. The model checkers embedded in PAT are designed to apply state-of-the-art model checking techniques for systematic analysis. Users can state assertions in various forms, and by just clicking one button, PAT would tell whether the assertion is true or not (in which case a counterexample is generated and ready to be simulated).
PAT is designed for systematic analysis of event-based compositional systems. The input language of PAT is mainly influenced by the classic Communicating Sequential Processes (CSP [Hoa85]). Nonetheless, we extend SP with various useful language features to suit our goal. Examples include shared variables, arrays, asynchronous message passing channels and event annotations which capture a variety of fairness constraints. The language constructs may be categorized into the following groups. The first group is the core subset of CSP operators, including event-prefixing, internal/external choices, alphabetized lock-step synchronization, conditional branching, interrupt, recursion, etc. The second group includes those language constructs which can be regarded as 'syntactic sugar¡¯ (to CSP), including global shared variables, and asynchronous channels. It has long been known that CSP is capable of modeling shared variables or asynchronous channels as processes. However, the dedicated language constructs offer great usability and may make the verification more efficient. The third group is a set of event annotations for capturing event-based fairness constraints. It is known that process algebras like CSP or CCS specifies safety only. The event annotation offers a flexible way of modeling fairness using an event based compositional language. The lastly group is the language for stating assertions, which later may be automatically verified using the built-in verifiers.
A global constant is defined using the following syntax,
#define max 5;
#define is a key word used for multiple purposes. Here it defines a global constant named max, which has the value 5. The semi-colon marks the end of the ¡®sentence¡¯.
Global definitions: variables/arrays
A global variable is defined using the following syntax,
var knight = 0;
where var is a key word for defining a variable and and knight is the variable name. Initially, knight has the value 0. Semi-colon is used to mark the end of the ¡®sentence¡¯ as above. We remark the input language of PAT is weakly typed and therefore no typing information is required when declaring a variable. Cast between incompatible types may result in a run-time exception. An fixed-size array may be defined as follows,
var board = [3, 5, 6, 0, 2, 7, 8, 4, 1];
where board is the array name and its initial value is specified as the sequence, e.g., board[0] = 3. The following defines an array of size 3.
var leader[3];
All elements in the array are initialized to be 0.
In PAT, process may communicate through message passing on channels. A channel is declared as follows,
channel c 5;
where channel is a key word for declaring channels only, c is the channel name and 5 is the channel buffer size; Channel buffer size must be greater or equal to 1. Notice that we do not allow channel size to be 0 (which basically means synchronous message passing). Synchronization is supported by following CSP's approach, i.e., alphabetized parallel composition.
Global definitions: propositions
In addition, the key word #define may be used to define propositions. For instance,
#define goal x == 0;
where goal is the name of the proposition and x == 0 is what goal means. A proposition name is used in the same way global constant is used. For instance, given the above definition, we may write the following,
if (goal) { P } else { Q };
which means if the value of x is 0 then do P else do Q. We remark that propositions are the basic elements of LTL formulae.
A process is defined as an equation in the following syntax,
P(x1, x2, ..., xn) = Exp;
where P is the process name, x1, ..., xn is an optional list of process parameters and Exp is a process expression. The process expression determines the computational logic of the process. A process without parameters is written either as P() or P. A defined process may be referenced by its name (with the valuations of the parameters). Process referencing allows a flexible form of recursion.
The deadlock process is written as follows,
Stop
The process does absolutely nothing.
The process which terminates immediately1 is written as follows,
Skip
The process terminates and then behaves exactly the same as Stop.
A simple event is a name for representing an observation. Given a process P, the following describes a process which performs e first and then behaves as specified by process P.
e -> P
where e is an event. An event is abstraction of an observation. Event prefixing a common construct for describing systems. The following describes a simple vending machine which takes in a coin and dispatches a coffee every time.
VM() = insertcoin -> coffee -> VM();
where event insertcoin models the event of inserting a coin into the machine and event coffee models the event of getting coffee out of the machine. An event may be in a compound form, e.g., x.exp1.exp2 where x is a name and exp1 and exp2 are expressions which are composed local variables (e.g., process parameters). For instance,
Phil(i) = get.i.(i + 1)%N -> Rest();
where i is a parameter of the process. We remark that event expressions are not allowed to contain global variables. This assumption is related to how we calculate alphabet of a process.
An event can be attached with assignments which update global variables as in the following example,
add(x = x+1;) -> Stop;
where x is a global variable. In general, an event may be attached with a sequential program (which may contain if-then-else, while, etc.). Notice that the sequential program is considered as an atomic action. That is, no interleaving of other processes before the sequential program finishes. In other words, once started, the sequential program continues to execute until it finished without being interrupted. From another point of view, the event can be viewed as a named piece of code. The name is used for constructing meaningful counterexamples (or associating fairness with the code, as discussed below).
[For advanced users only] An event may be attached with fairness constraints. Fairness is used to get rid of unrealistic executions of the system, e.g., one process which is ready to make some progress is always ignored by the scheduler. A set of pre-defined annotation may be used to mark an event. For instance, in the following process,
wf{e} -> P()
the event e is annotated with weak fair (captured by this reserved term wf). Informally, it means that if e is always enabled, then it must eventually be engaged. There are currently four kinds of event-based fairness, namely wf, sf, wl, and sl. The following table summarizes its informal meaning. For details, please refer to [SUNLDW08a].
wf(e)
weak fair: if e is always enabled, then it must eventually be engaged.
sf(e)
strong fair: if e is repeatedly enabled, then it must eventually be engaged.
wl(e)
weak live: if e is always ready (enabled in one of the process), then it must be eventually engaged.
wf(e)
strong live: if e is repeatedly ready (enabled in one of the process), then it must be eventually engaged.
Channel output/input
Processes may communicate through channels. Channel input/output is written in a similar way as simple event prefixing. Let P be a process expression.
c!exp -> P ¨C channel output
c?x -> P ¨C channel input
where c is a channel, exp is an expression which evaluates to a value (at run time) and x is a (local) variable which takes the input value. A channel must be declared before it is used. For channel output, the value evaluated from exp is stored in the channel buffer if the buffer is not full yet. If the buffer is full, the process waits. For channel input, the top element on the buffer is retrieved and then assigned to local variable x if the buffer is not empty. Otherwise, it waits.
A sequential composition is written as,
P; Q
where P and Q are processes. In this process, P starts first and Q starts only when P has finished.
In PAT (as in CSP), we distinguish between external choice and internal choice. External choice is made by the environment, e.g., the observation of a visible event or the valuation of the variables. An external choice is written as follows,
P [] Q
The choice operator [] states that either P or Q may execute. If P performs a visible event first, then P takes control. Otherwise, Q takes control. Internal choice introduces non-determinism explicitly. The following models an internal choice,
P <> Q
where either P or Q may execute. The choice is made internally and non-deterministically. Non-determinism is largely undesirable at design or implementation stage, whereas it is useful at modeling stage for hiding irrelevant information. For instance, it can be used to model the behaviors of a block-box procedure, where the exact details of the implementation is not available.
The generalized form of external/internal choice is written as,
[] x:{1..n}@ P(x) - which is equivalent to P(1) [] ... [] P(n)
<> x:{1..n}@ P(x) - which is equivalent to P(1) <> ... <> P(n)
A choice may depend on a Boolean expression which in term depends on the valuations of the variables. In PAT, we support the classic if-then-else as follows,
if (cond) { P } else { Q }
where cond is a Boolean formula. If cond evaluates to true, the P executes, otherwise Q executes. Notice that the else-part is optional. The process if(false) {P} behaves exactly as process Skip.
A generalized form of conditional choice is written as,
case {
cond1: P1
cond2: P2
default: P
}
where case is a key word and cond1, cond2 are Boolean expressions. if cond1 is true, then P1 executes. Otherwise, if cond2 is true, then P2. The condition is evaluated one by one until one which is true is found. In case no condition is true, the default process will be executed if there is one, otherwise, whatever follows will be executed.
A guarded process only executes when its guard condition is satisfied. In PAT, a guard process is written as follows,
[cond] P
where cond is a Boolean formula and P is a process. If cond is true, P executes. Notice that different from conditional choice, if cond is false, the whole process will wait until cond is true and then P executes.
Two processes which run concurrently without barrier synchronization is written as,
P ||| Q
where ||| denotes interleaving. Both P and Q may perform their local actions without referring to each other. Notice that P and Q can still communicate via shared variables or channels. The generalized form of interleaving is written as,
||| x:{0..n} @ P(x)
Parallel composition of two processes with barrier synchronization is written as,
P || Q
where || denotes parallel composition. Different from interleaving, P and Q may perform lock-step synchronization, i.e., P and Q simultaneously perform an event. For instance, if P is a -> c -> Stop and Q is c -> Stop, because c is both in the alphabet of P and Q, it becomes a synchronization barrier. Therefore, at the beginning, only a can be engaged. After that, c is engaged by P and Q at the exactly time. In general, all events which are in both P and Q's alphabets must be synchronized. Notice that, which events are synchronization barriers depends on the alphabets of P and Q. In order to know what are the enabled actions, we therefore must first calculate the alphabets.
In tools like FDR, the shared alphabet of a parallel composition must be explicitly given. In PAT, however, we have a procedure to automatically calculate alphabets. The alphabet of a process is the set of events that the process takes part in. For instance, given the process defined as follows,
VM() = insertcoin -> coffee -> VM();
The alphabet of VM() is exactly the set of events which constitute the process expression, i.e., {insertcoin, coffee}. However, calculating the alphabet of a process is not always trivial. It may be complicated by two things. One is process referencing. The other is process parameters. In the above example, the process reference VM() happens to be the same as the process whose alphabet is being calculated. Thus, it is not necessarily to unfold VM() again. Should a different process is referenced, we must unfold that process and get its alphabet. For instance, assume VM() is now defined as follows,
VM() = insertcoin -> Inserted();
Inserted() = coffee -> VM();
To calculate the alphabet of VM(), we must unfold process Inserted() and combine alphabets of Inserted() with {insertcoin}. Notice that a simple procedure must be used to prevent unfolding the same process again. However, even with such a procedure, it may still be infeasible to calculate mechanically the alphabet of a process. The complicated is due to process parameters. For instance, given the following process,
P(i) = a.i -> P(i+1);
Naturally, the unfolding is non-terminating. In general, there is no way to solve this problem. Therefore, PAT offers two compromising ways to get the alphabets. One is to use a reasonably simple procedure to calculate a default alphabet of a process. When the default alphabet is not as expected, an advanced user is allowed to define the alphabet of a process manually. We detail the first in the following.
First of all, alphabet of processes are calculated only when it is necessarily. That means, only when a parallel composition is evaluated. This saves a lot of computational overhead. Processes in a large number of models only communicate through shared variables. If no parallel composition is present, there is no need to evaluate alphabets. We remark that when there is no shared abstract events, process P ||| Q and P || Q are exactly the same. Therefore, we recommend ||| when appropriate. When a parallel composition is evaluated for the first time, the default alphabet of each sub-process is calculated (if not manually defined). The procedure for calculating the default alphabet works by retrieving all event constituting the process expression and unfolding every newly-met process reference. It throws an exception if a process reference is met twice with different parameters (which indicate probably the unfolding in non-terminating). In which case, PAT asks the user to specify the alphabet of a process using the following syntax,
#alphabet P {...};
where P is process name and {...} is the set of events which is considered its alphabet. Notice that the event expressions may contain variables. The rules is that if process P(X) is defined, you may have alphabet definitions as follows,
#alphabet P {a.X};
Once the alphabets of P and Q are identified, we identify their intersection. If P is ready to perform an event which is not in the intersection, it may simply proceed. Same goes with Q. If P is ready to perform an event in the intersection, it has to wait until Q is also ready to perform this event and then proceed together.
Remarks: If process P is expected to have different alphabets in different places in the specification, a dummy may be defined to associate different alphabet with the same process.
Q1() = P();
#alphabet Q1 {¡};
Q2() = P();
#alphabet Q2 {¡};
The philosophy is that we see both the process expression and alphabet as signatures of a process (i.e., processes with the same process expression but different alphabets are essentially different processes!).
The generalized parallel composition is written as,
|| x:{0..n} @ P(x);
The alphabet of each P(x) is calculated. An event can be engaged if and only if all processes whose alphabet contains this event are ready to perform it.
Process P |> Q behaves as specified by P until the first visible event of Q is engaged and then the control transfers to Q. The following is an example,
Routine() |> exception -> ExceptionHandling()
where Routine is a process which performs normal daily task and ExceptionHandling is a process which performs necessary actions for error handling. Whenever an exception occurs (modeled as event exception), process ExceptionHandling takes the control over.
Process P \ A where A is a set of events turns events in A to invisible ones. Hiding is applied when only certain events are interested. Hiding may be used to introduce non-determinism. The following is an example,
dashPhil() = Phil() \ {getfork1, getfork2, putfork1, putfork2};
Phil() = getfork1 -> getfork2 -> eat -> putfork1 -> putfork2 -> Phil();
where process Phil() specifies a philosopher who gets two fork in order and then eats and then puts down both forks in the same order. Process dashPhil(), however, hides the events of getting up or putting down the forks. We can imagine that the philosopher is so quick that no one can tell how he gets the forks. People can only tell when he is eating. By hiding those events, the rest of the system can not observe those hidden events. We remark that hiding is often used to prevent unwanted synchronization in parallel composition.
Process P / A is the dual of hiding. Instead of turning events in A to be invisible, only events in A are not turned to be invisible. The following thus is another way of defining the process dashPhil() above.
dashPhil() = Phil() / {eat};
Recursion is achieved through process referencing flexibly. The following process contains mutual recursion.
P() = a -> Q();
Q() = b -> P();
System() = P() || Q();
It is straightforward to use process reference to realize common iterative procedures. For instance, the following process behaves exactly as while (cond) {P()};
Q() = if (cond) {P(); Q()};
An assertion is a query about the system behaviors. In PAT, we support a (still increasing) number of different assertions. We support the full set of Linear Temporal Logic (LTL) as well as classic CSP refinement/equivalence relationships.
Given P() as a process, the following assertion asks whether P() is deadlock-free or not.
#assert P() deadlockfree;
where both assert and deadlockfree are reserved key words. PAT's model checker performs a depth-first-search algorithm to repeatedly explore unvisited states until a deadlock state (i.e., a state with no further move) is found or all states have been visited.
Given P() as a process, the following assertion asks whether P() can reach a state at which some given condition is satisfied.
#assert P() reaches cond;
where both assert and reaches are reserved key words and cond is a proposition defined as a global definition. For instance, the following asks whether P() can reach a state at which x is negative.
var x = 0;
#define goal x < 0;
P() = add{x = x + 1;} -> P() [] minus{x = x -1;} -> P();
#assert P() reaches goal;
In order to tell whether the assertion is true or not, PAT's model checker performs a depth-first-search algorithm to repeatedly explore unvisited states until a state at which the condition is true is found or all states have been visited.
In PAT, we support the full set of LTL syntax. Given a process P(), the following assertion asks whether P() satisfies the LTL formula.
#assert P() |= F;
where F is an LTL formula whose syntax is defined as the following rules,
F = e | prop | [] F | <> F | X F | F1 U F2
where e is an event, prop is a pre-defined proposition, [] reads as "always", <> reads as "eventually", X reads as "next" and U reads as "until". Refer to [mc] for its formal semantics. Informally, the assertion is true if and only if every execution of the system satisfies the formula. Given an LTL formula, PAT's model checker firstly invokes a procedure to generate a Buchi automaton which is equivalent to the negation of the formula. Then, the Buchi automaton is composed the internal model of P() so as to determine whether the formula is true for all system executions or not. Refer to [SUNLDW08a] for details. For instance, the following asks whether the philosopher can always eventually eat or not (i.e., non-starvation).
#assert Phil() |= []<>eat;
In PAT, we support FDR's approach for checking whether an implementation satisfies a specification or not. That is, by the notion of refinement or equivalence. Different from LTL assertions, an assertion for refinement compares behaviors of a given process as a whole with another process, e.g., whether there is a subset relationship. There are in total 3 different notions of refinement relationship, which can be written in the following syntax.
#assert P() refines Q() -whether P() refines Q() in the trace semantics;
#assert P() refines<F> Q() -whether P() refines Q() in the stable failures semantics;
#assert P() refines<FD> Q() -whether P() refines Q() in the failures divergence semantics;
#assert P() equals Q() -whether P() equals Q() in the trace semantics;
#assert P() equals <F> Q() -whether P() equals Q() in the stable failures semantics;
#assert P() equals <FD> Q() -whether P() equals Q() in the failures divergence semantics;
PAT's model checker invokes a reachability analysis procedure to repeatedly explore the (synchronization) product of P() and Q() to search for a state at which the refinement relationship does not hold.
Appendix
¡¤ Dining philosophers
#define N 5;
Phil(i) = get.i.(i+1)%N -> get.i.i -> eat.i -> put.i.(i+1)%N -> put.i.i -> Phil(i);
Fork(x) = get.x.x -> put.x.x -> Fork(x) [] get.(x-1)%N.x -> put.(x-1)%N.x -> Fork(x);
College() = ||x:{0..N-1}@(Phil(x)||Fork(x));
Implementation() = College() / {eat.0};
Specification() = eat.0 -> Specification();
////////////////The Properties//////////////////
#assert College() deadlockfree;
#assert College() |= []<> eat.0;
#assert Implementation() refines Specification();
#assert Specification() refines Implementation();
#assert Implementation() refines <F> Specification();
#assert Specification() refines <F> Implementation();
#assert Implementation() refines <FD> Specification();
#assert Specification() refines <FD> Implementation();
¡¤ Leader election for network rings
////////////////The Model//////////////////
#define N 3;
////////////////Global Variables//////////////////
var detectorcorrect = 0;
var detector = false;
var leader[N];
var bullet[N];
var shield[N];
////////////////Processes//////////////////
Process(i) = [!((detectorcorrect==0 && detector) || (detectorcorrect!=0 && leader[0]+leader[1]+leader[2]> 0))]rule1.i.(i+1)%N{bullet[i]=1; leader[i]=1; shield[i]=1;} -> Process(i)
[] [leader[i] == 0 && shield[i] == 1 && ((detectorcorrect==0 && detector) || (detectorcorrect!=0 && leader[0]+leader[1]+leader[2]> 0))]
rule2.i.(i+1)%N{leader[i]=0; shield[i]=0; bullet[(i+1)%N] = 0; shield[(i+1)%N] = 1;} -> Process(i)
[] [leader[i] == 1 && shield[i] == 1 && ((detectorcorrect==0 && detector) || (detectorcorrect!=0 && leader[0]+leader[1]+leader[2]> 0))]
rule3.i.(i+1)%N{ bullet[i] = 1; leader[i] = 1; shield[i] = 0; bullet[(i+1)%N] = 0; shield[(i+1)%N] = 1;} -> Process(i)
[] [leader[i] == 1 && shield[i] == 0 && bullet[(i + 1) % N] == 0 && ((detectorcorrect==0 && detector) || (detectorcorrect!=0 && leader[0]+leader[1]+leader[2]> 0))]
rule4.i.(i+1)%N{ bullet[i] = 1; leader[i] = 1; shield[i]=0; bullet[(i+1) % N] = 0;} -> Process(i)
[] [shield[i] == 0 && bullet[(i+1)% N] == 1 && ((detectorcorrect==0 && detector) || (detectorcorrect!=0 && leader[0]+leader[1]+leader[2]> 0))]
rule5.i.(i+1)%N{bullet[i] = 1; leader[i] = 0; shield[i] = 0; bullet[(i+1)%N] = 0;} -> Process(i);
/* The Oracle*/
DetectorCorrect() = [detectorcorrect == 0](progress{detectorcorrect = 1;} -> DetectorCorrect());
RandomDetector() = [detectorcorrect == 0]((guess1{detector = false;} -> RandomDetector()) [] (guess2{detector = true;} -> RandomDetector()));
Initialization() = ((tau{leader[0] = 0;} -> Skip) [] (tau{leader[0] = 1;} -> Skip));
((tau{leader[1] = 0;} -> Skip) [] (tau{leader[1] = 1;} -> Skip));
((tau{leader[2] = 0;} -> Skip) [] (tau{leader[2] = 1;} -> Skip));
((tau{bullet[0] = 0;} -> Skip) [] (tau{bullet[0] = 1;} -> Skip));
((tau{bullet[1] = 0;} -> Skip) [] (tau{bullet[1] = 1;} -> Skip));
((tau{bullet[2] = 0;} -> Skip) [] (tau{bullet[2] = 1;} -> Skip));
((tau{shield[0] = 0;} -> Skip) [] (tau{shield[0] = 1;} -> Skip));
((tau{shield[1] = 0;} -> Skip) [] (tau{shield[1] = 1;} -> Skip));
((tau{shield[2] = 0;} -> Skip) [] (tau{shield[2] = 1;} -> Skip));
LeaderElection() = Initialization(); (DetectorCorrect() ||| RandomDetector() |||
Process(0)|||Process(1)|||Process(2));
////////////////The Properties//////////////////
#define oneLeader ( leader[0] + leader[1] + leader[2] == 1);
#assert LeaderElection() |= <>[]oneLeader;