Abstract
Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Akers, S.: Binary Decision Diagrams. IEEE Transactions on Computers C-27(6) , 509–516 (1978)
Berthomieu, B., Ribet, P.O., Vernadat, F.: The Tool TINA - Construction of abstract state spaces for Petri Nets and Time Petri Nets. International Journal of Production Research 42, 2741–2756 (2004)
Böde, E., Peikenkamp, T., Rakow, J., Wischmeyer, S.: Model based importance analysis for minimal cut sets. Reports of SFB/TR 14 AVACS 29, SFB/TR 14 AVACS, ISSN: 1860-9821 (April 2008)
Boniol, F., Wiels, V.: Landing gear system (2013), http://www.irit.fr/ABZ2014/landing_system.pdf (accessed on August 5, 2014)
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)
Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Model-based codesign of critical embedded systems. In: Proceedings of the 2nd International Workshop on Model Based Architecting and Construction of Embedded Systems (ACES-MB 2009), vol. 507, pp. 87–91. CEUR Workshop Proceedings (2009)
Bozzano, M., Cimatti, A., Katoen, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability, and performance analysis of extended AADL models. The Computer Journal (2010)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2008)
Farail, P., Gaufillet, P., Peres, F., Bodeveix, J.P., Filali, M., Berthomieu, B., Rodrigo, S., Vernadat, F., Garavel, H., Lang, F.: FIACRE: an intermediate language for model verification in the TOPCASED environment. In: European Congress on Embedded Real-Time Software (ERTS 2008). SEE (January 2008), http://www.see.asso.fr
Fernandez, J.C., Garavel, H., Kerbrat, A., Mounier, L., Mateescu, R., Sighireanu, M.: CADP - a protocol validation and verification toolbox (1996)
Groote, J.F., Kouters, T.W.D.M., Osaiweran, A.: Specification guidelines to avoid the state space explosion problem. In: Arbab, F., Sirjani, M. (eds.) FSEN 2011. LNCS, vol. 7141, pp. 112–127. Springer, Heidelberg (2012)
Grunske, L., Colvin, R., Winter, K.: Probabilistic model-checking support for FMEA. In: Proceedings of the 4th International Conference on Quantitative Evaluation of Systems (QEST 2007). IEEE (2007)
Güdemann, M., Ortmeier, F.: A framework for qualitative and quantitative model-based safety analysis. In: Proceedings of the 12th High Assurance System Engineering Symposium (HASE 2010), pp. 132–141 (2010)
Güdemann, M., Ortmeier, F., Reif, W.: Using deductive cause-consequence analysis (DCCA) with SCADE. In: Saglietti, F., Oster, N. (eds.) SAFECOMP 2007. LNCS, vol. 4680, pp. 465–478. Springer, Heidelberg (2007)
Lipaczewski, M., Struck, S., Ortmeier, F.: Using tool-supported model based safety analysis - progress and experiences in SAML development. In: Winter, V., Gandhi, R., Parakh, A. (eds.) IEEE 14th International Symposium on High-Assurance Systems Engineering, HASE 2012 (2012)
Ortmeier, F., Reif, W.: Safety optimization: A combination of fault tree analysis and optimization techniques. In: Proceedings of the Conference on Dependable Systems and Networks (DSN 2004). IEEE Computer Society Press, Florence (2004)
Ortmeier, F., Thums, A., Schellhorn, G., Reif, W.: Combining formal methods and safety analysis – the ForMoSA approach. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 474–493. Springer, Heidelberg (2004)
Ortmeier, F., Güdemann, M., Reif, W.: Formal failure models. In: Proceedings of the 1st IFAC Workshop on Dependable Control of Discrete Systems (DCDS 2007). Elsevier (2007)
Åkerlund, O., Bieber, P., Boede, E., Bozzano, M., Bretschneider, M., Castel, C., Cavallo, A., Cifaldi, M., Gauthier, J., Griffault, A., Lisagor, O., Luedtke, A., Metge, S., Papadopoulos, C., Peikenkamp, T., Sagaspe, L., Seguin, C., Trivedi, H., Valacca, L.: ISAAC, A framework for integrated safety analysis of functional, geometrical and human aspects. In: Proceedings of 2nd European Congress on Embedded Real Time Software, ERTS 2006 (2006)
SAE-AS5506: Architecture analysis and design language, AADL (2004)
SAE-AS5506/1: Architecture analysis and design language (AADL) Annex E: Error Model Annex (2006)
Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Vernadat, F., Percebois, C., Farail, P., Vingerhoeds, R., Rossignol, A., Talpin, J.P., Chemouil, D.: The TOPCASED project - a toolkit in open-source for critical applications and system development. In: Data Systems in Aerospace (DASIA), European Space Agency. ESA Publications (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Nykolaychuk, M., Lipaczewski, M., Liebusch, T., Ortmeier, F. (2014). On Efficiently Specifying Models for Model Checking. In: Ortmeier, F., Rauzy, A. (eds) Model-Based Safety and Assessment. IMBSA 2014. Lecture Notes in Computer Science, vol 8822. Springer, Cham. https://doi.org/10.1007/978-3-319-12214-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-12214-4_2
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12213-7
Online ISBN: 978-3-319-12214-4
eBook Packages: Computer ScienceComputer Science (R0)