Transcript Bandera Overview: ICSE00 talk

CIS 842: Specification and
Verification of Reactive Systems
Lecture 7: Demonstration of Basic Aspects
of the Bandera Tool Set
Copyright 2001, Matt Dwyer, John Hatcliff, and Radu Iosif. The syllabus and all lectures for this course are copyrighted
materials and may not be used in other course settings outside of Kansas State University in their current form or modified
form without the express written permission of one of the copyright holders. During this course, students are prohibited
from selling notes to or being paid for taking notes by any person or commercial firm without the express written
permission of one of the copyright holders.
Notes

Demo examples are chosen to be simple and
to illustrate tool components
 For more examples with interesting
specifications, see…
– Bandera tutorial…
– Extended version of SPIN’00 paper
• complete presentation of BoundedBuffer example
• Doug Lea’s Readers/Writers
• Publish/Subscribe framework from java.util
Outline

Concept of a session
– configuring Bandera for a run

Simple deadlock example
– illustrates session, code display,
counterexample navigation, and slicing

Pipeline example
– illustrates creating a temporal specification,
slicing, and abstraction
Configuring Bandera
A run of Bandera is configured by a session specification
A session specifies...
which Java files to take as input
which property to check
which tool components (e.g., slicer, abstraction) to
invoke
which backend model-checker to use
…other options
A session file holds several related sessions
sessions in session file can be executed in batch mode
or individually selected in the BUI.
Simple Deadlock Example
Process 1
Process 2
acquisition
acquisition
Lock 1
Lock 2
blocked
acquisition
blocked
acquisition
Simple Deadlock Example
public class Deadlock {
static Lock lock1;
static Lock lock2;
static int state;
public static
void main(String[] args) {
lock1 = new Lock();
lock2 = new Lock();
Process1 p1
= new Process1();
Process2 p2
= new Process2();
p1.start();
p2.start();
}
class Lock {}
class Process1 extends Thread {
public void run() {
Deadlock.state++;
synchronized (Deadlock.lock1) {
synchronized (Deadlock.lock2) {
Deadlock.state++;
}}}}
class Process2 extends Thread {
public void run() {
Deadlock.state++;
synchronized (Deadlock.lock2) {
synchronized (Deadlock.lock1) {
Deadlock.state++;
}}}}
Deadlock Example Artifacts
Abstracted Java
Point.java
Property Tool
Abstraction
Analyses Engine
BIRC
Translators
BIR
SPIN
.trail
dSPIN
Java
Jimple
Parser
SMV
Slicer
Error Trace Display
Sliced Java
Simulator
JPF
Pipeline Example
Requirements:
If main in PipeInt signals
shutdown (by calling the stop
method of c1), then Stage x
eventually shuts down.
Shutdown Actions:
c1.stop
c2.stop
..send 0
PipeInt
..send 0
Stage1
c1
1..100
c3.stop
>0: + 1
=0: stop
c4.stop
..send 0
Stage2
c2
>0: + 1
=0: stop
..send 0
Stage3
c3
>0: + 1
=0: stop
Connectors
…if stop received, send out 0
Listener
c4
..print
Pipeline Example
class PipeInt {
/**
* @observable predset1
Observable
*
LOCATION[main1] mainStop;
*/
static public void main (String[] args) {
Heap.c1 = new Connector();
Heap.c2 = new Connector();
Heap.c3 = new Connector();
Heap.c4 = new Connector();
(new
(new
(new
(new
Stage1()).start();
Stage2()).start();
Stage3()).start();
Listener()).start();
for (int i = 1; i < 100; i++)
Heap.c1.add(i);
main1:
Heap.c1.stop();
}
}
Pipeline Example
final class Stage1 extends Thread {
/**
* @observable predset1
Observable
*
LOCATION[run1] stage1Shutdown;
*/
public void run() {
System.out.println("Stage1 startup");
int tmp = -1;
while (tmp != 0) {
if ((tmp = Heap.c1.take()) != 0)
Heap.c2.add(tmp + 1);
}
Heap.c2.stop();
run1:
System.out.println("Stage1 shutdown");
}
}
Pipeline Example
final class Connector {
int queue = -1; /* represents empty queue */
public final synchronized int take() {
int value;
while (queue < 0) /* wait ‘til not empty */
try {
wait();
} catch (InterruptedException ex) {}
value = queue; /* get value to send out */
queue = -1;
/* set queue to empty
*/
return value; /* send out value
*/
}
public final synchronized void add(int value) {
queue = value;
notifyAll();
}
Pipeline Example Specification
Requirements:
If main in PipeInt signals
shutdown (by calling the stop
method of c1), then Stage x
eventually shuts down.
For hints on how to construct the
specification, a user might consult the
Specification Patterns Webpage
…an example of the response or
leads to pattern with global scope
BSL Specification (for first stage shutdown):
forall[s:Stage1].
{stage1Shutdown(s)} responds to {mainStop} globally;