Generating Formal Specifications for Security-Critical Applications - A Model-Driven Approach

The SecureMDD approach aims to generate both, a for- mal specification for verification and executable code, from UML diagrams. The UML models define the static as well as dynamic components of the system under development. This model-driven approach is focused on security-critical applications that are based on cryptographic protocols, esp. Java Card applications. In this paper we describe the gen- eration of the formal specification from the UML model which is then used as input for our interactive verification system KIV. The formal specification is based on abstract state machines and algebraic specifications. It allows to formulate and to prove application-specific security prop- erties.