Towards the Formal Development of Software Based Systems: Access Control System as a Case Study

Abstract

Our daily life is increasingly becoming more and more dependent on software as they are being extensively used to control safety and mission-critical systems. This has lead to very stringent verification requirements for ensuring that the software performs as intended. However, the testing based techniques cannot provide a rigorous verification due to limited computational and memory constraints and traditional  formal verification techniques, like model checking and theorem proving, are not too straightforward to work with in the industrial setting. In this paper, as a first step to overcome these limitations, we describe a hybrid property based testing and model checking based technique for verifying both models and implementation of access control systems.
Our approach addresses the model checking of critical properties of access control systems and aims at improving their reliability by using property based testing to analyze the corresponding software code. For illustration purposes, a simple example of an access control system is used.

DOI: http://dx.doi.org/10.5755/j01.itc.47.3.20330