Model Checking of Security-Critical Applications in a Model-Driven Approach

Marian Borek, Nina Moebius, Kurt Stenzel and Wolfgang Reif

This paper illustrates the integration of model checking in SecureMDD, a model-driven approach for the development of security-critical applications. In addition to a formal model for interactive verification as well as executable code, a formal system specification for model checking is generated automatically from a UML model. Model checking is used to find attacks automatically and interactive verification is used by an expert to guarantee security properties. We use AVANTSSAR for model checking and KIV for interactive verification. The integration of AVANTSSAR in SecureMDD and the advantages and disadvantages over interactive verification with KIV are demonstrated with a smart card based electronic ticketing example.
published 2013 Proceedings of the 11th International Conference on Software Engineering and Formal Methods (SEFM), LNCS 8137, Madrid, Spain, September 25-27, 2013.

Publisher: Springer Berlin Heidelberg



For questions regarding the publication, please contact!