Author: Natsuki Terada
This example was developed by Natsuki Terada from the Japanese Railways
Research Institute (RTRI) on a two year visit to IFAD in 2000 and 2001.
It models a database for digital Automatic Train Control in Japan. More
information can be found in:
Natsuki Terada, Formal Integrity Analysis of Digital ATC Database,
In Proceedings of WCRR2001 (World Congress on Railway Research), 2001.
Natsuki Terada, Integrity Analysis of Digital ATC Database with
Automatic Proofs, In VDM Workshop 3, Part of the FME 2002 conference,
Copenhagen, Denmark, July 2002.
Natsuki Terada, Application of Formal Methods to Automatic Train Control
Systems, In Proceedings of Symposium on Formal Methods for Railway
Operation and Control Systems (FORMS 2003), 2003.
N. Terada and M. Fukuda, Application of Formal Methods to the Railway
Signaling Systems, In Quarterly Report of RTRI, 2002, Vol 43, no 4,
pp 169-174.
Language Version: vdm10
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland
