Title: Towards a hybrid formal analysis technique for safety-critical software architectures

Authors: Ammar Boucherit; Laura M. Castro; Osman Hasan; Abdallah Khababa

Addresses: Computer Science Department, University of El-Oued, Algeria ' MADS Research Group, A Coruña University, Spain ' SEECS, National University of Sciences and Technology (NUST), Pakistan ' Computer Science Department, Ferhat Abbas University, Setif, Algeria

Abstract: Given the catastrophic damage that bugs in critical systems can inflict on human life and its socio-economic environment, the use of rigorous analysis techniques while developing such systems is getting more and more important especially with the increasingly growing complexity of their architecture. However, the aforementioned growing complexity of such systems architecture leads to many scalability issues for the existing formal specification and verification approaches. This paper presents a novel and scalable formal development approach for critical system software architectures. In particular, our proposal is based on rewriting logic and combines both model checking and property-based testing techniques to bridge the gap between these complementary techniques, and hence overcome the drawbacks of previous attempts to ensure the absence of undesired or unexpected behaviour in the specification and implementation of a critical system.

Keywords: model-checking? safety-critical systems? software architecture? property-based testing? rewriting logic.

DOI: 10.1504/IJCCBS.2021.117993

International Journal of Critical Computer-Based Systems, 2021 Vol.10 No.2, pp.95 - 119

Received: 04 Jan 2020
Accepted: 05 Oct 2020
Published online: 06 Oct 2021 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article