Formal Methods Europe Logo Formal Methods Europe
   
   
 
  Choosing
  Methods
  Tools
  Applications
  FAQs
  Literature
  Journals
  Courses
  Projects
  Universities
  Industry
  Groups
  Links
 

Application name:

Compact Dynamic Bus Station

Organisation:

Utrecht University, dept. of Philosophy; Nederland Haarlem BV; CWI

Method:

PSF, ACP, Linear Programming by means of Cplex, ASF+SDF

Tools:

PSF Toolkit, ASF+SDF Meta-environment, Cplex

Domain:

Public Transport

Period:

Fall 1994 - Winter 1995.

Size:

10 manmonths.

Description:

A compact dynamic bus station is an approach to offer a better product to travellers: up-to-date information on arrival and departure, and enhanced surveyability of the station by making it as small as possible. To that end a control system has the task to regulate in real-time the busses that visit the station. The most important task is to assign busses to platforms in an optimal way. Several formalisms were used in this project. The project resulted in a working and resonably complete prototype of a control system for compact dynamic bus stations.

Conclusions:

We experienced that it was very hard to come-up with a proper formal specification. We think this was due to the fact that this was a new domain to us, as well to the commercial partner. During the project a switch was made: a prototype was constructed in order develop a better feeling of the domain. The formal effort was minimized.

Publications:

Compact Dynamisch Busstation. A.S. Klusener, S.F.M. van Vlijmen and A. Schrijver. Technical report CS--N9601. National Research Institute for Mathematics and Computer Science (CWI). 1996. In dutch.

Algebraic Specification in Action. S.F.M. van Vlijmen. Phd thesis. Utrecht University, department of Philosophy. 1998.

Contact:

Name:S.F.M. van Vlijmen
Organisation:Utrecht University
Address:Utrecht University
Country:The Netherlands
E-mail:vlijmen@phil.uu.nl

Remarks:

The work was for a large part funded by Nederland Haarlem, the industrial partner.