Abstract
For model-based development to be a success in practice, it needs to have a convincing added-value associated with its use. Our goal is to provide such added-value by developing tool-support for the analysis of UML models against difficult system requirements. Towards this goal, we describe a UML verification framework supporting the construction of automated requirements analysis tools for UML diagrams. The framework is connected to industrial CASE tools using XMI and allows convenient access to this data and to the human user. As a particular example, we present plugins for verifying models defined using the security extension UMLsec of UML. The verification framework allows advanced users of the UMLsec approach to themselves implement verification routines for the constraints of self-defined stereotypes. In particular, we focus on an analysis plug-in that utilizes the model-checker Spin to verify security properties of cryptography-based systems.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abadi, M.: Security protocols and their properties. In: Bauer, F.L., Steinbrüggen, R. (eds.) Foundations of Secure Computation, pp. 39–60. IOS Press, Amsterdam. 20th International Summer School, Marktoberdorf, Germany (2000)
Abadi M. and Jürjens J. (2001). Formal eavesdropping and its computational interpretation. In: Kobayashi, N. and Pierce, B.C. (eds) Theoretical Aspects of Computer Software (4th International Symposium, TACS 2001), vol. 2215 of Lecture Notes in Computer Science, pp 82–94. Springer, Heidelberg
Best, B., Jürjens, J., Nuseibeh, B.: Model-based security engineering of distributed information systems using UMLsec. In: ICSE. ACM (2007)
Breu, R., Popp, G., Alam, M.: Model based development of access policies. Int. J. Softw. Tools Technol. Transf (STTT). Contained in this issue (2006)
Castor library. Available at http://castor.exolab.org (2003)
Campbell L., Cheng B., McUmber W. and Stirewalt K. (2002). Automatically detecting and visualising errors in UML diagrams. Requir. Eng. 7(4): 264–287
Crook, R., Ince, D.C., Lin, L., Nuseibeh, B.: Security requirements engineering: when anti-requirements hit the fan. In: RE, pp. 203–205. IEEE Computer Society (2002)
Cohen E. (2003). First-order verification of cryptographic protocols. J. Comput. Secur. 11(2): 189–216
Devanbu, P., Stubblebine, S.: Software engineering for security: a roadmap. In: 22nd International Conference on Software Engineering (ICSE 2000): Future of Software Engineering Track, pp. 227–239. ACM (2000)
Dolev D. and Yao A. (1983). On the security of public key protocols. IEEE Trans. Inf. Theory IT-29(2): 198–208
Engels, G., Küster, J., Heckel, R., Lohmann, M.: Model-based verification and validation of properties. Electr. Notes Theor. Comput. Sci. 82(7), (2003)
Fernandez, E.B., Hawkins, J.C.: Determining role rights from use cases. In: Workshop on role-based access control, pp. 121–125. ACM (1997)
Fernández-Medina, E., Martínez, A., Medina, C., Piattini, M.: UML for the design of secure databases: integrating security levels, user roles, and constraints in the database design process. In: Jürjens et al. [21], pp. 93–106
Gentleware. http://www.gentleware.com (2003)
Giorgini P., Massacci F. and Mylopoulos J. (2003). Requirement engineering meets security: a case study on modelling secure electronic transactions by VISA and Mastercard. In: Song, I.-Y., Liddle, S.W., Ling, T.W., and Scheuermann, P. (eds) 22nd International Conference on Conceptual Modeling (ER 2003), vol. 2813 of Lecture Notes in Computer Science, pp 263–276. Springer, Heidelberg
Gurevich Y. (1995). Evolving algebras 1993: Lipari guide. In: Börger, E. (eds) Specification and Validation Methods, pp 9–36. Oxford University Press, Oxford
Houmb, S.H., den Braber, F., Lund, M.S., Stølen, K.: Towards a UML profile for model-based risk assessment. In: Jürjens et al. 21, pp. 79–92
Höhn, S., Jürjens, J.: Automated checking of SAP security permissions. In: 6th Working Conference on Integrity and Internal Control in Information Systems (IICIS). International Federation for Information Processing (IFIP). Kluwer, Academic Publishers (2003)
Huber, F., Molterer, S., Rausch, A., Schätz, B., Sihling, M., Slotosch, O.: Tool supported specification and simulation of distributed systems. In: International Symposium on Software Engineering for Parallel and Distributed Systems, pp. 155–164 (1998)
Holzmann G. (2003). The Spin Model Checker. Addison-Wesley, Reading
Jürjens, J., Cengarle, V., Fernandez, E.B., Rumpe, B., Sandner, R. (eds.) Critical Systems Development with UML (CSDUML 2002), TU München Technical Report TUM-I0208, 2002. UML 2002 satellite workshop proceedings
Jürjens, J., Fox, J.: Tools for model-based security engineering. In: 28th International Conference on Software Engineering (ICSE 2006). ACM (2006)
Jézéquel, J.-M., Hußmann, H., Cook, S. (eds.) In: 5th International Conference on the Unified Modeling Language (UML 2002), vol. 2460 of Lecture Notes in Computer Science. Springer, Heidelberg (2002)
Jürjens J. and Shabalin P. (2004). Automated verification of UMLsec models for security requirements. In: Jézéquel, J.-M., Hußmann, H. and Cook, S. (eds) UML 2004—The Unified Modeling Language, vol. 2460 of Lecture Notes in Computer Science, pp 412–425. Springer, Heidelberg
Jürjens, J., Shabalin, P.: Tools for secure systems development with UML In: FASE 2005, Lecture Notes in Computer Science, Edinburgh, 2–10 April 2005. Springer, Heidelberg
Jürjens, J.: UMLsec webpage, 2002–06. Accessible at http://www.umlsec.org
Jürjens, J.: UMLsec: Extending UML for secure systems development. In: Jézéquel et al. [23], pp. 412–425
Jürjens J. (2004). Secure Systems Development with UML. Springer, Heidelberg
Jürjens, J.: Sound methods and effective tools for model-based security engineering with UML. In: 27th International Conference on Software Engineering (ICSE 2005). IEEE Computer Society (2005)
Kirby, J., Archer, M., Heitmeyer, C.: Applying formal methods to an information security device: An experience report. In: 4th IEEE International Symposium on High Assurance Systems Engineering (HASE 1999), pp. 81–88. IEEE Computer Society (1999)
Koch, M., Parisi-Presicce, F.: Access control policy specification in UML. In: Jürjens et al. [21], pp. 63–78
Kim D.-K., Ray I., France R.B. and Li N. (2004). Modeling role-based access control using parameterized UML models. In: Wermelinger, M. and Margaria, T. (eds) Fundamental Approaches to Software Engineering (FASE 2004), vol. 2984 of Lecture Notes in Computer Science, pp 180–193. Springer, Heidelberg
Lodderstedt, T., Basin, D., Doser, J.: SecureUML: a UML-based modeling language for model-driven security. In: Jézéquel et al. [23], pp. 426–441
Lilius, J., Porres, I.: Formalising UML state machines for model checking. In: France, R.B., Rumpe, B. (eds.) The Unified Modeling Language (UML 1999), vol. 1723 of Lecture Notes in Computer Science, pp. 430–445. Springer, Heidelberg (1999)
Meadows, C.: Open issues in formal methods for cryptographic protocol analysis. In: DARPA Information Survivability Conference and Exposition (DISCEX 2000), pp. 237–250. IEEE Computer Society (2000)
Mouratidis, H., Jürjens, J., Fox, J.: Towards a comprehensive framework for secure systems development. In: 18th International Conference on Advanced Information Systems Engineering (CAiSE 2006), Lecture Notes in Computer Science. Springer, Heidelberg (2006)
Margaria T., Nagel R. and Steffen B. (2005). jETI: A tool for remote tool integration. In: Halbwachs, N. and Zuck, L.D. (eds) 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), vol. 3440 of Lecture Notes in Computer Science, pp 557–562. Springer, Heidelberg
Object Management Group. MOF 1.4 Specification, April 2002. Available at http://www.omg.org/technology/documents/formal/mof.htm
Netbeans project. Open source. Available from http://mdr.netbeans.org (2003)
Novosoft NSUML project. Available from http://nsuml.sourceforge.net/ (2003)
Ober, Iu., Graf, S., Ober, Il.: Validation of UML models via a mapping to communicating extended timed automata. In: SPIN 2004, pp. 127–145 (2004)
Rivest R., Shamir A. and Adleman L. (1978). A method for obtaining digital signatures and public-key cryptosystems. Commun. the ACM 21: 120–126
Schumann J. (1997). Automatic verification of cryptographic protocols with SETHEO. In: McCune, W. (eds) 14th International Conference on Automated Deduction (CADE-14), vol. 1249 of Lecture Notes in Computer Science, pp 87–100. Springer, Heidelberg
Schäfer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. In: Stoller, S.D., Visser, W, (eds.) Workshop on Software Model Checking, vol. 55(3) of Electronical Notes in Theoretical Computer Science. Elsevier, 2001. Satellite event of the 13th International Conference on Computer-Aided Verification (CAV 2001)
The SMV system. Available from http://www-2.cs.cmu. edu/~modelcheck/smv.html
Sindre G. and Opdahl A.L. (2005). Eliciting security requirements with misuse cases. Requir. Eng. 10(1): 34–44
Stoller S.D. (2002). A bound on attacks on authentication protocols. In: Baeza-Yates, R.A., Montanari, U. and Santoro, N. (eds) IFIP TCS, vol 223 of IFIP Conference Proceedings, pp 588–600. Kluwer, Dordrecht
Schmidt, ÁVarró, D.: CheckVML: a tool for model checking visual modeling languages. In: Stevens, P. (ed.) The Unified Modeling Language (UML 2003), vol. 2863 of Lecture Notes in Computer Science, pp. 92–95. 6th International Conference. Springer, Heidelberg (2003)
Object Management Group: OMG Unified Modeling Language Specification v1.5. Version 1.5. OMG Document formal/03-03-01 (2003)
Object Management Group. OMG XML Metadata Interchange (XMI) Specification (2002)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Jürjens, J., Shabalin, P. Tools for secure systems development with UML. Int J Softw Tools Technol Transf 9, 527–544 (2007). https://doi.org/10.1007/s10009-007-0048-8
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-007-0048-8