A Formal Verification Environment for Railway Signaling System Design
Tóm tắt
A fundamental problem in the design and development of embedded control systems is the verification of safety requirements. Formal methods, offering a mathematical way to specify and analyze the behavior of a system, together with the related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools often fail to formally validate such systems. This paper outlines an experience on formal specification and verification carried out in a pilot project aiming at the validation of a railway computer based interlocking system. Both the specification and the verification phases were carried out in the JACK (Just Another Concurrency Kit) integrated environment. The formal specification of the system was done by means of process algebra terms. The formal verification of the safety requirements was done first by giving a logical specification of such safety requirements, and then by means of model checking algorithms. Abstraction techniques were defined to make the problem of safety requirements validation tractable by the JACK environment.
Tài liệu tham khảo
J.R. Abrial et al. The B Method. BP International Ltd., 1991.
A. Anselmi, C. Bernardeschi, A. Fantechi, S. Gnesi and S. Larosa, G. Mongardi and F. Torielli. An Experience in Formal Verification of Safety Properties of a Railway Signaling Control System. In Proceedings SAFECOMP'95 Conference. Belgirate, Springer-Verlag, pages 474–488, 1995.
C. Bernardeschi and G. Ferro. A Sample Study Exemplifying the Use of JACK. In Proceedings Workshop on Automated Formal Methods, ENTCS. University of Oxford, 1996 (to appear).
R. S. Boyer and J.S. Moore. A Computational Logic. ACM Monograph Series, Academic Press, 1979.
J.P. Bowen and M.G. Hinchey. Seven More Myths of Formal Methods. IEEE Software 12:34–41, July 1995.
A. Bouali and R. De Simone. Symbolic bisimulation minimization. In Proceedings Fourth Workshop on Computer-Aided Verification, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, pages 96–108, 1992.
A. Bouali, S. Gnesi and S. Larosa. The integration Project for the JACK Environment. Bulletin of the EATCS 54:207–223, October 1994.
A. Bouali, A. Ressouche, V. Roy and R. De Simone. The FC2TOOLS set. In Proceedings Workshop on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
G. Boudol. Notes on Algebraic Calculi of Processes. NATO ASI Series F13, 1985.
G. Bruns. A Case Study in Safety Critical Design. In Proceedings Workshop on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, pages 213–224, 1992.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation 98 2:142–270, June 1992.
E.M. Clarke, E.A. Emerson and A.P. Sistla. Automatic Verification of Finite—State Concurrent Systems Using Temporal Logic Specification. ACM Transaction on Programming Languages and Systems 8:244–263, April 1986.
C. Da Silva, B. Dehbonei and F. Mejia. Formal Specification in the Development of Industrial Applications: Subway Speed Control System. In M. Diaz and R. Groz, editors, Formal Description Techniques, V (C-10). Elsevier Science Publishers B, V, North-Holland, pages 199–213, 1993.
B. Dehbonei and F. Mejia. Formal Methods in the Railways Signaling Industry. In Proceedings FME'94: Industrial Benefit of Formal Methods, volume 873 of Lecture Notes in Computer Science. Spain, pages 26–34, 1994.
R. De Nicola, A. Fantechi, S. Gnesi and G. Ristori. An Action-based Framework for Verifying Logical and Behavioral Properties of Concurrent Systems. Computer Network and ISDN systems 25:761–778, February 1993
R. De Nicola and F.W. Vaandrager. Action versus State based Logics for Transition Systems. In Proceedings Ecole de Printemps on Semantics of Concurrency, volume 469 of Lecture Notes in Computer Science. Springer-Verlag, pages 407–419, 1990.
R. De Nicola, A. Fantechi, S. Gnesi and G. Ristori. Hardware Components within JACK,” In Proceedings of CHARME '95, volume 987 of Lecture Notes in Computer Science. Springer-Verlag, pages 246–260, 1995.
E.A. Emerson and J.Y. Halpern. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. Journal of Computer and System Sciences 30:1–24, 1985.
E. A. Emerson and J.Y. Halpern. Sometimes and Not Never Revisited: on Branching Time versus Linear Time Temporal Logic. Journal of ACM 33:51–178, January 1986.
G. Ferro. AMC: ACTL Model Checker. Reference Manual. IEI-Internal Report, B4-47 December 1994.
S. Fisher, A. Scholz and D. Taubner. Verification in Process Algebra of the Distributed Control of Track Vehicles-A Case Study. Journal of Formal Methods in System Design ?:99–122, February 1994
S. Gnesi. A Formal Verification Environment for Concurrent Systems Design. In Proceedings Workshop on Automated Formal Methods, ENTCS. University of Oxford, 1996 (to appear).
V. Hartonas-Garmhausen, T. Kurfess, E.M. Clarke and D. Long. Automatic Verification of Industrial Designs. In Proceedings Workshop on Industrial-Strength Formal Specification Techniques. Boca Raton, Florida, April 1995.
C.R. Hoare. Communicating Sequential Processes. Prentice Hall Int., London, 1985.
M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM 32:137–161, January 1985.
R. Pugliese and E. Tronci. Automatic Verification of a Hydroelectric Power Plant. In Proceedings FME'96 Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 425–444, 1996.
E. Madelaine and D. Vergamini. AUTO: A Verification tool for Distributed Systems using Reduction of Finite Automata Networks. In S.T Vuong, edtor, Formal Description Techniques II, pages 61–66, 1990.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems-Specification. Springer-Verlag, 1992.
R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
G. Mongardi. Dependable Computing for Railway Control Systems. In Proceedings Dependable Computing for Critical Applications 3. Springer-Verlag, pages 255–277, 1992.
W. Nyberg. An Evaluation of Using State-Based Specification Languages for an Automatic Train Protection System. In Proceedings Nordic Seminar on Dependable Computing Systems ( NSDCS'94). Lingby, Denmark, pages 105–116, 1994.
D. Park. Concurrency and Automata on Infinite Sequences. In Proccedings Fifth GI Conference, volume 104 of Lecture Notes in Computer Science. Springer-Verlag, pages 167–183, 1981.
A. Pnueli. Linear and Branching Structures in the Semantics and Logic of Reactive Systems. In Proceedings of 12th ICALP, volume 194 of Lecture Notes in Computer Science, 1985.
V. Roy and R. De Simone. AUTO and Autograph. In Proceedings Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science. Springer-Verlag, pages 65–75, 1990.
A. Simpson. The Formal Specification of an Automatic Train Protection System. In Proceedings FME'94 Industrial Benefit of Formal Methods, volume 873 of Lecture Notes in Computer Science. Spain, pages 602–617, 1994.