1. Introduction to formal method
Traditional engineering disciplines rely substancially on mathematical models and calculation to make decisions about designs. Formal methods refers to the variety of mathematical modelling techniques that are applicable to computer system design. The formal defination of formal methods is in the following manner:
Formal methods used in developing computer systems are mathematically based techniques for describing system properties. Such formal methods provide frameworks within which perple can specify, develop, and verify systems in a systematic, rather than ad hoc manner.A method is formal if it has a sound mathematical basis, typically given by a formal specification language. This basis provides a means of precisely defining notions like consistency and completeness, and more relevant, specification, implementation, and correctness.
The taxonomy of the degrees of rigor in formal methods are of the following:
2. Formal Verification
Formal verification is an alternative family of methods that use techniques based on mathematical logic to insure the quality of hardware and software systems. Verification takes two approaches: Design verification uses formal logic in the design and specification of a system, providing a structured framework for translating top-level design specifications into a collection of concrete tasks describable by algorithms which can be realized by programmers. Program verification involves proofs of correctness of the programs themselves.
Many professionals in the software industry have increasingly used formal verification methods. The dedicated use of these methods has delivered new levels of software integrity. They generally help the designer concentrate on what the system does rather than on how it does it. Formal verification can be thought of as an umbrella method that includes other methods such as model checking, proof checking, code checking and many more. The concept behind formal methods is to be able to verify software products through the use of mathematical logic.
Generally, formal verification can be considered to contain two types of approaches: design verification and program verification. Design verification uses programming logic to provide a sound framework for translating user requirements into a logic based "language" that can be understood by programmers. Program verification is concerned with the proof that the program is "doing what it is coded to do." This tutorial strictly deals with one method of design verification: model checking.
3 Model Checking
Model checking is a method for formally verifying finite-state concurrent systems. Specifications about the system are expressed as temporal logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not. Extremely large state-spaces can often be traversed in minutes. In model checking, the "checking" is based on the finite state machine. A model-checking tool, as its primary goal, is to check the various states of a software product; this is typically called state-space analysis. It is checking for the existence of deadlocks, livelocks, reachability of local states, etc. The checking action is to check what the program is doing rather than how it is doing it, so the primary purpose of the tool is to generate a sequence of states that the model possesses, check those states, and report the results.
Model Checking, through simulation, is a technique that can be used to verify particular attributes concerning a software product. As with many modeling techniques, and as the name implies, they require some "vision" of the specifications. This "vision" is what many in the industry call a model. A model is a representation of the specifications of the software product in some formal programming language or picture. Arguably, the greatest advantage of a formal programming language, since being based on mathematics, provides a concrete and provable foundation. Due to these mathematical foundations, model checking can employ theorems to "prove" of the correctness of a specification. In most cases, they provide the ability to specify among other items, pre and post conditions, assertions, and temporal logic to meet the specifications. Models are abstractions that omit lots of real features of a physical system, which are irrelevant to the check of a formula of some logic.
3.1 Partial Order Reduction and Symbolic Model Checking
State space generated during verification of protocols is usually so large that most of the time because of memory limitations verification is not completed. This problem is also known as the state-explosion problem. State space explosion is a fundamental obstacle in formal verification of designs and protocols. Solutions to help alleviate this problem fall within two categories: symbolic model checking and partial-order reduction. Symbolic model checking does not create an explicit state space. Instead, sets of states are identified and "linked" to one another via a binary decision diagram (BDD), and hence the word "symbolic" or reference from one set of states to another set. To help in this understanding, one can draw the analogy to a relational database and the entity relationship diagram where tables are linked to one another via a primary key. Partial-order reduction is used within the world of parallel and concurrent programming. Oversimplifying the definition of partial order eduction, it is methods used to decrease the number of states that must be checked in a state machine.
The implement the partial order reduction technique requires knowledge about formal methods and verification. Checking for livelocks and deadlocks in a state machine is only one aspect of the model checker. The ability to check for other conditions may require either the entire state machine to be vigorously tested, or a partial order reduction based on a different algorithm that ensures a specific property is verified.
3.2 Propositional Logic and Temporal Logic
Propositional Logic is a logic based on propositions, or declarative sentences. Propositional Logic has limitations to express more subtle declarative phrases and this led to the design of Predicate Logic, which is also called First Order Logic.
3.2.1 Temporal Logic
Temporal logic (TL), also known as Chronological Logic and Tense Logic, is an extension of conventional (propositional) logic which incorporates special operators that cater for time. With Temporal Logic one can specify (and verify, using the SPIN)how components, protocols, objects, modules, procedures and functions behave as time progresses. The specification is done with (Temporal) logic statements that make assertions about properties and relationships in the past, present, and the future. Temporal Logic, which is the logic upon which model-based verification or model checking is built, originated in philosophy as a branch of logic dealing with the "topology of time". With Temporal Logic, in addition to the propositional logic operators (and (&&), or (||), xor (^), not (!), etc.) there are four future-time operators and four, dual, past time operators:
Safety properties in Temporal Logic state that:
No matter what inputs are given, and no matter how choices are resolved inside the system design, the system will not get into a specific undesirable situation, such as emission of undesirable outputs, or undesirable modes of operation being reached.Liveness properties in Temporal Logic state that:
Some desired configuration will be visited eventually, or some output will be generated eventually.3.2.2 Reactive vs. Transformational Systems
There are two categories of system behavior. The two categories are Transformational and Reactive. Understanding the differences between these two types of system behavior is important to learning about Temporal Logic.
Transformational (sub) Systems
Transformational (sub) Systems are those which have all inputs ready when invoked and the outputs are produced after a certain computation period. It is also called sequential System.Reactive Systems
A well understood reactive system is a traffic-light controller. It never has all its inputs ready--the inputs arrive in endless and perhaps unexpected sequences. It is virtually impossible to write a transformational program that implements a controller such as this.Just about every system has a reactive component, because a system is seldom isolated from its environment. On the contrary, the reason the system exists is typically to collaborate or interact with some entity or entities in its environment. Sending, receiving, recognizing and subjecting sequences of symbols--a reactive behavior, does such collaboration.
3.2.3 Temporal Logic and Reactive Systems
Temporal Logic allows you to specify assertions about
program behavior as time progresses. For example, a traffic-light controller
needs to assert:
[]((RedLightOn -> <>GreenLightOn) &&
(GreenLightOn -> <> RedLightOn))
Which reads: always (i.e., now and any time in the
future), if the lights are red then there exists a time further in the
future where lights will be green, and if lights are green then there exists
a time in the future where lights will be red.
There are many variations on the theme of TL. There is Linear-time Temporal Logic (LTL), Branching Temporal Logic (BTL), Real-Time Temporal Logic (RTTL), Computation Tree Logic (CTL), Graphical Interval Logic (GIL) and Quantified Regular Expressions (QRE), among others. Here, LTL -- upon which the tool SPIN is based, and CTL -- upon which the tool SMV is based, will be discussed in more detail in the following sections.
3.2.4 Computation Tree Logic (CTL)
Computation Tree Logic (CTL), has proven to be extremely fruitful in verifying hardware and communication protocols, and people are beginning to apply it even to verification of software. CTL views time as branching, as one might expect from the "tree" part of the name, so that from a given branch alternative states may be reached. This form of logic lends itself to the verification of concurrent, reactive systems, and those which are non-deterministic.
CTL Connectives
Connectives in CTL consist of two characters. The first is either A or E, and the second is either X, F, G, or U. Their meanings are:
A
Along all possible paths (inevitably)
E
Along at least one path (possibly)
X
Next state
F
Some future state
G
All future states (globally)
U
Until
The pair of characters are put together to form sequences like AX, EF, AG, etc., except for U, which is a binary connective.
Example of CTL
If q is a propositional atom which stands for the descriptive phrase, "The printer is busy", then the CTL formula
EX qmeans something like "Along at least one path, the next state of the printer is busy" or "It is possible that the printer is busy in the next state".
3.2.5 SMV and CTL
SMV is a verification tool which takes the CTL as the logic basis. SMV is widely used in hardware design verification and sepcification area.
SMV input structure
MODULE: defines a template
for a class of state-variables
One-of modules are possible and
a main module is required
VAR:
variable definitions
ASSIGN: transition
definitions
SPEC:
properties to be checked
FAIRNESS: global assumptions about system
behavior
SMV model of the dining philosophers problem
MODULE main
VAR
fork1 : 0..3;
fork2 : 0..3;
fork3 : 0..3;
phil1 : process philosopher(1, fork1, fork2);
phil2 : process philosopher(2, fork2, fork3);
phil3 : process philosopher(3, fork3, fork1);
ASSIGN
init(fork1) := 0;
init(fork2) := 0;
init(fork3) := 0;
SPEC
EF(AG phil1.state = wait & phil2.state = wait & phil3.state = wait)
SPEC
AG(EX 1)
SPEC
EF(AG fork1 = 1 & fork2 = 2 & fork3 = 3)
MODULE philosopher(pid, leftFork, rightFork)
VAR
state : {thinking, wait, eating, doneEating};
ASSIGN
next(leftFork) := case
(state = thinking) & (leftFork = 0): pid;
(state = doneEating) & !(rightFork = pid) & (leftFork = pid): 0;
1 : leftFork;
esac;
next(state) := case
(state = thinking) & (leftFork = pid): wait;
(state = wait) & (rightFork = pid): eating;
(state = eating): {eating, doneEating};
(state = doneEating) & !(leftFork = pid) & !(rightFork = pid): think
ing;
1 : state;
esac;
next(rightFork) := case
(state = wait) & (rightFork = 0): pid;
(state = doneEating) & (rightFork = pid): 0;
1 : rightFork;
esac;
The result from SMV:
-- specification AG EX 1 is true -- specification EF (AG fork1 = 1 & fork2 = 2 & fork3 = 3... is true resources used: user time: 0.53 s, system time: 0.01 s BDD nodes allocated: 11744 Bytes allocated: 1048576 BDD nodes representing transition relation: 593 + 1As shown, above the result of EF(AG phil1.state = wait & phil2.state = wait & phil3.state = wait) is true, and it means that
3.3 Linear Temporal Logic (LTL)
Linear time logics view time as a sequence of states
with no choice as to which state is next, or, at least, the choice of the
next state is deterministic. In
this view, LTL examines a single path or history
in the execution of a program. Contrast this with the view of CTL.
Connectivities of LTL:
[]
Always
<>
Eventually
o
Next cycle
(-)
previous cycle
U
Until
Example of LTL
[] p
This means that p is always true.
<>R -> (P U R)
This means this always the case that P exist before
R happens.
Safety Property
A safety property asserts that nothing bad happens with the execution of a program statement or particular series of statements. An example of bad would be an improper or wrong output. The following TL statement reflects this concept:
[]({readySignal == 1} -> (){ackSignal == 0})
This assertion is read as "Always, readySignal equals one implies ackSignal equals zero on the next cycle". It makes use of the Always operator(the box) and the Next Cycle operator( the empty parentheses pair).
A second example of a safety property is:
[]({readySignal == 1} -> (-){ackSignal == 0})
This one is just like the first on except the use of the previous cycle operator (-). Obviously, it is read as "Always, readySignal equals one impliesackSignal equals zero on the previous cycle".
Liveness Property
A liveness property asserts that something good will happen, eventually:
<>({out1==1} && ()()[]{out2 < 2} && (-){out3==0})
This one can be read as "Eventually, out1 will equal one, and then two cycles later and always after that, out2 is less than two and on the previouscycle out3 equals zero. This example uses the Eventually operator (the diamond <>), the always operator (the box []), and the Next and Previous Cycle operators (the empty parentheses pair () and the parenthesized minus sign (-), respectively.
4. SPIN and PROMELA
SPIN is a software package developed in the Bell Labs formal specification and verification group. SPIN can be used to trace logical errors in distributedsystems design. The tool checks the logical consistency of a specification. It finds deadlocks, unspecified receptions, flag incompleteness, race conditions, and unwarranted assumptions about the relative speeds of processes.
SPIN can analyze a specification in three ways: simulation, exhaustive search, and bit space (partial order reduction) search for large specifications.
The easiest way to use SPIN is to simulate the specification. The simulation will end when the specification terminates or when an assertion fails. The simulator allows for rapid prototyping with random, guided, or interactive simulations.
SPIN can do a more strict analysis of the specification by exhaustively searching all reachable states the system can take. SPIN creates a custom(pan.c) C program, which when compiled and run, performs the exhaustive search. When the program fails to meet its specifications, the custom analyzer will produce the path that forced the system into the invalid state. It is capable of rigorously proving the validity of user specified correctness requirements.
For large specifications, it may be infeasible to perform an exhaustive search due to memory limitations. In this case, SPIN will search a more compactform of the space (bit-space), but only a fraction of the possible states. This partial order reduction search still provides some degree of certainty.
4.1 PROMELA
PROMELA (PROtocol MEta LAnguage) is a formal specification modeling language used as input into the SPIN verifier. A PROMELA model can contain three different types of objects: processes, variables, and message channels.
All processes are global objects. Variables and message channels can be declared either locally or globally within a process. There is no difference between statements and conditions in PROMELA. The execution of every statement is conditional upon its executability. And the executability of a statement is the basic means of synchronization. A process can wait for an event to happen by waiting for a statement to become executable. A condition can only be executed when that condition is true. If the condition is not true, execution blocks until it becomes true. The scope of a variable is global if it is defined outside a process declaration, and local if it is defined within a process declaration.
4.1.1 Variables
There are five basic data types: bit, bool, byte, short, and int. The sixth data type: chan, specifies message channels. A message channel is an object that can store a number of values, grouped into user defined structures.
4.1.2 Process Types
The behavior of a process is defined in a proctype declaration. The process type is named "A". The body of the declaration is enclosed by curly braces and contains a list of zero or more statements. An example of a process type looks like this:
#define OFF 0
#define LOW 1
#define MED 2
#define HIGH 3
byte state = OFF
proctype A()
{
atomic {
(state == LOW) -> state = MED;
(state == MED) -> state = HIGH;
(state == HIGH) -> state = OFF
}
}
proctype B()
{
atomic {
(state == OFF) -> state = state + 1
}
}
Since the assignment in process B is executable when state = OFF, they can always terminate without delay. Process A is blocked until the variable state contains the proper value.
4.1.3 Atomic Sequences
A set of statements enclosed within parenthesis and prefixed by the keyword atomic indicates that the sequence is to be executed as one indivisible unit,non-interleaved with any other processes. Atomic sequences are an important tool in reducing the complexity of a validation model, by dramatically reducing the number of cases that would need to be considered in a validation, without changing the possible behaviors of the processes.
4.1.4 The Initial Process
An init process must be declared within any PROMELA specification, since a proctype declaration only declares process behavior, it does not execute it. The init process is comparable to a main() in a standard C program.
An init process takes the following format:
init
{
run A();
run B()
}
The above init process starts the two processes (A and B), which will run concurrently. Process B will execute its conditional statement and terminate. Process A will then run through its conditional statements sequentially and terminate, leaving the state set to its original value of OFF.
Running a SPIN simulation of the above short program with the -p option (shows the state changes of the PROMELA processes at every step) produces the following output:
zaurak$ spin -p test
0: proc - (:root:) creates proc 0 (:init:)
1: proc 0 (:init:) creates proc 1 (A)
1: proc 0 (:init:) line 22 "test" (state 1) [(run
A())]
2: proc 0 (:init:) creates proc 2 (B)
2: proc 0 (:init:) line 23 "test" (state 2) [(run
B())]
3: proc 2 (B) line 17 "test" (state 1) [((state==0))]
4: proc 2 (B) line 17 "test" (state 2) [state =
(state+1)]
4: proc 2 (B) terminates
5: proc 1 (A) line 10 "test" (state 1) [((state==1))]
6: proc 1 (A) line 10 "test" (state 2) [state =
2]
7: proc 1 (A) line 11 "test" (state 3) [((state==2))]
8: proc 1 (A) line 11 "test" (state 4) [state =
3]
9: proc 1 (A) line 12 "test" (state 5) [((state==3))]
10: proc 1 (A) line 12 "test" (state 6) [state =
0]
10: proc 1 (A) terminates 10: proc 0 (:init:) terminates3
processes created
4.1.5 Message Channels
Message channels are used to model the transfer of data from one process to another and can be declared either locally or globally, using the keyword chan. An example of a message channel is:
#define QSZ 8
#define N 2
/* define channels */
#define a 0
#define b 1
/* define message types */
mtype = { req, busysig, accept, data, ack, disc
};
chan in[N] = [QSZ] of {mtype, byte, byte};
The chan declaration initializes an array of 2 channels, each with a capacity of 8 message slots, with each slot containing a message type of type mtype, and two eight bit values.
The statement: in[b]!req(sa, db) sends a req (request)
message to process b's message channel.
The statement: in[b]?req(sa, db) receives a request
message within b's proctype declaration.
4.1.6 Case Selection
The selection structure is simple, and contains two or more execution sequences, each preceded by a double colon. Only one sequence from the list isexecuted. A sequence can be selected only if its first statement is executable. Therefore the first statement is called a guard. If more than one guard is executable, one of the corresponding sequences is selected at random. If all guards are unexecutable, the process blocks until at least one of them can be selected.
/* Received a request message for client A */
in[a]?req(srcid, destid) ->
assert(srcid != a);
assert(destid == a);
if
:: (state[a] == IDLE) ->
state[a] = INIT;
in[srcid]!accept(destid, srcid)
:: (state[a] == INIT) ->
in[srcid]!busysig(destid, srcid)
fi
The above case selection example will check the guards to see if either client A state is IDLE or INIT. If it is IDLE, client A state will be changed to INITand will put an accept message out on the channel of whichever client sent the original request message. If client A's state is INIT, and it receives a request message, it will place a busy signal message out on the channel.
4.1.7 Correctness Requirements & Validation
The primary purpose behind PROMELA is validation. But in order to validate a design, we need to be able to specifically identify what it means for a design to be correct. Three of the most standard correctness criteria consist of: absence of livelocks, deadlocks, and improper terminations. All correctness criteria within PROMELA define behaviors that are claimed to be impossible. The behavior of a validation model is defined by the set of all the execution sequences it can perform, where an execution sequence is a finite ordered set of states.
4.1.8 Assertions
The statement: assert(destid == a), is an assertion. An assertion is a boolean condition that must be satisfied whenever a process reaches a given state.If the condition is true, the statement has no effect. The validity of the statement is violated, if there is at least one execution sequence in which the condition is false when the assert statement becomes executable.
4.1.9 System Invariants
If there exists a boolean statement (assertion) that is true in the initial system state, and remains true for all subsequent reachable states, then a formal system invariant can be created. In PROMELA, you can place the system invariant by itself in a separate monitor process. This process then runsindependently of the rest of the system and therefore can decide to evaluate the assertion at any time. A system invariant takes the following format in PROMELA:
proctype monitor()
{
assert(counter == 0 || counter == 1)
}
4.1.10 Deadlocks
In order to define a deadlock in PROMELA, we need to be able to distinguish the expected end states from the unexpected ones. The final state of an execution sequence must satisfy the following criteria to be provably free of deadlocks and unspecified receptions. First, every instantiated process has either terminated or reached a state marked as a proper end state. Second, all message channels are empty.
4.1.11 Non-progress Cycles
In order to claim the absence of non-progress cycles, there must be a way to define system states that denote progress within the model. A progress state label marks a state that must be executed for the model to make progress. Execution sequences that violate this are called non-progress cycles. Infinite behaviors within execution sequences that include markedstates are called livelocks.
4.1.12 Temporal Claims
Temporal claims are claims that define temporal orderings of properties of states. But, since all the correctness criteria in PROMELA are based on properties that are claimed to be impossible, temporal claims must also express orderings of properties that are impossible. The notation for a temporal claim in PROMELA is:
never
{
do
:: skip
:: condition -> break
od;
accept: do
:: condition
}
4.2 SPIN / PROMELA EXAMPLES
4.2.1 A Recursive Factorial Program
proctype fact(int n; chan p)
{
int result;
if
:: (n <= 1) -> p!1
:: (n >= 2) ->
chan child = [1] of {int};
run fact(n - 1, child);
child?result;
p!n*result
fi
}
init
{
int result;
chan child = [1] of {int};
run fact(8, child);
child?result;
printf("result of 8! is: %d\n", result)
}
Executing a simulation of this short program with SPIN's -r (receive message) flag and -s (send message) flag produces the following output:
$ spin -s -r factorial
17: proc 8 (fact) line 6 "factorial" Send 1 -> queue
8 (p)
18: proc 7 (fact) line 10 "factorial" Recv 1 <-
queue 8 (child)
20: proc 7 (fact) line 11 "factorial" Send 2 ->
queue 7 (p)
22: proc 6 (fact) line 10 "factorial" Recv 2 <-
queue 7 (child)
23: proc 6 (fact) line 11 "factorial" Send 6 ->
queue 6 (p)
25: proc 5 (fact) line 10 "factorial" Recv 6 <-
queue 6 (child)
26: proc 5 (fact) line 11 "factorial" Send 24 ->
queue 5 (p)
27: proc 4 (fact) line 10 "factorial" Recv 24 <-
queue 5 (child)
29: proc 4 (fact) line 11 "factorial" Send 120 ->
queue 4 (p)
31: proc 3 (fact) line 10 "factorial" Recv 120 <-
queue 4 (child)
32: proc 3 (fact) line 11 "factorial" Send 720 ->
queue 3 (p)
33: proc 2 (fact) line 10 "factorial" Recv 720 <-
queue 3 (child)
35: proc 2 (fact) line 11 "factorial" Send 5040
-> queue 2 (p)
37: proc 1 (fact) line 10 "factorial" Recv 5040
<- queue 2 (child)
38: proc 1 (fact) line 11 "factorial" Send 40320
-> queue 1 (p)
40: proc 0 (:init:) line 21 "factorial" Recv 40320
<- queue 1 (child)
result of 8! is: 40320
9 processes created
4.2.2 Dining Philosophers problem in PROMELA and SPIN result
bit fork[3];
mtype = {thinking, waiting, eating};
proctype philosopher(byte left, right) {
mtype state = thinking;
do
:: ((state==thinking) && (fork[left]==0)) -> atomic{fork[left]=1; state=w
aiting;}
:: ((state==waiting) && (fork[right]==0)) -> atomic{fork[right]=1; state=
eating;}
:: (state==eating) ->
if
:: skip;
:: atomic{state=thinking; fork[right]=0; fork[left]=0;}
fi
od;
}
init {
fork[0]=0;
fork[1]=0;
fork[2]=0;
run philosopher(0, 1);
run philosopher(1, 2);
run philosopher(2, 0);
}
pan: invalid endstate (at depth 37) pan: wrote dining-philosopher-deadlock.promela.trail (Spin Version 3.0.9 -- 11 January 1998) Warning: Search not completed + Partial Order Reduction Full statespace search for: never-claim - (none specified) assertion violations + acceptance cycles - (not selected) invalid endstates + State-vector 40 byte, depth reached 37, errors: 1 27 states, stored 7 states, matched 34 transitions (= stored+matched) 14 atomic steps hash conflicts: 0 (resolved) (max size 2^18 states) 1.493 memory usage (Mbyte)5 Example of concurrent system specfication and verification: Road Traffic Regulation System
5.1 Overview:
This document describes the system, which is a road system with two intersections. (See graphic view)
5.2 Description:
The main road is the one that crosses two branch roads via two intersections. Each intersection has only two roads crossing each other. On each intersection there are four traffic lights that control the flow of traffics. On both sides of the road at the intersection, there are two identical buttons, which are receiving pedestrians' requests for crossing the road, and there are two identical pedestrian crossing signals to response pedestrians' requests. Both intersections are identical. The main road has a higher traffic flow volume than the branch road.
The general rule for this system is that traffics have higher priority than pedestrians. There is another regulation that if both main road traffic lights are GREEN, pedestrian should yield the traffics in Main road by waiting until one of the main road traffic lights in these two intersections changes into RED. This will help the traffic flow in main road.
Pedestrian who pushes the button first will have a priority. If two pedestrians push the button simultaneously in the same intersection, the one who wants to cross the branch road has a higher priority.
Every traffic light (RoadLight) has two states: RED and GREEN. When it is RED, the traffics stop and wait. When it is GREEN, the traffics move ahead.
Every pedestrian crossing signal (PedestrianLight) has two states: RED and WHITE. When it is RED, pedestrian must stop and wait. When it is WHITE, pedestrian can cross the street with protection.
Every pedestrian's request makes button send request signal to the traffic system. Button has two states: ButtonOn and ButtonOff.
5.3 Controls of the system:
PedestrianLightIntersection() controls the pedestrian light at intersection. It decides under what condition the PedestrianLightMain1 and PedestrianLightSub1 can be changed.
RoadLightIntersection() regulates the cycle of intersection traffic light. The traffic light will change by it self in a cycle if not interrupted by pedestrian. If PedestrianLightIntersection() sends signal to RoadLightIntersection(), and then RoadLightIntersection() will switch the traffic lights in this intersection.
Pedestrian() simulate the pedestrian. It can randomly generate signal to simulate the request for crossing the street. This function will also reset the button when the PedestrianLight has changed in response to the request.
5.4 Intended behavior:
Any pedestrian who sends a request to cross the street will receive a response from the traffic control system by giving him or her a white light on PedestrianLight to allow him or her to cross the street (every request will eventually return a white light on PedestrianLight).
The traffic system will response the pedestrians' request in the order of first in first served.
5.5 Unintended behavior:
Once the pedestrian pushes the button to send a request for crossing the street, the pedestrian should not get starved by waiting forever for the pedestrian crossing signal.
No matter how many pedestrians sending requests, the road traffics should also not be blocked forever.
The traffic system should not run into a state in which no request could be served.
5.6 Decomposition
To design a low-coupling system structure and also high-cohesion, the initial decomposition for the system is based on the nature of the real world. The project has two separated intersections and each intersection can be decomposed down into 3 concurrent processes: Traffic light, pedestrian cross light, and another separate process: Pedestrian process. If we model a two intersections system, which has two random generated pedestrians.
1. RoadLight() is a process which regulate the most important part of the intersection system --- changing traffic light in a time cycle.
2. PedestrianLight() models the pedestrian lights control system that regulate the pedestrians lights lighted up by pedestrian who want to cross the Main Road or the Side Road of a intersection.
3. Pedestrian() is modeling the real pedestrian who is trying to get across the street if he or she really wish.
5.7 Abstractions
0. Before I do the abstraction for each component I have defined several Invariants for this system. First I need to define the direction for this system and then it will be easier to describe for the rest of the abstraction process. The system graphic view has shown some basic direction definition. East and West are the directions of side road. South and North are the direction of Main road. E,W, N and S represent the direction in each intersection. The intersection number is pid.
/* direction */ #define E 2 #define W 3 #define N 4 #define S 51. RoadLight() is a process which regulate the most important part of the intersection system --- changing traffic light in a time cycle.
The data structure in RoadLight() is not very complicate. It has four Traffic Lights that control four direction of the intersection. The direction and location have been defined previously. The behavior of proctype RoadLight () is that it change the traffic lights in a cycle. i.e. green -> red -> green -> red. The yellow state is eliminated from light cycles since there is no significant feature for that. The opposite side of the road should have same road light. Here in each intersection there is only one variable rLight[pid] works as traffic light. The initial state of the rLight[ ] is setting main road green.
byte rLight[3];Every time the RoadLight changes from red to green, it will reset the PedestrianLight i.e. pLight[ ] to red. The PedestrianLight control proctype will take care of how to change the PedestrianLight from red to white. In the do loop there is a skip statement, which was originally designed for the asynchronization and help two intersections asynchronized. It was designed for preventing deadlock if there is a channel available between intersections. Certainly there are other features that is abstracted out of this mini system such as at night when main roads get blinking yellow signals but side roads get blinking red signals.
proctype RoadLight(byte pid) {
do
:: rLight[pid] == green ->
atomic {rLight[pid] = red;
pLight[pid].direction[E] = red;
pLight[pid].direction[W] = red;
}
:: rLight[pid] == red ->
atomic {rLight[pid] = green;
pLight[pid].direction[E] = red;
pLight[pid].direction[W] = red;
}
:: true -> skip
od
}
Originally I put two channels to let two intersections
to communicate between each other, but finally I gave up since the system
is too big to verify. The memory is not enough (nearly 200 Mbytes memory
usage).
2. PedestrianLight() models the pedestrian lights control system that regulate the pedestrians lights lighted up by pedestrian who want to cross the Main Road or the Side Road of a intersection.
PedestrianLight() is a process linked in the middle of RoadLight and Pedestrian. Pedestrian pushes the Button and also sends the request to the PedestrianLight(). The PedestrianLight() will do the following things.
It will check whether the Road Light of the side
road is red.
If rLight[pid] = green, then it will check whether
there is message sent from Pedestrian requesting to go across the street.
If also yes, then the message to Pedestrian to allow him to pass and also
set pLight to white.
If rLight[pid] = red, then PedestrianLight() will do an extra checking: to check whether the traffic light at the other intersection is red. If the other one is green then it will do nothing. One of the most important behaviors that I added into this system is that only if both main road traffic lights of both intersections change into red the Pedestrian can walk across the road. This is trying to help the traffic flow of the main road.
If both main road traffic lights of both intersections
are red then the PedestrianLight() will change the pLight[Main] to white
and send signal to the Pedestrian to allow him to pass. This behavior represent
the rush hour feature of a street which helps the Main Road traffic flow.
PedestrianLight() will not change the pLight to
white unless the Pedestrian push the Button. PedestrianLight() will talk
with will different Pedestrian with different channel. Channels have defined
for the massage passing between Pedestrian() and PedestrianLight().
/* channels */
typedef channel {
chan pedes[3] = [1] of {byte, byte, byte}
};
channel ch[3];
proctype PedestrianLight(byte pid, pid2, ped, ped2) {
byte state, where, condi;
atomic { state = idle;
}
end:
do
:: rLight[pid] == red ->
atomic {
if
:: ch[pid].pedes[ped] ? [E, ped, ButtonOn] ->
ch[pid].pedes[ped] ? where, ped, condi;
ch[pid].pedes[ped] ! E, ped, white;
pLight[pid].direction[E] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped] ? [W, ped, ButtonOn] ->
ch[pid].pedes[ped] ? where, ped, condi;
ch[pid].pedes[ped] ! W, ped, white;
pLight[pid].direction[W] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped2] ? [E, ped2, ButtonOn] ->
ch[pid].pedes[ped2] ? where, ped2, condi;
ch[pid].pedes[ped2] ! E, ped2, white;
pLight[pid].direction[E] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped2] ? [W, ped2, ButtonOn] ->
ch[pid].pedes[ped2] ? where, ped2, condi;
ch[pid].pedes[ped2] ! W, ped2, white;
pLight[pid].direction[W] = white;
state = idle
:: else
fi;
}
:: rLight[pid] == red && rLight[pid2] == green ->
state = waitPLight
:: rLight[pid2] == red && rLight[pid] == green ->
state = waitPLight
:: rLight[pid] == red && rLight[pid2] == green ->
atomic {if
:: ch[pid].pedes[ped] ? [N, ped, ButtonOn] ->
ch[pid].pedes[ped] ? where, ped, condi;
ch[pid].pedes[ped] ! N, ped, white;
pLight[pid].direction[N] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped] ? [S, ped, ButtonOn] ->
ch[pid].pedes[ped] ? where, ped, condi;
ch[pid].pedes[ped] ! S, ped, white;
pLight[pid].direction[S] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped2] ? [N, ped2, ButtonOn] ->
ch[pid].pedes[ped2] ? where, ped2, condi;
ch[pid].pedes[ped2] ! N, ped2, white;
pLight[pid].direction[N] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped2] ? [S, ped2, ButtonOn] ->
ch[pid].pedes[ped2] ? where, ped2, condi;
ch[pid].pedes[ped2] ! S, ped2, white;
pLight[pid].direction[S] = white;
state = idle
:: else
fi;
}
od
}
3. Pedestrian() is modeling the real pedestrian
who is trying to get across the street if he or she really wish.
Pedestrian() is a model of real world pedestrians. They have several choices here in the system. They can have three states: idle, waitPLight1 and waitPLight2. The second and third are represent where they are requesting to go across the street.
When Pedestrian is idle he or she can push any of the Button in these two intersections and sending request to PedestrianLight() through channel and also set pButton[pid].direction[ ] = ButtonOn.
When the message is returned from PedestrianLight() in responding the pedestrian's request, he or she will reset the
pButton[pid].direction[ ] and cross the road by reset the state back to idle.
proctype Pedestrian(int ped) {
byte state, where, condi;
atomic { state = idle;
}
end:
do
:: state == idle -> state = idle
:: state == idle -> atomic { pButton[1].direction[E] = ButtonOn;
state = waitPLight1;
ch[1].pedes[ped] ! E, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[1].direction[W] = ButtonOn;
state = waitPLight1;
ch[1].pedes[ped] ! W, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[1].direction[N] = ButtonOn;
state = waitPLight1;
ch[1].pedes[ped] ! N, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[1].direction[S] = ButtonOn;
state = waitPLight1;
ch[1].pedes[ped] ! S, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[2].direction[E] = ButtonOn;
state = waitPLight2;
ch[2].pedes[ped] ! E, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[2].direction[W] = ButtonOn;
state = waitPLight2;
ch[2].pedes[ped] ! W, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[2].direction[N] = ButtonOn;
state = waitPLight2;
ch[2].pedes[ped] ! N, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[2].direction[S] = ButtonOn;
state = waitPLight2;
ch[2].pedes[ped] ! S, ped, ButtonOn;
}
:: state == waitPLight1 && ch[1].pedes[ped] ? [where, ped, white] ->
atomic { ch[1].pedes[ped] ? where, ped, white;
pLight[1].direction[where] = white;
state = idle;
pButton[1].direction[where] = ButtonOff;
}
:: state == waitPLight2 && ch[2].pedes[ped] ? [where, ped, white] ->
atomic { ch[2].pedes[ped] ? where, ped, white;
pLight[2].direction[where] = white;
state = idle;
pButton[2].direction[where] = ButtonOff;
}
od;
}
5.8 Restrictions
There are some limitation for the system, which can be viewed as restriction such as timers, and sensors that are not modeled.
Pedestrian can have his or her own choice on how much time he or she push the pButton[pid].direction[ ]. And also they can decide whether they need to wait or not after they push the Button. But for this system every Pedestrian is restricted to wait for the signal if he or she push it.
5.9 Formalizations
Here is the promela source
code for two pedestrians two intersections:
/****************************************************************
* File : system2.prom *
* Author: Gang Liu *
* Date: April 04, 1999 *
* Note: Model of the traffic control system (revised) *
****************************************************************/
/* This is the two pedestrians, two intersections version */
/* define the states of the PedestrianLight that may
waiting for the RoadLight */
#define idle 0
#define waitPLight 1
/* direction */
#define E 2
#define W 3
#define N 4
#define S 5
/* States of TrafficLight and PedestrianLight */
#define red 6
#define green 7
#define white 8
/* States of Button */
#define ButtonOn 9
#define ButtonOff 10
/* define the states of the Pedestrian who may
waiting for the RoadLight */
#define waitPLight1 19
#define waitPLight2 20
/* Buttons, PedestrianLights and RoadLights positions */
typedef array {
byte direction[11]
};
array pLight[3];
array pButton[3];
byte rLight[3];
/* channels */
typedef channel {
chan pedes[3] = [1] of {byte, byte, byte}
};
channel ch[3];
proctype RoadLight(byte pid) {
do
:: rLight[pid] == green ->
atomic {rLight[pid] = red;
pLight[pid].direction[E] = red;
pLight[pid].direction[W] = red;
}
:: rLight[pid] == red ->
atomic {rLight[pid] = green;
pLight[pid].direction[E] = red;
pLight[pid].direction[W] = red;
}
:: true -> skip
od
}
proctype Pedestrian(int ped) {
byte state, where, condi;
atomic { state = idle;
}
end:
do
:: state == idle -> state = idle
:: state == idle -> atomic { pButton[1].direction[E] = ButtonOn;
state = waitPLight1;
ch[1].pedes[ped] ! E, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[1].direction[W] = ButtonOn;
state = waitPLight1;
ch[1].pedes[ped] ! W, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[1].direction[N] = ButtonOn;
state = waitPLight1;
ch[1].pedes[ped] ! N, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[1].direction[S] = ButtonOn;
state = waitPLight1;
ch[1].pedes[ped] ! S, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[2].direction[E] = ButtonOn;
state = waitPLight2;
ch[2].pedes[ped] ! E, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[2].direction[W] = ButtonOn;
state = waitPLight2;
ch[2].pedes[ped] ! W, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[2].direction[N] = ButtonOn;
state = waitPLight2;
ch[2].pedes[ped] ! N, ped, ButtonOn;
}
:: state == idle -> atomic { pButton[2].direction[S] = ButtonOn;
state = waitPLight2;
ch[2].pedes[ped] ! S, ped, ButtonOn;
}
:: state == waitPLight1 && ch[1].pedes[ped] ? [where, ped, white] ->
atomic { ch[1].pedes[ped] ? where, ped, white;
pLight[1].direction[where] = white;
state = idle;
pButton[1].direction[where] = ButtonOff;
}
:: state == waitPLight2 && ch[2].pedes[ped] ? [where, ped, white] ->
atomic { ch[2].pedes[ped] ? where, ped, white;
pLight[2].direction[where] = white;
state = idle;
pButton[2].direction[where] = ButtonOff;
}
od;
}
proctype PedestrianLight(byte pid, pid2, ped, ped2) {
byte state, where, condi;
atomic { state = idle;
}
end:
do
:: rLight[pid] == red ->
atomic {
if
:: ch[pid].pedes[ped] ? [E, ped, ButtonOn] ->
ch[pid].pedes[ped] ? where, ped, condi;
ch[pid].pedes[ped] ! E, ped, white;
pLight[pid].direction[E] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped] ? [W, ped, ButtonOn] ->
ch[pid].pedes[ped] ? where, ped, condi;
ch[pid].pedes[ped] ! W, ped, white;
pLight[pid].direction[W] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped2] ? [E, ped2, ButtonOn] ->
ch[pid].pedes[ped2] ? where, ped2, condi;
ch[pid].pedes[ped2] ! E, ped2, white;
pLight[pid].direction[E] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped2] ? [W, ped2, ButtonOn] ->
ch[pid].pedes[ped2] ? where, ped2, condi;
ch[pid].pedes[ped2] ! W, ped2, white;
pLight[pid].direction[W] = white;
state = idle
:: else
fi;
}
:: rLight[pid] == red && rLight[pid2] == green ->
state = waitPLight
:: rLight[pid2] == red && rLight[pid] == green ->
state = waitPLight
:: rLight[pid] == red && rLight[pid2] == green ->
atomic {if
:: ch[pid].pedes[ped] ? [N, ped, ButtonOn] ->
ch[pid].pedes[ped] ? where, ped, condi;
ch[pid].pedes[ped] ! N, ped, white;
pLight[pid].direction[N] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped] ? [S, ped, ButtonOn] ->
ch[pid].pedes[ped] ? where, ped, condi;
ch[pid].pedes[ped] ! S, ped, white;
pLight[pid].direction[S] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped2] ? [N, ped2, ButtonOn] ->
ch[pid].pedes[ped2] ? where, ped2, condi;
ch[pid].pedes[ped2] ! N, ped2, white;
pLight[pid].direction[N] = white;
state = idle
:: else
fi;
if
:: ch[pid].pedes[ped2] ? [S, ped2, ButtonOn] ->
ch[pid].pedes[ped2] ? where, ped2, condi;
ch[pid].pedes[ped2] ! S, ped2, white;
pLight[pid].direction[S] = white;
state = idle
:: else
fi;
}
od
}
init{
atomic {int i = 0; int j = 0;
do
:: i <=1 -> j = 0; i++;
do
:: j <= 10 ->
pLight[i].direction[j] = red;
pButton[i].direction[j] = ButtonOff;
j++;
:: else -> break
od;
rLight[i] = green;
::else -> break
od;
}
atomic {run RoadLight(1);
run RoadLight(2);
run Pedestrian(1);
run Pedestrian(2);
run PedestrianLight(1, 2, 1, 2);
run PedestrianLight(2, 1, 1, 2);
}
}
5.10 Validation
Deadlock check:
pan: out of memory 2.87064e+08 bytes used 102400 bytes more needed 5.36871e+08 bytes limit (2^MEMCNT) hint: to reduce memory, recompile with -DCOLLAPSE # good, fast compression, or -DMA=224 # better/slower compression, or -DBITSTATE # supertrace (Spin Version 3.0.9 -- 11 January 1998) Warning: Search not completed + Partial Order Reduction Full statespace search for: never-claim - (not selected) assertion violations + cycle checks - (disabled by -DSAFETY) invalid endstates + State-vector 224 byte, depth reached 1450091, errors: 0 820392 states, stored 1.59498e+06 states, matched 2.41537e+06 transitions (= stored+matched) 2.28695e+06 atomic steps hash conflicts: 1.02208e+06 (resolved) (max size 2^19 states) Stats on memory usage (in Megabytes): 190.331 equivalent memory usage for states (stored*(State-vector + overhead)) 157.660 actual memory usage for states (compression: 82.83%) State-vector as stored = 184 byte + 8 byte overhead 2.097 memory used for hash-table (-w19) 120.000 memory used for DFS stack (-m5000000) 287.064 total actual memory usage real 6:40.2 user 1:11.5 sys 8.3No deadlock so far, but the system is too big to verify.
Simulation for the system. The FSM of this system is also available for Pedestrian, PedestrianLight and RoadLight.
5.11 Specification and Verification
1.
Requirement:
When
the push the button to request to cross the street, his/her state will
remain waitPLight until the button is off.
Observables:
pButton[pid].direction[N],
state[ped]
Refinement:
AFTER
pButton[pid].direction[N] is ButtonOn and BEFORE pButton[pid].direction[N]
is ButtonOff, state[ped] ALWAYS be waitPLight[pid]
Pattern and scope:
Universality,
Between
Specification:
LTL: [ ] (( Q & <> R) -> P U R)
[ ] ((
pButton[pid].direction[N] == ButtonOn & <>pButton[pid].direction[N]
== ButtonOff) ->
(state[ped]
== waitPLight[pid] U pButton[pid].direction[N] == ButtonOff)
warning: for p.o. reduction to be valid the never claim must be stutter-closed (never claims generated from LTL formulae are stutter-closed) pan: out of memory 1.34137e+08 bytes used 102400 bytes more needed 1.34218e+08 bytes limit (2^MEMCNT) hint: to reduce memory, recompile with -DCOLLAPSE # good, fast compression, or -DMA=220 # better/slower compression, or -DBITSTATE # supertrace (Spin Version 3.0.9 -- 11 January 1998) Warning: Search not completed + Partial Order Reduction Full statespace search for: never-claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates - (disabled by never-claim) State-vector 220 byte, depth reached 874254, errors: 0 565076 states, stored 1.2897e+06 states, matched 1.85477e+06 transitions (= stored+matched) 1.55911e+06 atomic steps hash conflicts: 4.12536e+06 (resolved) (max size 2^16 states) Stats on memory usage (in Megabytes): 128.837 equivalent memory usage for states (stored*(State-vector + overhead)) 106.329 actual memory usage for states (compression: 82.53%) State-vector as stored = 180 byte + 8 byte overhead 0.262 memory used for hash-table (-w16) 24.000 memory used for DFS stack (-m1000000) 134.137 total actual memory usage real 1:23.2 user 1:08.0 sys 3.12.
warning: for p.o. reduction to be valid the never claim must be stutter-closed (never claims generated from LTL formulae are stutter-closed) pan: out of memory 6.70654e+07 bytes used 102400 bytes more needed 6.71089e+07 bytes limit (2^MEMCNT) hint: to reduce memory, recompile with -DCOLLAPSE # good, fast compression, or -DMA=220 # better/slower compression, or -DBITSTATE # supertrace (Spin Version 3.0.9 -- 11 January 1998) Warning: Search not completed + Partial Order Reduction Full statespace search for: never-claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates - (disabled by never-claim) State-vector 220 byte, depth reached 203502, errors: 0 222796 states, stored 561348 states, matched 784144 transitions (= stored+matched) 716902 atomic steps hash conflicts: 666578 (resolved) (max size 2^16 states) Stats on memory usage (in Megabytes): 50.797 equivalent memory usage for states (stored*(State-vector + overhead)) 41.927 actual memory usage for states (compression: 82.54%) State-vector as stored = 180 byte + 8 byte overhead 0.262 memory used for hash-table (-w16) 24.000 memory used for DFS stack (-m1000000) 67.065 total actual memory usage real 30.2 user 27.5 sys 1.23.
Observables:
rLight[pid],
pLight[pid].direction[N]
Refinement:
It never
happen that rLight[pid] is green and the pLight[pid].direction[N] is white
Pattern and scope:
Absence,
Globally
Specification:
LTL: [ ] (!P)
[ ] (!
pLight[pid].direction[N] == white && rLight[pid] == green)
warning: for p.o. reduction to be valid the never claim must be stutter-closed (never claims generated from LTL formulae are stutter-closed) error: max search depth too small pan: out of memory 3.34668e+07 bytes used 102400 bytes more needed 3.35544e+07 bytes limit (2^MEMCNT) hint: to reduce memory, recompile with -DCOLLAPSE # good, fast compression, or -DMA=220 # better/slower compression, or -DBITSTATE # supertrace (Spin Version 3.0.9 -- 11 January 1998) Warning: Search not completed + Partial Order Reduction Full statespace search for: never-claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates - (disabled by never-claim) State-vector 220 byte, depth reached 9999, errors: 0 164473 states, stored 299415 states, matched 463888 transitions (= stored+matched) 358668 atomic steps hash conflicts: 25088 (resolved) (max size 2^19 states) Stats on memory usage (in Megabytes): 37.500 equivalent memory usage for states (stored*(State-vector + overhead)) 30.958 actual memory usage for states (compression: 82.56%) State-vector as stored = 180 byte + 8 byte overhead 2.097 memory used for hash-table (-w19) 0.240 memory used for DFS stack (-m10000) 33.467 total actual memory usage real 17.1 user 15.7 sys 0.5
4.
Requirement:
When
traffic light is green, pedestrian light should never be white
Observables:
rLight[pid],
pLight[pid].driection[N]
Refinement:
It NEVER
happens that rLight[pid] is green and at the same time pLight is white
Pattern and scope:
Absence,
Globally
Specification:
LTL: [ ] (! P)
[ ] (!
( rLight[pid] == green && pLight[pid].direction[N] == white)
warning: for p.o. reduction to be valid the never claim must be stutter-closed (never claims generated from LTL formulae are stutter-closed) error: max search depth too small pan: out of memory 3.34668e+07 bytes used 102400 bytes more needed 3.35544e+07 bytes limit (2^MEMCNT) hint: to reduce memory, recompile with -DCOLLAPSE # good, fast compression, or -DMA=220 # better/slower compression, or -DBITSTATE # supertrace (Spin Version 3.0.9 -- 11 January 1998) Warning: Search not completed + Partial Order Reduction Full statespace search for: never-claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates - (disabled by never-claim) State-vector 220 byte, depth reached 9999, errors: 0 164634 states, stored (164769 visited) 482699 states, matched 647468 transitions (= visited+matched) 392525 atomic steps hash conflicts: 21342 (resolved) (max size 2^19 states) Stats on memory usage (in Megabytes): 37.537 equivalent memory usage for states (stored*(State-vector + overhead)) 30.989 actual memory usage for states (compression: 82.56%) State-vector as stored = 180 byte + 8 byte overhead 2.097 memory used for hash-table (-w19) 0.240 memory used for DFS stack (-m10000) 33.467 total actual memory usage real 15.8 user 14.7 sys 0.4
5.
Requirement:
There
exists that two traffic lights of two intersections are both green or both
red.
Observables:
rLight[pid]
Refinement:
There
EXISTS that rLight[1] and rLight[2] are both red or both green.
Pattern and scope:
Existence,
Globally
Specification:
LTL: <> (P)
<>
((rLight[1] == red && rLight[2] == red) || (rLight[1] == green
&& rLight[2] == green))
warning: for p.o. reduction to be valid the never claim must be stutter-closed (never claims generated from LTL formulae are stutter-closed) (Spin Version 3.0.9 -- 11 January 1998) + Partial Order Reduction Full statespace search for: never-claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates - (disabled by never-claim) State-vector 176 byte, depth reached 103, errors: 0 2 states, stored 0 states, matched 2 transitions (= stored+matched) 101 atomic steps hash conflicts: 0 (resolved) (max size 2^19 states) 2.542 memory usage (Mbyte) real 0.0 user 0.0 sys 0.0
6.
Requirement:
If pedestrian
crossing light is white it will eventually change to red
Observables:
pLight[pid].direction[N]
Refinement:
The state
that pLight[pid].direction[N] is white will LEAD-TO a state that pLight[pid].direction[N]
is red
Pattern and scope:
Response,
Globally
Specification:
LTL: [ ] ( P -> <> S)
[ ] (
pLight[pid].direction[N] == white -> <> pLight[pid].direction[N] ==
red)
warning: for p.o. reduction to be valid the never claim must be stutter-closed (never claims generated from LTL formulae are stutter-closed) error: max search depth too small pan: out of memory 3.34668e+07 bytes used 102400 bytes more needed 3.35544e+07 bytes limit (2^MEMCNT) hint: to reduce memory, recompile with -DCOLLAPSE # good, fast compression, or -DMA=220 # better/slower compression, or -DBITSTATE # supertrace (Spin Version 3.0.9 -- 11 January 1998) Warning: Search not completed + Partial Order Reduction Full statespace search for: never-claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid endstates - (disabled by never-claim) State-vector 220 byte, depth reached 9999, errors: 0 164634 states, stored (164769 visited) 482699 states, matched 647468 transitions (= visited+matched) 392525 atomic steps hash conflicts: 21342 (resolved) (max size 2^19 states) Stats on memory usage (in Megabytes): 37.537 equivalent memory usage for states (stored*(State-vector + overhead)) 30.989 actual memory usage for states (compression: 82.56%) State-vector as stored = 180 byte + 8 byte overhead 2.097 memory used for hash-table (-w19) 0.240 memory used for DFS stack (-m10000) 33.467 total actual memory usage real 15.8 user 14.7 sys 0.4
6. References
1. Marciniak, J.J. (ed.), Encyclopedia of Software Enineering, Wiley,
1994
2. http://shemesh.larc.nasa.gov/fm/fm-what.html
3. M. Huth and M. Ryan, Logic in Computer Science: Modelling and reasoning
about systems, Cambridge University Press, 1999
4. G.J. Holzmann, Design and Validation of Computer Protocols, Prentice
Hall, New Jersey, 1991
5. G.J. Holzmann, "Using SPIN", 1995, http://gd.tuwien.ac.at/plan9/doc/spin.html.
6. G.J. Holzmann, "The Spin Model Checker, IEEE Trans. on Software
Engineering, Vol. 23, No. 5, May 1997, pp. 279-295.
7. J. Herzog, Introduction to Formal Verification, 1997 http://www.math.hmc.edu/~jpl/intro.html.
8. J. Herzog, Model Checkers, 1996, http://www.math.hmc.edu/~jpl/modelcheckers.html.
9. J. Herzog, SPIN,1996, http://www.math.hmc.edu/~jpl/reviews/spinreview.html.
10. J. Herzog, SMV, 1996, http://www.math.hmc.edu/~jpl/reviews/smvreview.html.
11. SPIN Verifier's Roadmap: Building and Verifying SPIN Models, 1997,
http://cm.bell-labs.com/cm/cs/what/spin/Man/Roadmap.html.
12. Sheila Anderson, et. al., A Tutorial in Model Checking, http://www.cis.ksu.edu/~afrand/cis841/modelchecking/models.html
13. M. B. Dwyer. Data Flow Analysis Frameworks for Concurrent Programs,
KSU, 1995.
14. M. B. Dwyer and L. A. Clarke, Data Flow Analysis for Verifying
Properties of Concurrent Programs, Proceedings of the Second ACM SIGSOFT
Symposium on Foundations of Software Engineering, New Orleans, LA, December
1994, pp. 62-75.
15. Formal Methods, http://archive.comlab.ox.ac.uk/formal-methods.html
16. C. S. Pasareanu, M. B. Dwyer and M. Huth, Modular Verificaiton
of Software Units, KSU, 1998
17. K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers,
1993
18. Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent
Systems: Specification, Springer-Verlag, 1991
19. C. S. Pasareanu, M. B. Dwyer, Software Model Checking Case Studies,
http://www.cis.ksu.edu/santos/bandera/index.html
20. R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper, Simple On-the-fly
Automatic Verification of Linera Temporal Logic, Proceedings of PSTV'95,
1995
21. SMV reference, http://www.cis.ksu.edu/santos/smv-doc/
22. Spin Online References, http://cm.bell-labs.com/cm/cs/what/spin/Man/index.html
23. A Specification Pattern System, http://www.cis.ksu.edu/santos/spec-patterns
24. Promela Language Reference, http://cm.bell-labs.com/cm/cs/what/spin/Man/promela.html
7. Glossary
assertion
An assertion is any statement that is supposed to be true at a particular
time in the operations of the system. Usually describes the state of the
system or the values of variables within the system in non-trivial ways.
code
A program written in an actual programming language; any use of a compilable,
translatable, or interpretable language- as opposed to specification languages
in which a system can be described but not executed.
correctness
Correctness is a concept with which most people are familiar in vague,
general terms; this is the way in which it is usually used here.
In its broadest sense, it includes something of the notion that the
program does what it was intended to do; in more specific use, it usually
means that the program conforms to its specifications.
deadlock
Deadlock is a condition in which two or more mutually dependent processes
are prevented by their dependence from proceeding. The states in which
no further protocol execution is possible, for instance because all protocol
processes are waiting for conditions that can never be fulfilled.
For example, if four cars simultaneously arrive at an intersection,
they could theoretically remain there forever. Deadlock is generally considered
something to avoid.
design tools
Design tools are programs used in developing a system from scratch.
By providing an environment in which to develop specifications or the program
itself, the tools can apply formal methods behind the scenes to ensure
that the system being developed is correct.
finite state machine
A finite state machine is a representation of a computer system as
a series of states and the transitions that take the system from one state
to another. Although the number of states can be quite large, many systems
can be modeled as one of these machines.
formal methods
Refers to applying rigorous mathematical methods, usually those found
in mathematical logic, to developing and testing computer programs.
improper terminations
The completion of a protocol execution without satisfying the proper
termination conditions.
initial conditions
Conditions which must be met before an operation or series of operations
can begin. For example, a division function might have the initial condition
that the divisor is not zero.
invariant
An invariant is a type of assertion that describes a relationship between
variables that holds as the values of those variables change. A special
type of invariant is the loop invariant.
livelock
ececution sequences that can be repeated indefinitely often without
ever making effective progress.
loop invariant
A loop invariant is type of assertion that remains true from one repetition
of the loop to the next. Usually, the invariant describes some non-trivial
relationship between the variables changed by the loop. For example, if
a program has a loop which adds one to inc and subtracts one from dec then
the sum of inc and dec will be a constant. Loop invariants are a common
type of invariant.
model checker
A model checker is a program that works by examining a piece of code
or a specification and reducing it to a finite-state machine.
Once this is done, it examines the space of states, looking for invariant-violations,
deadlocks, and other types of situations.
non-progress loop
A non-progress loop in a loop in which no work gets done. 'Work' in
this sense is defined by the designer, and would include any operations
that bring the system closer to terminating.
postcondition
A postcondition is something which is true or expected to be true upon
completion of a program or fragment thereof. The most common postconditions
are halting and the returning of correct values.
precondition
A precondition is something which is true or expected to be true when
a program or fragment of a program is called. For example, one would not
expect to call a 'divide' function with 0 as the denominator.
proof checker
A proof checker works much the same way that a mathematical proof works.
By using a piece of code or a specification as a starting place, it successively
applies rules of logic or mathematics until it deduces the desired goal.
specification
A specification a description of what a program should do; this can
be informal or formal. Informal specifications are usually in English,
and formal specifications are expressed in a formal specification language.
Specification design occurs before the program is written.
specification checker
Specification checkers work on a high-level specification language.
The specification language usually has two components:
statements that describe what the system will do, and assertions that
describe the states the system should be in at a given point.
The tool then attempts to show that if the system acts as described,
then the assertions will in fact hold.
specification checking
At the specification level: checking to make
sure that the formal specifications match the designers' ideas of what
the program will do
At the code level: checking to make sure that
the program matches its formal specifications.
state
A state is one instance of the totality of assignments to variables
in the system, including the flow of control and other 'environment' variables.
One concrete example of a way in which the system can be. All operations
in a system are transitions from one state to another.
theorem prover
A theorem prover attempts to generate automatically a proof of a given
conjecture. Theorem provers are distinct from proof checkers in that a
theorem prover generates a proof automatically; a proof checker requires
user input in order to generate a proof.
A theorem prover has the advantage of requiring less input from the
user, but a proof checker has the advantage of giving the user more control
over the direction of the proof.
validation
Validation is the act of checking to make sure that a program does
what is expected of it; includes verification, testing, and any other steps
taken to insure the correctness of the system. As with verification, this
process generally occurs during and after the writing of a program.
verification
Verification is the act of formally showing the system to operate correctly.
Includes the use of verification tools, proving code by hand, and other
formal processes.
1.What is the main concept behind "formal methods"?
a.Verifying software by prototyping.
b.Verifying software by mathematical
logic.
c.Verifying software by modeling.
2.Formal verirfication allows the designer to focus on
a.what the system does.
b.how the system works.
3.Generally, formal verification is considered to have two types of
approaches:
a.System Verification & Feature
Verification
b.Design Verification & Program
Verification
4.Model checking is a method used in which approach of formal verification?
a.System Verification
b.Feature Verification
c.Design Verification
d.Program Verification
5.