International Journal of Critical Computer-Based Systems (5 papers in press)
Using Temporal Logics for Specifying Weak Memory Consistency Models
by Maximilian Senftleben, Klaus Schneider
Abstract: The formal verification of multithreaded programs is not just more difficult due to the concurrent behaviours, but also due to the used underlying weak memory consistency models. Weak memory models arise from techniques like store buffering that were introduced to increase the performance. However, all of these techniques weaken the memory consistency, and may result in unintuitive behaviours where processors may disagree on the order in which write operations occurred. A requirement for verification are therefore unambiguous and complete specifications of such memory consistency models. In the past, specifications based on different formalisms have been presented which often lacked of comparability and the direct usability for model checking. In this paper, we therefore introduce the use of temporal logic to describe the behaviour of memory systems. In particular, we use Linear Temporal Logic (LTL) to define the weak memory models. Thereby, we can easily check the properties of a multithreaded program against several different consistency models and determine the weakest consistency guarantees required to fulfill the given specification.
Keywords: weak memory model; memory model; weak memory consistency; memory consistency; weak consistency; memory specification; specification; temporal logic; model checking; verification; LTL.
Formal Probabilistic Performance Verification of Randomly-scheduled Wireless Sensor Networks
by Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid
Abstract: Energy efficiency in Wireless Sensor Networks (WSN) is one of the most critical issue regardless of the target application. While scheduling sensors by partitions to preserve energy is a simple and intuitive approach in\r\nthis context, it is also important to not compromise on the main performance requirements of the considered application. For mission-critical WSN applications, different Quality of Service (QoS) requirements on network performance have to be met. Besides, various assumptions, may effectively impact the sensing performance capabilities of the network. Nevertheless, most analysis techniques focus on the average performance values, and does not consider neither the targeted QoS requirements, nor the probabilistic feature of the algorithm. Based on the theorem proving approach, we first provide, in this paper, an accurate formal analysis of the network lifetime maximization problem, under QoS constraints, for randomly-scheduled wireless sensor networks.\r\nAfter that, we tackle the higher-order-logic formalization of the intrusion coverage intensity, for a modified version of the randomized scheduling, with more realistic assumptions for the intrusion object, in a two or three dimensional plane.
Keywords: Theorem proving ; Wireless sensor networks ; Node scheduling ; Performancernanalysis ; Network lifetime ; Intrusion coverage.
Special Issue on: VECoS'2015/16 Modelling and Verification
A Model Based Approach to Combine Conformance and Load Tests: An eHealth Case Study
by Moez Krichen, Afef Jmal, Mariam Lahami
Abstract: In this paper, we propose a new model-based framework that combines both conformance and load tests in the context of real-time systems. Our new framework is based on the model of extended timed automata with inputs/ouputs and shared integer variables. In addition, we define a new extended timed input output conformance relation etioco. This latter allows to compare a given implementation with respect to its specifications considering load conditions. We also discuss some modelling issues and we provide a new technique for deriving analog-clock tests from the specification of the System Under Test (SUT). In order to show the relevance of our approach, we report on a critical case study from the healthcare field. An important contribution in this work was to use a rich formalism to model multi-user systems and to combine conformance and load tests in the same model. This point constitutes an important testing area that is usually misunderstood.
Keywords: Model-Based Software Testing; Conformance/Load Tests; Extended Timed Automata; Test Generation; Real-Time Systems.
Performance Evaluation of Stochastic Real-Time Systems with the SBIP Framework
by Ayoub Nouri, Braham Lotfi Mediouni, Marius Bozga, Jacques Combaz, Saddek Bensalem, Axel Legay
Abstract: The SBIP framework consists of a stochastic real-time component-
based modelling formalism and a statistical model checking engine. The former
is built as a stochastic extension of the real-time BIP formalism and enables
the construction of stochastic real-time systems in a compositional way. The
statistical engine implements a set of statistical algorithms for the quantitative
and qualitative assessment of probabilistic properties. The paper provides a
thorough introduction to the SBIP formalism and the associated verification
method. In a second part, it surveys several case studies about modelling
and verification of real-life systems, including various network protocols and
Keywords: Stochastic Systems; Real-time; Component-based; Formal Models; Generalised Semi-Markov Process; GSMP; BIP; Statistical Model Checking; SMC; Performance Evaluation.
Fault Diagnosis of Discrete-Event systems Based on the Symbolic Observation Graph
by Abderraouf Boussif, Mohamed Ghazel, Kais Klai
Abstract: Fault diagnosis of Discrete-Event Systems (DESs) has received a lot of attention in industry and academia during the last two decades. In DESbased diagnosis, the two main discussed topics are offline diagnosability analysis and online diagnosis. A pioneering approach that led to the development of various techniques is based on the so-called diagnoser, which is a deterministic automaton used for both diagnosability analysis and online diagnosis if the system is diagnosable. However, this approach suffers from the combinatorial explosion problem due to the exponential complexity of construction. Thus, the diagnoser approach is no longer adequate when dealing with large complex systems. To partially overcome this problem, an efficient approach to construct a symbolic diagnoser is proposed in this paper. The proposed approach consists in constructing a diagnoser based on the Symbolic Observation Graph (SOG), which combines symbolic and enumarative representations in order to build a determinitic observer from a partially observed model. The symbolic observation graph was firstly used for the formal verification using event-based modelchecking as an efficient alternative to the Kripke structure. Besides, the construction of the diagnoser as well as the verification of diagnosability are performed simultaneously on the fly, which can considerably reduce the generated state space of the diagnoser and thus the overall running time. In order to evaluate the efficiency and the scalability of the proposed approach, some experimental and comparative results relatively to other existing methods are presented and discussed, on the basis of a DES benchmark.
Keywords: Discrete-Event Systems; Diagnosability Analysis; Symbolic Observer Graph; On-the-Fly Verification.