-
Overview
Sigref is a novel tool for the bisimulation minimization of labelled transition systems. The novelty of Sigref is that it is designed for symbolic representations of labelled transition systems (i.e., using BDDs). Sigref supports several notions of bisimulation equivalence, among which are the most prominent ones, e.g., strong, weak, and branching bisimulation. The most appealing property of Sigref is that all supported bisimulation types are handled within a uniform framework based on signatures. Hence, Sigref is also easily extendible to new types of bisimulation by just formulating the appropriate signature. The development of Sigref is tightly coupled to AVACS::S3, a sub-project of the German Transregional Colloborative Research Center 14 AVACS, devoted to Automatic Verification and Analysis of Complex Systems. For details, please check [www.avacs.org]
-
Publications
The following publications contain details about the implementation and performance of Sigref:
-
M. Herbstritt, R. Wimmer, T. Peikenkamp, E. Böde, M. Adelaide, S. Johr, H. Hermanns, B. Becker
Analysis of Large Safety-Critical Systems: A Quantitative Approach
Reports of SFB/TR 14 AVACS Nr. 8 (siehe www.avacs.org), 2006, ISSN 1860-9821 (pdf, bibtex) -
R. Wimmer, M. Herbstritt, B. Becker
Minimization of Large State Spaces using Symbolic Branching Bisimulation
Proceedings of the 9th IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems, April 2006 (pdf@IEEE-Xplore, bibtex) -
Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr,
Thomas Peikenkamp, Reza Pulungan, Ralf Wimmer, Bernd Becker
Compositional Performability Evaluation for Statemate
Proceedings of the 3rd International Conference on Quantitative Evaluation of Systems (QEST), Sept. 2006 (bibtex)
R. Wimmer, M. Herbstritt, H. Hermanns, K. Strampp, B. Becker
Sigref - A Symbolic Bisimulation Tool Box
Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), October 23-26, 2006, Beijing, China (pdf@Springer, bibtex) -
M. Herbstritt, R. Wimmer, T. Peikenkamp, E. Böde, M. Adelaide, S. Johr, H. Hermanns, B. Becker
Further publications related to AVACS can be obtained from the [AVACS publication browser]
Benchmarks
The following examples were mentioned in our current submission to TACAS 2007. The xml-files contain the BDD description for the labelled transition system. For the Statemate examples, there is also a brief description available.
| model description | xml-file |
|---|---|
| ETCS-1 | etcs-1.xml |
| ETCS-2 | etcs-2.xml |
| ETCS-3 | etcs-3.xml |
| BS-P | bs-p.xml |
| Kanban-4 | kanban-4.xml |
| Kanban-5 | kanban-5.xml |
| Kanban-6 | kanban-6.xml |
| Kanban-7 | kanban-7.xml |
| Kanban-8 | kanban-8.xml |
| Kanban-9 | kanban-9.xml |
| Milner-4 | milner-4.xml |
| Milner-5 | milner-5.xml |
| Milner-6 | milner-6.xml |
| Milner-7 | milner-7.xml |
| Milner-8 | milner-8.xml |
A DTD for the xml-format can be found [here].
Software Download
Sigref is publicly available, but please respect our wish to know to whom
we have distributed the software. Hence, we really appreciate that you complete the
following formular. After submitting the data, you will be directed to a website
for downloading Sigref. Your submitted data will be kept secure.
Model descriptions
ETCS models
Overview
Overview
The model targets the problem of having more than one train on
the same track. It is scalable so that arbitrary many trains can
be handled. The analysis should check the collision of trains.
In this work we focused on three instantiations having
one, two, or three trains.
There is a controlling unit for the track, named RBC (Radio Block Center).
This unit and the working principle are part of the ETCS
(European Train Control System) standard (see e.g.
[ERTMS/ETCS]).
This controller works that way
that it gets the actual position of each moving train. To authorize a train
to move on, it sends an authorization message. The idea is that the RBC
only sends a moving authorization if it got the position from the previous
train. Since a train is only allowed to send its new position if it is
moving, each train can only move if the previous trains did already move
before.
With these assumptions (which are made to simplify the model) that a
train can either move with full speed or doesn't move, and that the
track the train is moving after getting a authorization from the RBC
is constant, the safety requirement is much more simple (and needs no
calculation of the exact position of one train): The train is safe if
it only moves after getting the authorization from the RBC and if the
RBC only sends a new authorization if it got an position notification
from the previous train.
This requirement is monitored by an observer. The observer also
controls that the train does not stop if the track is free.
There are some failures which can lead into faulty and unsafe behavior.
For example the communication between the RBC and the trains can be lost.
Model Description
Main Chart
The MAIN_CHART comprises the trains, a MAIN_OBSERVER,
and an initializer, responsible for giving the first train on the
track the authority to move on. The initializer simply fires the
FREE_PLACE event, if the condition WAIT_FREE_PLACE_FM
from the environment is set. The MAIN_OBSERVER waits for the
FAILURE event from a train. The only thing it has to do is
catch all failures from the trains and switch to its FAILURE
state.
Structure of Trains
There is one activity chart for each train. It is split into three
parallel ones. The first represents the RBC-communication part for
this train, the second the train itself, and the third the observer.
Each activity chart gets an input MOVE_FROM_PRED from the
activity chart of the train in front of it,
and sends an output MOVE_TO_NEXT to activity chart belonging to
the train behind it. Furthermore every activity charts gets eight
different conditions as input, representing the environmental
behavior, which can not be directly influenced by the controller. This
might be the expected, or an faulty behavior.
- FREE_PLACE
- This condition should be set, if there is a free place at the start of the track section.
- TRANS_SUCCEEDS
- Will be set, if the transmission from the train to the RBC is successful.
- TRANS_FAILS
- Will be set, if the transmission from the train to the RBC is not successful. This failure mode can lead into a faulty behavior.
- ERROR_STARTS
- Will be set, if an internal error inside the RBC occurs. The normal way to handle such an error is, to restart the RBC.
- ERROR_ENDS
- Will be set, if an internal error inside the RBC is repaired (for example, if the RBC was restarted).
- CONN_LOSS_STARTS
- Will be set, if the connection between the RBC and the train is lost.
- CONN_LOSS_ENDS
- Will be set, if the connection between the RBC and the train is restored. It is assumed, that the RBC is in its idle state, when the connection is reestablished.
- BRAKE
- Will be set, if the train does not get a new moving authorization, for some time.
- REPORT
- Will be set, when all necessary information for a new position report to the RBC are collected.
RBC Communication
Most of the environmental behavior influences the communication
behavior between the train and the RBC. Normally the RBC part,
responsible for the train, is idle (state IDLE). If it receives
a position information from the train in front of it (event
MOVE_FROM_PRED), is tries to transmit a moving authorization.
Depending to the environmental behavior, this either fails, or
succeeds (conditions TRANS_FAILS or TRANS_SUCCEEDS). The
moving authorization will be submitted as an event (MOVE) to
the parallel state which represents the train. If a train sends its
position report to the RBC, an event (MOVE_TO_NEXT) is send to
the next.
There are two types of errors, which can make the communication not
work. If the condition ERROR_STARTS is set, no communication
between the train and the RBC is possible, due to an internal error of
the RBC. The same applies when the condition CONN_LOSS_STARTS
is set, indicating a connection loss. The loss of connection has a
higher priority, because it does not matter, whether the RBC works
correct or not, when there is no connection. To return into normal
(connected) behavior, the conditions ERROR_ENDS or
CONN_LOSS_ENDS have to be set.
Train
The train is separated in two parallel parts. The first controls the
moving of the train. After getting a the MOVE event from the
RBC communication part, the train is in the MOVING state until
the BRAKE condition is set. After that the train waits in the
BRAKING state until a new moving authorization is given. The
second part controls the position reports. If the parallel chart is in
state MOVING, a new position is reported (via the
POSITION event). After that, the train has to wait in the state
REPORT_SENT for the a new REPORT event, which indicates,
that all necessary information for a new report are collected. Then it
changes to the REPORT_READY state, form which it can again send
a new position report (under the condition of being in the
MOVING state).
Observer
The observer has two parallel states, one observing the correct
sending of a moving authorization, and the other observing the correct
sending of a position report. The moving authorization is observed by
making sure, that the MOVE_FROM_PRED event is followed by the
MOVE event. This is done by two exclusive states
(WAIT_FROM_PRED and WAIT_FOR_MOVE). If one of the events
is set without the other the chart switches to a failures state, and
fires a FAILURE event to the MAIN OBSERVER.
The position report is observed in a similar way. Here the events
POSITION and MOVE_TO_NEXT have to occur alternating. If
not the chart switches in a failure state again, and the
FAILURE event is fired to the MAIN OBSERVER.
Braking-system models
Model Description
Model Description
The braking system is taken from the case study used in the ARP 4761. The job of the system is to provide hydraulic pressure to the wheels of the aircraft, whenever the pilot pushes the braking pedals. The autobraking mode, where the pilot specifies a deceleration rate and the braking system computes the necessary braking commands itself, is not considered.
The system consists three redundant hydraulic pressure lines, various valves and
a computer called BSCU (Braking System Command Unit), which computes
braking and anti-skid commands based on the pilot input. The structure of the
system is shown in figure 1. The inputs to the
system are supplied by three external activities. POWER supplies
electrical power needed by the BSCU via two redundant lines PWR_1 and
PWR_2. Hydraulic pressure (HYDRAULIC) is supplied from three
independent lines, the green or normal line (GREEN_PRESSURE_IN), the blue
or alternate line (BLUE_PRESSURE_IN) and the emergency line
(EMERGENCY_PRESSURE_IN). Note that this is a small difference to the
original system given in the ARP, as the emergency pressure is supplied from
inside the system there. The remaining inputs are given by the PILOT.
These are the braking command specified via the position of the braking pedals
(PEDAL_POS), the manual mode selection (MODE_SELECTION, see below)
and the deceleration rate for the autobraking (AB_DECEL_RATE, currently
unused). The output of the system is the hydraulic pressure applied to the
wheels. Pressure can be supplied via two redundant lines,
GREEN_PRESSURE_OUT and BLUE_PRESSURE_OUT. These lines are driven
by the three different operational modes, corresponding to the three input
pressure lines.
The normal mode is driven by the green pressure line and is completely
controlled by the BSCU. When the BSCU or the green pressure line fails, the
alternate mode engages. Pressure is supplied via the blue hydraulic line,
basic braking commands are now directly controlled by the pilot. The BSCU will
add anti skid commands if it is working. When the blue pressure failes, the
emergency pressure kicks in which also drives the blue output pressure. In
emergency mode, anti skid is disabled, regardsless of the BSCU state.
Mode switches are controlled by the SELECTOR_VALVE_AC. It switches to the
next available pressure line, when the currently active on fails. Switching is
monotonic in this version of the model - the system starts in normal mode and
can only switch ``down'' to the next available mode, not back. When the BSCU
stops operating, it sends a shutoff signal to the
SHUT_OFF_SELECTOR_VALVE_AC valve, which inhibits the green pressure to
reach the selector valve, thus deactivating the normal mode.
The implementation of the BSCU is shown in
figure 2. It consists of two redundant computation
units (COMMAND_1_AC and COMMAND_2_AC), two monitoring units
(MONITOR_1_AC and MONITOR_2_AC), the logic to chose
between these two lines (SELECT_CMD_AC) and the shutoff monitor
(SHUTOFF_AC). In the current implementation, each command unit simply
copies the braking command given by the pedal position. The monitoring units
compute a reference command in the same way and compare it to the output of the
command units. As soon as those commands differ, the corresponding invalid
signal is set (INVALID_1 or INVALID_2). The switching
unit selects the command computed by the first command unit, unless the
INVALID_1 signal is set. As soon as both invalid signals are set, the
shutoff unit sets the shutoff signal.
Safety Analysis
There are two safety requirements which are considered in the analysis of the braking system. The first requirement under consideration is the shutoff of the BSCU. The following failure modes are considered for this analysis:
- failure of the command computation (
CMD_{1,2}) - failure of the anti skid command computation (
AS_CMD_{1,2}) - failure of the monitor command computation (
MON_{1,2}_CMD)
The analysis generated the quotient shown in figure 3.
The second safety requirement under consideration is the complete loss of braking commands. The failure modes under considertation are the same as above and additionally:
- failure of the invalid signals (
INVALID_{1,2}), - failure of the command selection switch (
SELECT_CMD_2) - failure of electrical power (
PWR_{1,2}) - failure of hydraulic pressure
(
{GREEN,BLUE,EMERGENCY}_PRESSURE_IN) - manual mode selection (
MODE_SELECTION)
Contact
In case of questions, don't hesitate to drop an email to wimmer@informatik.uni-freiburg.de.
