Newsfeeds
Most recent issue published online in the International Journal of Critical Computer-Based Systems.
International Journal of Critical Computer-Based Systems
-
Towards a hybrid formal analysis technique for safety-critical software architectures
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.
-
Towards compositional verification of synchronous reactive systems
We present work towards a compositional design approach that will lead designers to develop safe reactive systems. To this end, we extend the theory of I/O-automata that is widely used for modelling reactive systems with composition operator required for dealing with a specific assembly of such systems: systems that consist of a chain of components arranged so that the output of each component is the input of the next, and behave like pipelines. We show that the proposed composition operator ensures semantics preserving of reactive components models. The paper presents a general result on correct-by-construction approach for reactive systems design.
-
An SMT-based approach for generating trace examples and counter-examples of parametric properties
The ParTraP language has been designed to express temporal and timed properties on finite execution traces of parametric events. It aims to ease properties' expression for users not experienced in formal methods. In this paper, we propose an approach that allows generating trace examples and counter-examples in an understandable fashion in order to help such users to better express requirements. So, ParTraP properties are mapped into a satisfiability modulo theories (SMT) context to be fed to Z3 SMT solver to check satisfaction and produce interpretations. A tool named ParTraP-EG is dedicated to that purpose. We report experiments carried out on a set of properties from an industrial case study of computer-aided surgery system.