3rd SAM Workshop: SDL-2000 Design Contest

3rd SAM
(SDL And MSC)
Workshop

Aberystwyth
24th-26th June 2002

Organisers: SDL Forum Society and

SDL-2000 Design Contest
Specification of a Railway Crossing

The SDL and MSC (SAM) workshop provides an open discussion arena in the year between SDL Forums, which are held every two years. Part of the 3rd SAM Workshop is an SDL-2000 design contest.

The task is to specify a railway crossing with 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 winner of the contest will be the specification(s) that best demonstrate(s) the use of SDL and/or MSC.

Submissions to the Contest are accepted independently from paper submissions. The PC will select up to six best solutions for publication on the Web page of the SDL Forum Society prior to the workshop. Each published solution will be rewarded with 125 Euros. The SAM workshop will include a panel session where the results of the Contest will be discussed. At this event, the best solution will be selected by the audience. The prize for the best solution is 500 Euros.

Submission policy:

Participants of the contest are encouraged to register at Contest2002@sdl-forum.org. They will be inserted into an email list Contest-participants@sdl-forum.org where all clarifications to the original task are communicated. Moreover, the current specification of the problem can always be found at http://www.sdl-forum.org/Events/SAM03Contest.htm.

When: 12th May 2002

Where: Contest2002@sdl-forum.org

Format: The formal parts should be 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.