Dataset in support of the conference paper "An Event-B Formal Model for Access Control and Resource Management of Serverless Applications"

Dataset title: RHP (Request Handling Pattern) and Authorization Mechanism.

The dataset contains Event-B developments for RHP (Request Handling Pattern) and refinements for authorization mechanism in AWS environment.

It supports the paper "An Event-B Formal Model for Access Control and Resource Management of Serverless Apps" to be presented at ABZ 2024: 10th International Conference on Rigorous State-Based Methods, Bergamo, Italy, June 25-28

This dataset contains:
The Rodin platform archive *AWS-Based_RHP_SSR_Auth_Pattern.zip* and *AWS-Based_RHP_ROP_LSR_cs1_sc1.zip* former contains the RHP pattern devolvement and refinements for authorization mechanism whereas latter contains and Event-B model for a case study scenario by using RHP pattern and the proposed refinement strategy for authorisation mechanism.

The Rodin platform configuration is as follows.
- Rodin Platform 3.7.0 (www.event-b.org)
- Event-B Theory 4.0.0 (Rodin Update Site)
- Atelier B Provers 2.3.0 (Atelier-B Update Site)
- SMT Solvers 1.5.0 (Rodin Update Site)
The archive can be imported into the Rodin platform.