Towards a hybrid formal analysis technique for safety-critical software architectures Online publication date: Wed, 06-Oct-2021
by Ammar Boucherit; Laura M. Castro; Osman Hasan; Abdallah Khababa
International Journal of Critical Computer-Based Systems (IJCCBS), Vol. 10, No. 2, 2021
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.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Critical Computer-Based Systems (IJCCBS):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com
Our Blog 
Follow us on Twitter 
Visit us on Facebook