TY - GEN
T1 - A tool for the generation of a secure access control filter
AU - Mai Nguyen, Thi
AU - Mammar, Amel
AU - Laleau, Régine
AU - Hameg, Samir
N1 - Publisher Copyright:
© 2016 IEEE.
PY - 2016/8/23
Y1 - 2016/8/23
N2 - Currently, it is well recognized that coupling graphical and formal notations offers several advantages. Indeed, even if a graphical representation permits to design a visual, synthetic and user-friendly view of the system, it may be source of ambiguity and does not permit any formal verification. Formal methods help to remedy these shortcomings by giving a precise semantics to graphical notations such that it becomes possible to verify a large range of properties and even to generate correct implementations. Nevertheless, users cannot take a full advantage of the benefits of such a combination if it is not supported by an automatic tool that liberates them from the tedious translation activity. Following this direction, the present paper describes the main functionalities of a tool that automatically generates a formal secure access control filter for information systems. The goal of the filter is to regulate the access to data of an information system according to a set of static and dynamic rules. Data are described using a UML class diagram, whereas the static and dynamic rules are modeled using SECUREUML and UML activity diagrams respectively. Basically, the tool automatically generates the B formal specification corresponding to these diagrams and the filter.
AB - Currently, it is well recognized that coupling graphical and formal notations offers several advantages. Indeed, even if a graphical representation permits to design a visual, synthetic and user-friendly view of the system, it may be source of ambiguity and does not permit any formal verification. Formal methods help to remedy these shortcomings by giving a precise semantics to graphical notations such that it becomes possible to verify a large range of properties and even to generate correct implementations. Nevertheless, users cannot take a full advantage of the benefits of such a combination if it is not supported by an automatic tool that liberates them from the tedious translation activity. Following this direction, the present paper describes the main functionalities of a tool that automatically generates a formal secure access control filter for information systems. The goal of the filter is to regulate the access to data of an information system according to a set of static and dynamic rules. Data are described using a UML class diagram, whereas the static and dynamic rules are modeled using SECUREUML and UML activity diagrams respectively. Basically, the tool automatically generates the B formal specification corresponding to these diagrams and the filter.
U2 - 10.1109/RCIS.2016.7549285
DO - 10.1109/RCIS.2016.7549285
M3 - Conference contribution
AN - SCOPUS:84987660318
T3 - Proceedings - International Conference on Research Challenges in Information Science
BT - IEEE RCIS 2016 - IEEE 10th International Conference on Research Challenges in Information Science
A2 - Ralyte, Jolita
A2 - Espana, Sergio
A2 - Souveyet, Carine
PB - IEEE Computer Society
T2 - 10th IEEE International Conference on Research Challenges in Information Science, IEEE RCIS 2016
Y2 - 1 May 2016 through 3 May 2016
ER -