Paper Info
Title
Validation of security-design models using Z
Abstract
This paper is aimed at formally specifying and validating security-design models of an information system. It combines graphical languages and formal methods, integrating specification languages such as UML and an extension, SecureUML, with the Z language. The modeled system addresses both functional and security requirements of a given application. The formal functional specification is built automatically from the UML diagram, using our RoZ tool. The secure part of the model instanciates a generic security-kernel written in Z, free from applications specificity, which models the concepts of RBAC (Role-Based Access Control). The final modeling step creates a link between the functional model and the instanciated security kernel. Validation is performed by animating the model, using the Jaza tool. Our approach is demonstrated on a case-study from the health care sector where confidentiality and integrity appear as core challenges to protect medical records.
Year
DOI
Venue
2011
10.1007/978-3-642-24559-6_19
ICFEM
Keywords
Field
DocType
formal method,functional model,z language,information system,uml diagram,roz tool,jaza tool,security-design model,instanciated security kernel,formal functional specification
Programming language,Security kernel,Software engineering,Unified Modeling Language,Computer science,Role-based access control,Access control,Security policy,Formal methods,Functional specification,Computer security model
Conference
Volume
ISSN
Citations 
6991
0302-9743
8
PageRank 
References 
Authors
0.51
16
3
Name
Order
Citations
PageRank
Nafees Qamar1527.57
Yves Ledru21109.20
Akram Idani311015.56