Examples
Each example is stored in different folders and
contains a 'README' file with running explanations.
Download the examples
Details:
Model | #TAs | #Clocks | Observer | |
#Loc | #Trans | |||
Pipe6 | 13 | 14 | 15 | 197 |
Pipe7 | 15 | 16 | 17 | 227 |
Fddi10 | 21 | 32 | 21 | 221 |
RemoteBR | 12 | 13 | 29 | 395 |
MinePump | 8 | 8 | 9 | 58 |
Struct | 6 | 7 | 8 | 50 |
Pipe6 and Pipe7 are pipe-lines of sporadic processes that forward
a signal emitted by a quasi periodic source (6 and 7 stages
resp.). The observer captures a scenario violating an end-to-end constraint for
signal propagation.
Pipe6 observer.
Pipe6 activity tables.
Obs | Revelant Components | Relevant Clocks | ||||||||||||||||||||||||||
0 | observer6 | f120 | l1 | l2 | l3 | l4 | l5 | l6 | p1 | p2 | p3 | p4 | p5 | p6 | S | X1 | X2 | X3 | X4 | X5 | X6 | Z1 | Z2 | Z3 | Z4 | Z5 | Z6 | |
1 | observer6 | l1 | l2 | l3 | l4 | l5 | l6 | p1 | p2 | p3 | p4 | p5 | p6 | R | X1 | X2 | X3 | X4 | X5 | X6 | Z1 | Z2 | Z3 | Z4 | Z5 | Z6 | ||
2 | observer6 | l2 | l3 | l4 | l5 | l6 | p1 | p2 | p3 | p4 | p5 | p6 | R | X2 | X3 | X4 | X5 | X6 | Z1 | Z2 | Z3 | Z4 | Z5 | Z6 | ||||
3 | observer6 | l2 | l3 | l4 | l5 | l6 | p2 | p3 | p4 | p5 | p6 | R | X2 | X3 | X4 | X5 | X6 | Z2 | Z3 | Z4 | Z5 | Z6 | ||||||
4 | observer6 | l3 | l4 | l5 | l6 | p2 | p3 | p4 | p5 | p6 | R | X3 | X4 | X5 | X6 | Z2 | Z3 | Z4 | Z5 | Z6 | ||||||||
5 | observer6 | l3 | l4 | l5 | l6 | p3 | p4 | p5 | p6 | R | X3 | X4 | X5 | X6 | Z3 | Z4 | Z5 | Z6 | ||||||||||
6 | observer6 | l4 | l5 | l6 | p3 | p4 | p5 | p6 | R | X4 | X5 | X6 | Z3 | Z4 | Z5 | Z6 | ||||||||||||
7 | observer6 | l4 | l5 | l6 | p4 | p5 | p6 | R | X4 | X5 | X6 | Z4 | Z5 | Z6 | ||||||||||||||
8 | observer6 | l5 | l6 | p4 | p5 | p6 | R | X5 | X6 | Z4 | Z5 | Z6 | ||||||||||||||||
9 | observer6 | l5 | l6 | p5 | p6 | R | X5 | X6 | Z5 | Z6 | ||||||||||||||||||
10 | observer6 | l6 | p5 | p6 | R | X6 | Z5 | Z6 | ||||||||||||||||||||
11 | observer6 | l6 | p6 | R | X6 | Z6 | ||||||||||||||||||||||
12 | observer6 | p6 | R | Z6 | ||||||||||||||||||||||||
13 | observer6 | |||||||||||||||||||||||||||
14 | observer6 |
Fddi10 is an extension of the FDDI token Model ring protocol where the
observer monitors the time
the token takes to return to a given station.
RemoteBR is a design composed of a central component and two remote
sensors. When the central component needs sampled data, it broadcasts a request
to the sensors. Each sensor handles requests by reading the last stored value by
the sampler and sending it back to the central component. There, the readings
are paired for further processing. The observer captures scenarios where a
request for collecting a pair of data items is not fully answered in less than a
given amount of time.
RemoteBR scenario speficifaction in VTS.
Obs | Revelant Components | Relevant Clocks | |||||||||||||||||||
0 | obsbr | netv1 | netv2 | pair | requester | lpair | l1 | l2 | reader1 | reader2 | netrqst | N1 | N2 | P | PA | R1 | R2 | S | X1 | X2 | X_RQSTSENT |
1 | obsbr | ||||||||||||||||||||
2 | obsbr | netv1 | netv2 | pair | lpair | l1 | l2 | reader1 | reader2 | netrqst | N1 | N2 | P | PA | R1 | R2 | X1 | X2 | X_RQSTSENT | ||
3 | obsbr | netv1 | netv2 | pair | lpair | l1 | l2 | reader1 | reader2 | netrqst | N1 | N2 | P | PA | R1 | R2 | X1 | X2 | X_RQSTSENT | ||
4 | obsbr | netv1 | netv2 | pair | lpair | l2 | reader1 | reader2 | netrqst | N1 | N2 | P | PA | R1 | R2 | X2 | X_RQSTSENT | ||||
5 | obsbr | netv1 | netv2 | pair | lpair | l2 | reader2 | netrqst | N1 | N2 | P | PA | R2 | X2 | X_RQSTSENT | ||||||
6 | obsbr | netv2 | pair | lpair | l2 | reader2 | netrqst | N2 | P | PA | R2 | X2 | X_RQSTSENT | ||||||||
7 | obsbr | netv2 | pair | lpair | l2 | reader2 | P | PA | R2 | X2 | X_RQSTSENT | ||||||||||
8 | obsbr | netv2 | pair | lpair | reader2 | P | PA | R2 | X_RQSTSENT | ||||||||||||
9 | obsbr | netv2 | pair | lpair | P | PA | X_RQSTSENT | ||||||||||||||
10 | obsbr | pair | lpair | PA | X_RQSTSENT | ||||||||||||||||
11 | obsbr | pair | X_RQSTSENT | ||||||||||||||||||
12 | obsbr | ||||||||||||||||||||
13 | obsbr | netv1 | netv2 | pair | lpair | l2 | reader2 | N2 | P | PA | R2 | X2 | X_RQSTSENT | ||||||||
14 | obsbr | netv1 | netv2 | pair | lpair | reader2 | N2 | P | PA | R2 | X_RQSTSENT | ||||||||||
15 | obsbr | netv1 | netv2 | pair | lpair | N2 | P | PA | X_RQSTSENT | ||||||||||||
16 | obsbr | netv1 | pair | lpair | P | PA | X_RQSTSENT | ||||||||||||||
17 | obsbr | netv1 | netv2 | pair | lpair | l2 | reader1 | reader2 | N2 | P | PA | R1 | R2 | X2 | X_RQSTSENT | ||||||
18 | obsbr | netv1 | netv2 | pair | lpair | reader1 | reader2 | N2 | P | PA | R1 | R2 | X_RQSTSENT | ||||||||
19 | obsbr | netv1 | netv2 | pair | lpair | reader1 | N2 | P | PA | R1 | X_RQSTSENT | ||||||||||
20 | obsbr | netv1 | pair | lpair | reader1 | P | PA | R1 | X_RQSTSENT | ||||||||||||
21 | obsbr | netv1 | netv2 | pair | lpair | l1 | l2 | reader1 | reader2 | N2 | P | PA | R1 | R2 | X1 | X2 | X_RQSTSENT | ||||
22 | obsbr | netv1 | netv2 | pair | lpair | l1 | reader1 | reader2 | N2 | P | PA | R1 | R2 | X1 | X_RQSTSENT | ||||||
23 | obsbr | netv1 | netv2 | pair | lpair | l1 | reader1 | N2 | P | PA | R1 | X1 | X_RQSTSENT | ||||||||
24 | obsbr | netv1 | pair | lpair | l1 | reader1 | P | PA | R1 | X1 | X_RQSTSENT | ||||||||||
25 | obsbr | netv1 | netv2 | pair | lpair | l1 | l2 | reader1 | reader2 | netrqst | N1 | N2 | P | PA | R1 | R2 | X1 | X2 | X_RQSTSENT | ||
26 | obsbr | netv1 | netv2 | pair | lpair | l1 | reader1 | reader2 | netrqst | N1 | N2 | P | PA | R1 | R2 | X1 | X_RQSTSENT | ||||
27 | obsbr | netv1 | netv2 | pair | lpair | l1 | reader1 | netrqst | N1 | N2 | P | PA | R1 | X1 | X_RQSTSENT | ||||||
28 | obsbr | netv1 | pair | lpair | l1 | reader1 | netrqst | N1 | P | PA | R1 | X1 | X_RQSTSENT |
Minepump is a design of a fault-detection mechanism for a distributed
mine-drainage controller. A watchdog task periodically checks the
availability of a water level sensor device by sending a request and extracting
acks that were received and queued during the previous cycle by another sporadic
task. When the watchdog finds the queue empty, it registers a fault condition in
a shared memory which is periodically read, and forwarded to a remote console,
by a proxy task. The observer checks if the failure of high-low water sensor is
always informed to the remote operator before a given deadline.
Struct is an adaptation of a well-know working design: the active
structural control system that limits structural vibration due to earthquakes or
strong winds. The pulse-control algorithm is mapped into two tasks: the Modeler
and the Pulser. The Modeler is a sporadic task
which, once initialized, serves the messages arriving from the sensor. Then, it
updates in a predictive fashion a model stored in a shared protected object
Model and starts a new communication with the sensor to be served in the next
invocation. The Pulser periodically (110 time units (t.u.)) reads the model,
calculates the pulse magnitude and starts a communication with the actuator (which
in turn will expand to counteract external forces). The sampling takes within 50
and 55 t.u., then the data is prepared within 10 t.u. The actuator applies the
pulse for a duration within 25 to 30 t.u., and then data is prepared for
communication (10. t.u. aswell). The Comm component models handshake
communication where it takes within 3 and 5 t.u. to perform the communication (message
and acknowledgement).