A Survey: Applying Formal Methods to a Software Intensive System

Adriaan de Groot, Jozef Hooman, Fabrice Kordon, Emmanuel Paviot-Adet, Isabelle Mounier Laboratoire, Michel Lemoine, Gervais Gaudiere, Victor L. Winter, Deepak Kapur

Appeared in: Proceedings of the IEEE High-Assurance Systems Engineering Workshop (HASE 01), pages 55 - 64, 2001.


This paper surveys various complementary formal approaches that could be used to facilitate the development of the train control system described in BART case study. This system is interesting because train control must take into account complex behaviors, positional uncertainties, noise, continuous aspects, and a predefined computational architecture. The approaches discussed are works in progress and are not complete at the time of the writing of this paper.