FORMAL METHODS IN DEVELOPMENT OF SAFETY CRITICAL SYSTEM SOFTWARE
Keywords:
software, formal methods, safetyAbstract
This article focuses on using formal methods in development of safety critical system software in transport. Such system has an increasing complexity and has to meetcertain quality requirements. Formal methods are set in the software development process. The use of formal method Event-B is demonstrated on a railway level crossing protection equipment specification.
Downloads
Download data is not yet available.
References
(1) Abrial J.R. The B tool. In: Bloomfield R.E., Marshall L.S., Jones R.B. (eds) VDM '88 VDM — The Way Ahead. VDM 1988. Lecture Notes in Computer Science, vol 328. Springer, Berlin, Heidelberg.
(2) Bowen J. Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press, 1996. 302 s. ISBN 978-18-5032-230-6.
(3) ČSN 34 2650. Železniční zabezpečovací zařízení – Přejezdová zabezpečovací zařízení. ed. 2. Praha: Úřad pro technickou normalizaci, metrologii a státní zkušebnictví, 2010.
(4) ČSN EN 50128. Drážní zařízení – Sdělovací a zabezpečovací systémy a systémy zpracování dat – Software pro drážní řídicí a ochranné systémy, ed. 2. Praha: Úřad pro technickou normalizaci, metrologii a státní zkušebnictví, 2012.
(5) Event-B.org [online]. [cit. 2019-01-12]. Dostupné z: <http://www.eventb.org/install.html>.
(6) Lamport, L. A High-Level View of TLA+ [online]. 2018 [cit. 2019-01-14]. Dostupné z: <http://lamport.azurewebsites.net/tla/high-level-view.html>.
(7) Petri, C.A., Reisig, W. Petri net. Scholarpedia [online]. 2008 [cit. 2018-12-29]. Dostupné z: <http://www.scholarpedia.org/article/Petri_net>.
(8) The ProB Animator and Model Checker [online]. [cit. 2019-01-12]. Dostupné z: <https://www3.hhu.de/stups/prob/index.php/The_ProB_Animator_and_Model_Checker>
(9) RTCA DO-178C. Software Considerations in Airborne Systems and Equipment Certification. Version C. 2011.
(2) Bowen J. Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press, 1996. 302 s. ISBN 978-18-5032-230-6.
(3) ČSN 34 2650. Železniční zabezpečovací zařízení – Přejezdová zabezpečovací zařízení. ed. 2. Praha: Úřad pro technickou normalizaci, metrologii a státní zkušebnictví, 2010.
(4) ČSN EN 50128. Drážní zařízení – Sdělovací a zabezpečovací systémy a systémy zpracování dat – Software pro drážní řídicí a ochranné systémy, ed. 2. Praha: Úřad pro technickou normalizaci, metrologii a státní zkušebnictví, 2012.
(5) Event-B.org [online]. [cit. 2019-01-12]. Dostupné z: <http://www.eventb.org/install.html>.
(6) Lamport, L. A High-Level View of TLA+ [online]. 2018 [cit. 2019-01-14]. Dostupné z: <http://lamport.azurewebsites.net/tla/high-level-view.html>.
(7) Petri, C.A., Reisig, W. Petri net. Scholarpedia [online]. 2008 [cit. 2018-12-29]. Dostupné z: <http://www.scholarpedia.org/article/Petri_net>.
(8) The ProB Animator and Model Checker [online]. [cit. 2019-01-12]. Dostupné z: <https://www3.hhu.de/stups/prob/index.php/The_ProB_Animator_and_Model_Checker>
(9) RTCA DO-178C. Software Considerations in Airborne Systems and Equipment Certification. Version C. 2011.
Downloads
Published
2019-04-26
How to Cite
Bubeník, M. (2019). FORMAL METHODS IN DEVELOPMENT OF SAFETY CRITICAL SYSTEM SOFTWARE. Perner’s Contacts, 14(1), 21–27. Retrieved from https://pernerscontacts.upce.cz/index.php/perner/article/view/385
Issue
Section
Articles
License
Copyright (c) 2020 Michal Bubeník
This work is licensed under a Creative Commons Attribution 4.0 International License.
