FORMÁLNÍ METODY VE VÝVOJI SOFTWARU BEZPEČNOSTNĚ KRITICKÉHO SYSTÉMU
Klíčová slova:
software, formální metody, bezpečnost, software, formální metody, bezpečnostAbstrakt
Článek se zaměřuje na využití formálních metod při vývoji softwaru pro bezpečnostně kritické systémy v dopravě. Takové systémy mají narůstající složitost a musejí vyhovovat určitým požadavkům na kvalitu. Formální metody jsou zařazeny do procesu vývoje softwaru. Použití vybrané formální metody Event-B je demonstrováno na specifikaci chování železničního přejezdového zabezpečovacího zařízení.
Stažení
Data o stažení nejsou doposud dostupná.
Reference
(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.
Stahování
Publikováno
2019-04-26
Jak citovat
Bubeník, M. (2019). FORMÁLNÍ METODY VE VÝVOJI SOFTWARU BEZPEČNOSTNĚ KRITICKÉHO SYSTÉMU. Perner’s Contacts, 14(1), 21–27. Získáno z https://pernerscontacts.upce.cz/index.php/perner/article/view/385
Číslo
Sekce
Články
Licence
Copyright (c) 2020 Michal Bubeník
Tato práce je licencována pod Mezinárodní licencí Creative Commons Attribution 4.0 .
