Organised by: SDL Forum Society
and

The SDL and MSC (SAM) workshop provides an open discussion arena in the year between SDL Forums, which are held every two years. For the SDL-2000 design contest as part of the 3rd SAM Workshop the contest task was to specify a railway crossing

There were five entries to the contest all of which were judged to as good for publication on the SDL Forum WWW site as described in the contest rules below. These can be found at the following locations:

http://www.sdl-forum.org/SAM_contest/Aguilar

http://www.sdl-forum.org/SAM_contest/Brandt

http://www.sdl-forum.org/SAM_contest/Conquet

http://www.sdl-forum.org/SAM_contest/Li_Probert_Williams (WINNERS)

http://www.sdl-forum.org/SAM_contest/QueinsMetzger

Each of these has the SDL source available as a CIF file and as a viewable PDF file. The CIF format is an ASCII format that should be interchangable between tools, but the actual tool used is shown in the name of the file: Cinderella, GEODE or SDT. In the case of GEODE, CIF is also the native format for the tool so no other files are needed (but note that GEODE normally expects the file extnsion to .pr rather than .cif).

Some common tests were provided and the results of runniing these are provided as PDF files. Other documentation provided is also available in PDF format. These and other files are described in more detail with the entry. These are listed after the requirements below.

Requirements

The requirements were for the system to have the following characteristics:

1. There are a number of tracks for the trains. The specification should be generic in the number of tracks.

2. There is a controller, taking into account the number of cars waiting and the trains approaching.

3. There is a gate for cars, which must be controlled. The pattern of cars approaching is simply given by a constant delay between the cars.

4. Each track has two sensors: one sensor when a train is approaching and one sensor when the train is leaving the gate. There is also a sensor that indicates when there is more than one car waiting.

5. There is a signal on each track informing the trains if they are allowed to pass or if they have to stop.

6. The controller can act either by closing the gate or by stopping a train (setting a closing signal). Each of these actions has to be finished before the train reaches the gate.

7. Trains: the solution should be generic in the number of trains. A train will start the breaking phase as soon it sees a stopping signal and restart when the stopping signal goes off. All trains on the same track are supposed to run in the same direction and with a minimal delay between them depending on their speed (a train must be able to stop even if the preceding one stops immediately). There are regular trains, which have a small (maximal) speed and fast trains, which can run faster. Regular and fast trains never run on the same track.

8. The active elements of the system are the trains, the sensors, the controller and the gate. The cars are not considered to be in the system.

9. The solution should allow several strategies of the gate controller to be checked.

10. At least the following strategies should be possible: trains take precedence - at least those with high speed; cars take precedence if there are too many waiting cars. Furthermore, each specification should provide a strategy.

11. There was (small) change in the requirements in the first week of April 2002. Participants are expected to show how they were able to adjust their specification to changes which are:

C1: It is not allowed to set the stopping signal for a track when a train is between the two sensors.

C2: It should be possible to manually control the crossing. In this case, unsafe actions should be rejected.

C3: A sensor does not produce one signal, but a sequence of signals (one for each of the wheels). The end of the sequence is given by a delay of a certain size after the last signal.

The winning entry is the specification(s) that best demonstrate(s) the use of SDL and/or MSC.

Submissions to the Contest were accepted independently from work shop paper submissions. The rules are that up to six best solutions were for publication on the Web page of the SDL Forum Society prior to the workshop: the authors of each published solution to be rewarded with 125 Euros (subject to giving the Society the right to publish on the WWW site). The SAM workshop programme includes a panel session for discussion of the results of the Contest where at least one author of each paper should be present. At the event, the best solution is selected by the audience. The prize for the best solution is 500 Euros.

Submission policy:

Participants of the contest were encouraged to register at the Contest2002 email address of sdl-forum.org. They were inserted into an email list where all clarifications to the original task were communicated. Moreover, the current specification of the problem could always be found at http://www.sdl-forum.org/Events/SAM03Contest.htm where the final specification is therefore to be found.

12th May 2002 was the deadline for submissions.

Format: The formal parts were requested in the format of any graphical SDL and/or MSC tool, which is publicly available.

Content:

• an SDL specification and/or an MSC specification;
• explanations to the specification(s);
• indication which tool(s) have been used to build the specification;
• assumptions about properties not given in the informal description;
• optionally demonstration of key properties by simulation traces or proofs.

Test cases

For each of the following testcases, an MSC trace showing the behaviour in the situation is provided. If the result is different depending on the controller, different traces are provided for different controllers.

Testcase A

TrackLayout: The opening time of the gate is greater than the time a regular speed train needs for the way between the first sensor and the gate.

Situation: There are no trains between the sensors, and the controller triggers the opening of the gate. Then, a train passes the first controller.

Expected behaviour: The opening of the gate is aborted, and the controller triggers its closing.

Testcase B

TrackLayout: The stopping signal is in front of the gate.

Situation: The stopping signal is set, while a train approaches. Its braking distance is longer than the interval between the train and the signal.

Expected behaviour: The train passes the signal.

Testcase C

Situation: There are several trains on all tracks between the sensors, and new ones are approaching from time to time. As there are too many cars waiting at the gate, it has to be opened, therefore, all stopping signals have to be set.

Expected behaviour: The controller sets the stopping signal on EACH track as soon as there are no trains between the sensors, and opens the gate after ALL stopping signals have been set.

Testcase D

TrackLayout: 1 fast track and 2 slow tracks; slow trains take at least 6 time units to reach the gate.

Situation: The following trains enter the system:
at time 0: a slow train on track slow1
at time 1: a slow train on track slow2
at time 2: a slow train on track slow1
at time 3: a slow train on track slow1
at time 4: a fast train on track fast
at time 5: a slow train on track slow1
at time 6: too many cars are waiting
at time 7: a slow train on track slow1
at time 8: a slow train on track slow1
at time 9: a slow train on track slow2
at time 10: a fast train on track fast

Testcase E

TrackLayout: 1 fast track and 2 slow tracks; slow trains take at least 6 time units to reach the gate.

Situation: The following trains enter the system:
at time 0: a slow train on track slow1
at time 1: a slow train on track slow1
at time 2: too many cars are waiting
at time 4: not many cars waiting
at time 5: a slow train on track slow2

Testcase F

TrackLayout: 1 fast track and 2 slow tracks; slow trains take at least 6 time units to reach the gate.

Situation: The following trains enter the system:
at time 0: a slow train on track slow1
at time 2: too many cars are waiting
at time 3: a slow train on track slow2
at time 4: not many cars waiting
at time 5: too many cars are waiting
at time 7: a fast train on track fast
at time 8: not many cars waiting

SDL contest models

See also the 3rd SAM Workshop