Combining UML, ASTD and B for the formal specification of an access control filter |
| |
Authors: | J Milhau A Idani R Laleau M A Labiadh Y Ledru M Frappier |
| |
Affiliation: | (1) Laboratoire Logiciels, Syst?mes, R?seaux - IMAG Universit? Joseph Fourier, Grenoble, France |
| |
Abstract: | Combination of formal and semi-formal methods is more and more required to produce specifications that can be, on the one
hand, understood and thus validated by both designers and users and, on the other hand, precise enough to be verified by formal
methods. This motivates our aim to use these complementary paradigms in order to deal with security aspects of information
systems. This paper presents a methodology to specify access control policies starting with a set of graphical diagrams: UML
for the functional model, SecureUML for static access control and ASTD for dynamic access control. These diagrams are then
translated into a set of B machines. Finally, we present the formal specification of an access control filter that coordinates
the different kinds of access control rules and the specification of functional operations. The goal of such B specifications
is to rigorously check the access control policy of an information system taking advantage of tools from the B method. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|