The Open UniversitySkip to content

A UML-based static verification framework for security

Siveroni, Igor; Zisman, Andrea and Spanoudakis, George (2010). A UML-based static verification framework for security. Requirements Engineering, 15(1) pp. 95–118.

Full text available as:
PDF (Accepted Manuscript) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (370kB) | Preview
DOI (Digital Object Identifier) Link:
Google Scholar: Look up in Google Scholar


Secure software engineering is a new research area that has been proposed to address security issues during the development of software systems. This new area of research advocates that security characteristics should be considered from the early stages of the soft- ware development life cycle and should not be added as another layer in the system on an ad-hoc basis after the system is built. In this paper we describe a UML-based Static Verification Framework (USVF) to support the design and verification of secure software systems in early stages of the software development life-cycle taking into consideration security and general requirements of the software system. USVF performs static verification on UML models consisting of UML class and state machine diagrams extended by an action language. We present an operational semantics of UML models, define a property specification language designed to reason about tempo- ral and general properties of UML state machines us- ing the semantic domains of the former, and implement the model checking process by translating models and properties into Promela, the input language of the SPIN model checker. We show that the methodology can be applied to the verification of security properties by rep- resenting the main aspects of security, namely availability, integrity and confidentiality, in the USVF property specification language.

Item Type: Journal Item
Copyright Holders: 2009 Springer-Verlag London Limited
ISSN: 1432-010X
Extra Information: Special Issue on RE'09: Security Requirements Engineering; Guest Editors: Eric Dubois and Haralambos Mouratidis
Keywords: UML; security requirements; model checking; SPIN
Academic Unit/School: Faculty of Science, Technology, Engineering and Mathematics (STEM) > Computing and Communications
Faculty of Science, Technology, Engineering and Mathematics (STEM)
Item ID: 41494
Depositing User: Andrea Zisman
Date Deposited: 10 Dec 2014 09:44
Last Modified: 08 Dec 2018 02:41
Share this page:


Altmetrics from Altmetric

Citations from Dimensions

Download history for this item

These details should be considered as only a guide to the number of downloads performed manually. Algorithmic methods have been applied in an attempt to remove automated downloads from the displayed statistics but no guarantee can be made as to the accuracy of the figures.

Actions (login may be required)

Policies | Disclaimer

© The Open University   contact the OU