Abstract
ARP4754 suggests that, whenever possible, aeronautical safety critical systems may be developed as well as checked in an incremental way. But in practice the safe design emerges from the functional essential design in a discontinuous fashion. Engineers take several decisions in the direction of safety that sometimes can loose some of the desired functional characteristics. This can increase the development cost by only detecting functional problems in late phases of the development life cycle. In this paper we propose a strategy that starts from an initial proposed design, where functional behavior is investigated using model checking, and evolves to a reliable and safe design in a stepwise fashion. At each step, where safety aspects are introduced, safety constraints are checked using probabilistic model checking (Markov analysis). The final design emerges when we cannot find any safety violation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Prism and CSP models, http://www.cin.ufpe.br/~acm/ecs/
Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems. Aerospace Recommended Practice ARP4761, SAE International, Warrendale, PA (December 1996)
Alexander, R., Herbert, N., Kelly, T.: Deriving Safety Requirements for Autonomous Systems. In: 4th SEAS DTC Technical Conference (2009)
Alexander, R.D., Kelly, T.P.: Escaping the non-quantitative trap. In: 27th International System Safety Conference, pp. 69–95 (2009)
Bozzano, M., Villafiorita, A.: Improving system reliability via model checking: The FSAP/NuSMV-SA safety analysis platform. In: Anderson, S., Felici, M., Littlewood, B. (eds.) SAFECOMP 2003. LNCS, vol. 2788, pp. 49–62. Springer, Heidelberg (2003)
Damasceno, A., Farias, A., Mota, A.: A Mechanised Strategy for Safe Abstraction of CSP Specifications (Best paper). In: Brazilian Symposium on Formal Methods, vol. 12, pp. 118–133 (2009)
Ebeling, C.E.: An Introduction to Reliability and Maintainability Engineering, 2nd Har/Cdr edn. Waveland Pr Inc., Prospect Heights (2009)
Kerlund, O.A., et al.: ISAAC, a framework for integrated safety analysis of functional, geometrical and human aspects. In: European Congress on Embedded Real Time Software, ERTS 2006 (2006)
Farias, A., Mota, A., Sampaio, A.: Compositional Abstraction of CSP Z Processes. Journal of the Brazilian Computer Society 14(2) (June 2008)
Goldsmith, M.: FDR: User Manual and Tutorial, version 2.77. Formal Systems (Europe) Ltd. (2001)
Gomes, A.J.O.: Model based safety analysis using probabilistic model checking. Master’s thesis, Federal University of Pernambuco (2010)
Grunske, L., Colvin, R., Winter, K.: Probabilistic Model-Checking Support for FMEA. In: QEST 2007: Proceedings of the Fourth International Conference on Quantitative Evaluation of Systems, pp. 119–128. IEEE Computer Society, Los Alamitos (2007)
Isobe, Y., Roggenbach, M.: Csp-prover – a proof tool for the verification of scalable concurrent systems. Journal of Computer Software, Japan Society for Software Science and Technology (JSSST) 25, 85–92 (2008)
Jesus, J.B.J.: Designing and formal verification of fly-by-wire flight control systems. Master’s thesis, Federal University of Pernambuco (2009)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Performance Evaluation Review 36(4), 40–45 (2009)
Laurent, O.: Using formal methods and testability concepts in the avionics systems validation and verification (v&v) process. In: 2008 International Conference on Software Testing, Verification, and Validation, pp. 1–10 (2010)
Lisagor, O., Kelly, T.: Incremental safety assessment: Theory and practice. In: 26th International System Safety Conference, published by the System Safety Society (2008)
Lisagor, O., McDermid, J., Pumfrey, D.J.: Towards a practicable process for automated safety analysis. In: 24th International System Safety Conference, pp. 596–607 (2006)
The MathWorks Inc. Simulink Validation and Verification 2 User’s Guide (2008)
Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall International (UK) Ltd., Englewood Cliffs (1994)
Papadopoulos, Y., McDermid, J., Sasse, R., Heiner, G.: Analysis and synthesis of the behaviour of complex programmable electronic systems in conditions of failure. Reliability Engineering & System Safety 71(3), 229–247 (2001)
Ramos, R., Sampaio, A., Mota, A.: Conformance notions for the coordination of interaction components. Science of Computer Programming 75(5), 350–373 (2010)
Roscoe, A.: The Theory and Practice of Concurrency. Prentice Hall PTR, Englewood Cliffs (1997)
Soares, G., Gheyi, R., Massoni, T., Cornelio, M., Cavalcanti, D.: Generating unit tests for checking refactoring safety. In: Brazilian Symposium on Programming Languages, pp. 159–172 (2009)
Stephenson, Z., McDermid, J., Choy, J.: Using simulation to validate style-specific architectural refactoring patterns. In: SEW 2006: Proceedings of the 30th Annual IEEE/NASA Software Engineering Workshop, pp. 123–132. IEEE Computer Society, Los Alamitos (2006)
Zeyda, F., Cavalcanti, A.: Mechanised Translation of Control Law Diagrams into Circus. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 151–166. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mota, A., Jesus, J., Gomes, A., Ferri, F., Watanabe, E. (2010). Evolving a Safe System Design Iteratively. In: Schoitsch, E. (eds) Computer Safety, Reliability, and Security. SAFECOMP 2010. Lecture Notes in Computer Science, vol 6351. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15651-9_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-15651-9_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15650-2
Online ISBN: 978-3-642-15651-9
eBook Packages: Computer ScienceComputer Science (R0)