International Journal of Critical Computer-Based Systems (5 papers in press)
uQC: A Property-Based Testing Framework for L4 Microkernels
by Cosmin Dragomir, Lucian Mogosanu, Mihai Carabas, Razvan Deaconescu, Nicolae Tapus
Abstract: As the complexity of software is ever increasing, traditional testing methods are unable to provide a high level of assurance with respect to the absence of implementation errors in software systems. In particular, operating system kernels represent a fundamental software component of computing systems, given their role of mediating user access to hardware resources. At the same time, formal verification of functional correctness of software proves to be a costly and difficult task even for microkernels. Microkernels implement only a minimal set of functionalities, while being relied on for applications with high security and/or safety requirements such as automotive software or dedicated cellular radio processors. We aim to find a trade-off between the strong guarantees of formal verification and the flexibility of traditional software testing methods such as unit testing, in order to verify that an L4 microkernel is ideally bug-free. To this end, we argue that this trade-off is provided by the method called property-based testing; property-based testing starts from a formal specification of the Application Programming Interface (API) and automatically generates test cases that make use of its functionality. In this paper we present the first steps towards this goal. Thus we describe the design and implementation of μQC, a property-based testing framework running as an user space application on top of an L4 microkernel (which we call VMXL4). We then give a summary of μQCs usage and we show that a subset of the L4 microkernel API can be automatically tested with a minimal amount of effort from the programmer.
Keywords: Software Testing; Property-Based Testing; L4 Microkernel; API.
Extending GSPNs for the Modelling, Analysis and Performance Evaluation of Dynamic Systems
by Samir Tigane, Laid KAHLOUL, Samir Bourekkache, Souheib Baarir
Abstract: Cloud-based systems are open systems where resources are theoretically non-limited and the number of connected users/devices varies all the time. These systems are close to dynamic systems where the structure changes at runtime. The objective of this paper is to present a new formalism "Extended Generalized Stochastic Petri Nets (EGSPNs)" dedicated to model, analyse and evaluate the performance of reconfigurable systems. In its basic form, GSPNs extend Petri nets by introducing stochastic time. In this paper, GSPNs are enriched with a set of mechanisms allowing the reconfigurability of their structure at runtime. The new formalism "EGSPNs" is applied to model, analyse and evaluate the performance of a case study.
Keywords: GSPNs; Extended GSPNs; Reconfigurable Systems; Formal Modelling; Performance Evaluation.
On Context-Independent and Context-Aware Cloud Services Substitutability Verification
by Sofiane Bourouz, Nadia Zeghib
Abstract: The composition of web services in cloud computing allows making them cooperative in order to satisfy a client request. However, the substitution of one of these services by another must ensure the proper functioning of the new composition. Hence there is a need to develop adequate methods to verify the services substitution. In this aim, we propose, in the present paper, two verification methods. The first one deals with context-independent substitution and sets if a web service can substitute another one. The second one focuses on context-aware substitution and decides the substitutability of web services in a specific composition. These methods use Open Colored Petri Net (OCNets) as a formal framework for modeling web services and their composition in cloud computing. This model allows the structural analysis of Web services interfaces. For the behavioral verification, we use services automata, which allow capturing OCNets behavior and checking its preservation.
Keywords: Web service; Web services substitutability; Open Colored Petri Nets; Context-awareness; Context-aware; Structural & behavioral verification.
Diagnosability Analysis and Fault Diagnosis of P-Time Labeled Petri Nets
by Patrice Bonhomme
Abstract: This paper addresses the problem of analyzing the diagnosability ofrna P-time labeled Petri net with partial information. Indeed, the set of transitionsrnis partitioned into those labeled with the empty string epsilon called silent (as theirrnfiring cannot be detected) including the faulty transitions and the observable ones.rnThe diagnosability can be defined as the ability to detect the type of a failurernwithin a finite number of steps after its occurrence - the system is then said tornbe diagnosable. The proposed approach is based on the synthesis of a modifiedrnstate observer where the fault transitions are considered as observable allowingrnthe construction of a Sampath-like diagnoser. The novelty of the developedrnapproach resides in the fact that, although the time factor is considered as intervals,rnthe diagnoser is computed thanks to the underlying untimed Petri net structurernof the P-time labeled model considered. Furthermore, the method relies onrnlinear programming techniques and the schedulability analysis of particular firingrnsequences exhibited by the analysis of the obtained diagnoser and does not requirernthe building of the state class graph.
Keywords: Petri nets; fault diagnosis; diagnosability; estimation; time dependent systems.
Special Issue on: VECoS'2015/16 Modelling and Verification
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.