AC2Alloy &TA is the outcome of a research which attempts to model Access Control Specification in the context of Spatio-Temporal Role Based Access Control using formal methods (Alloy & Timed Automata), Thus allowing for powerful automatic analysis to be carried out.
The project AC2Alloy&TA includes two tools: AC2Alloy which is a model driven approach that automates the transformation between Spatio-Temporal Role Based Access Control (STRBAC) specification and Alloy and AC2Uppaal which is a model driven approach that automates the transformation between Spatio-Temporal Role Based Access Control (STRBAC) model, Timed Automata and Timed Computation Tree Logic (TCTL) statements.
AC2Alloy is an Eclipse Plug-in application that makes use of the Model Driven Architecture (MDA) technology (SiTra) to auto-generate Alloy from Access Control specification in the context of STRBAC model. AC2Alloy transforms the STRBAC specification into XML representation of the STRBAC specification, and then an Alloy model will be automatically generated from the XML representation. The produced Alloy model can then be automatically analysed using Alloy Analyser, which is a SAT-solver based identify an erroneous design.
AC2Uppaal is an Eclipse Plug-in application for integrating STRBAC, Timed Automata and Timed Computation Tree Logic (TCTL) into a single tool. It enables the user to create STRBAC specification and transform them into XML representation Automatic. The XML representation of the STRBAC model is automatically transformed into Time Automata and TCTL statements. The produced Timed Automata and TCTL statements will be modelled and verified using the model checker Uppaal to detect conflicts in the STRBAC specifications.