Abstract
The paper relates an industrial experiment performed jointly by LAAS-CNRS and Electricité de France (EdF in short) for assessing the application of a formal method to the reverse engineering of (a part of) a fault-tolerant monitoring system designed for the control room of French N4 nuclear power plants. More specifically, the experiment is devoted to the formal specification and verification of the distributed scheduling algorithm managing the hot redundancy between the two computers composing the system, a single fault hypothesis being assumed for this function. The formal method used for the experiment is RT-LOTOS, a temporal extension of the LOTOS standard Formal Description Technique (FDT in short). The main motivation behind the experiment was to get a better understanding of the fault-tolerant features of the scheduling algorithm by means of both simulation and formal verification.
Chapter PDF
Similar content being viewed by others
Keywords
References
T. Bolognesi, J. van de Lagemaat, and C. Vissers, editors. LOTO-Sphere: Software Development with LOTOS. Kluwer Academic Publisher, 1995.
J.-P. Courtiat, P. Dembinski, G. Holzmann, L. Logrippo, H. Rudin, and P. Zave. Formal methods after 15 years: status and trends. To appear in Computer Networks and ISDN Systems, 1996.
CdO95] J.-P. Courtiat and R.C. de Oliveira. A Reachability Analysis of RT-LOTOS Specifications. In Proc. 8th Intern. Confer. on Formal Description Techniques (FORTE’95),Montreal, Canada, October 1995. Chapman Hall.
G.J. Holzmann. Design and validation of protocols: a tutorial. Computer Networks and ISDN Systems, 25: 981–1017, 1993.
M. Yannakakis and D. Lee. An efficient algorithm for minimizing real-time transition systems. In CAV ‘83, volume 697 of LNCS, pages 210–224. Springer-Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Andriantsiferana, L., Courtiat, JP., De Oliveira, R.C., Picci, L. (1997). An experiment in using RT-LOTOS for the formal specification and verification of a distributed scheduling algorithm in a nuclear power plant monitoring system. In: Mizuno, T., Shiratori, N., Higashino, T., Togashi, A. (eds) Formal Description Techniques and Protocol Specification, Testing and Verification. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35271-8_27
Download citation
DOI: https://doi.org/10.1007/978-0-387-35271-8_27
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5260-1
Online ISBN: 978-0-387-35271-8
eBook Packages: Springer Book Archive