Quality assurance for security-critical systems is particularly challenging: many systems are developed, deployed, and used
that do not satisfy their security requirements. A number of software engineering approaches have been developed over the
last few years to address this challenge, both in the context of model-level and code-level security assurance. However, there
is little experience so far in using these approaches in an industrial context, the challenges and benefits involved and the
relative advantages and disadvantages of different approaches. This paper reports on experiences from a practical application
of two of these security assurance approaches. As a representative of model-based security analysis, we considered the UMLsec
approach and we investigated the JML annotation language as a representative of a code-level assurance approach. We applied
both approaches to the development and security analysis of a biometric authentication system and performed a comparative
evaluation based on our experiences.
Keywords Security analysis - JML - UMLsec - biometric authentication
Empirical results category paper.