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

Authors

  • Ammar Boucherit Ferhat Abbas University , Computer Science Department, El Bez Campus, 19000, Setif
  • Laura M. Castro MADS research Group A coruña University Campus de Elviña
  • Abdallah Khababa Ferhat Abbas University , Computer Science Department, El Bez Campus, 19000, Setif
  • Osman Hasan NUST University, School of Electrical Engineering and Computer Science (SEECS) NUST Campus H-12, Islamabad

DOI:

https://doi.org/10.5755/j01.itc.47.3.20330

Keywords:

Access Control System, Model-Checking, Petri nets, Property-Based Testing, Rewriting Logic

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

Author Biography

Laura M. Castro, MADS research Group A coruña University Campus de Elviña

 

 

 

 

Downloads

Published

2018-09-10

Issue

Section

Articles