International Journal of Critical Computer-Based Systems (9 papers in press)
Smart Homes IoT Techniques for Dynamic Provision of Cloud Benefactors
by P. Sanjeevi, Viswanathan Perumal
Abstract: Present years have realized the expansion of computing settings for IoT (Internet of Things) amenities, which switch huge amounts of data using several devices that are continuously associated to networks. Since the information communication and amenities arise on an assortment of devices, such as household appliances, embedded devices, and sensor nodes, the dynamic provision of IoT cloud benefactors necessities are progressively important at this juncture. This work is based on IoT for home automation which is a collection of sensors controlled by microcontroller. Through microcontroller, we direct data to the cloud server for sharing the sensor data to the cloud server and accessed through mobile app. We used cloud server as Ubidots for monitoring the sensors like Gas, Flame, Sound, and Temperature. The main inspiration of this work is to alert communication through smartphone and email on any abnormal constraint. This work is intended to decrease data transmit, decrease time, cost operative and easy to use.
Keywords: Internet of Things; Cloud server; Home Automation; RFID.
Performance evaluation of a novel redundancy method for videoconferencing traffic in MPLS networks
by Mohamad Chaitou
Abstract: Performance evaluation of computer networks using mathematical modeling is widely used in assessing the advantages and drawbacks of any new mechanism before its deployment. In this contribution, we introduce a new mechanism that aims at rerouting multi-point to multi-point (MP2MP) traffic such as videoconferencing in Multi Protocol Label Switching- Traffic Engineering (MPLS-TE) networks. Then we develop a stochastic model in order to evaluate the amelioration incurred by our proposal compared to the existing approaches. In particular, we assess two criterions: the scalability and bandwidth efficiency. Our results show that our proposed method leads to better scalability while reducing the ratio of bandwidth wastage such as traffic duplication observed in the existing mechanisms. Our proposed rerouting mechanism contains two parts. First, we define the concept of MP2MP TE tunnel in MPLS as opposed to the existing MP2MP connectionless tunnel (i.e. without support of TE features such as bandwidth reservation and fast reroute in case of link and/or node failure). Second, we explain how to build a MP2MP TE bypass tunnel that is how to encapsulate a primary MP2MP TE tunnel into a backup MP2MP TE tunnel in order to provide the fast redundancy feature.
Keywords: Mathematical modeling; stochastic models; MPLS-TE; fast reroute,
Analysing Timed Compatibility of Web Service Choreography
by Maya Souilah Benabdelhafid, Béatrice Bérard, Mahmoud Boufaida
Abstract: Web Services become the most mature implementation of the Service Oriented Computing (SOC) paradigm. The verification of behavioural compatibility is then necessary to ensure correct composition of services, which depends not only on qualitative properties such as absence of deadlock but also on some quantitative properties related to performance. Most of the proposed approaches verify the composition in service orchestration modelling. However, service choreography is more collaborative in nature and describes direct interactions between services. Although many existing approaches use Petri Nets (PNs) and Colored PNs (CPNs) to analyse behavioural compatibility, few of them explore time constraints. We propose to model service interactions in a choreography with Timed CPNs and perform automatic verification and simulation using CPN Tools. We evaluate our approach with a case study from the Algerian e-Government, where we show how to verify global time constraints for the renewal of biometric passports.
Keywords: Web Service; Choreography; Compatibility; Composition; Formal Modelling; Timed CPNs; Time Constraints; Performance Analysis; Simulation; CPN Tools.
Verification of Distributed Systems Involving Bounded-Time Migration
by Bogdan Aman, Gabriel Ciobanu
Abstract: We introduce and study a prototyping language for real-time distributed systems involving bounded-time migration and communication. The time constraints of this language are expressed as bounded intervals given by real numbers used to model faithfully the uncertainty of the delay in migration and communication of processes placed at explicit locations of a distributed system. We provide the operational semantics of this language, and illustrate the new language by an example. Due to a translation of the bounded real-time distributed systems described in rTiMo into a network of timed safety automata, we can use an existing software tool for analyzing their qualitative and quantitative properties.
Keywords: Distributed system; bounded-time; migration; verification.
A Formal Verification of Dynamic Updating in a Java-based Embedded System
by Razika Lounas, Mohamed Mezghiche, Jean-Louis Lanet
Abstract: Dynamic Software Updating (DSU) consists in updating running
programs on the fly without any downtime. This feature is interesting in critical
applications that must run continuously. Because updates may lead to safety errors
and security breaches, the question of their correctness is raised. Formal methods
are a rigorous means to ensure the correctness required by applications using
DSU. In this paper, we present a formal verification of correctness of DSU in a
Java-based embedded system. Our approach is based on three major contributions.
First, a formal interpretation of the semantics of update operations to ensure
type safety of the update. Secondly, we rely on a functional representation of
bytecode, the predicate transformation calculus, and a functional model of the
update mechanism to ensure the behavioral correctness of the updated programs.
It is based on the use of Hoare predicate transformation to derive a specification
of an updated bytecode. Thirdly, we use the functional representation to model
the safe update point detection mechanism. This mechanism guarantees that
none of the updated method active methods are active. This property is called
activeness safety. We propose a functional specification that allows to derive proof
obligations that guarantee the safety of the mechanism.
Keywords: Dynamic software updating; formal methods; weakest precondition calculus; Dynamic update safety.
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.
A Methodological Approach for Checking Safety-Critical Systems Software
by Luis E. Mendoza Morales, Manuel I. Capel
Abstract: The complexity of modern safety-critical systems together with the absence of appropriate software verification tools is one reason for the large number of errors in the design and implementation of these systems. A methodological approach named Formal Compositional Verification Approach that uses model checking techniques to verify safety-critical systems software is presented. This approach facilitates decomposition of complex safety-critical systems software into independently verified individual software components, and establishes a compositional method to verify these systems using state-of-the-art model checkers. Our objective in this paper is to facilitate the description of a safety-critical system software as a collection of verified software components, allowing the software verification of complex safety-critical systems. An application on a real-life software project in the field of mobile phone communication is discussed to demonstrate the applicability of the proposed approach.
Keywords: Methodological approach; Safety-critical systems software; Model checking; Software verification; Software specification; Compositional verification.
Software Semantics and Syntax as a Tool for Automated Test Generation
by Nadia Nahar, Kazi Sakib
Abstract: Test automation saves time and cost by digitizing test generation and execution. The existing techniques fail to produce effective and compilable test scripts for not considering both syntactic and semantic information. The proposed three-layer architecture incorporates these information for generation of proper test scripts. It analyzes the source code for extracting syntax and UML diagrams for obtaining semantics. Class methods and sequence of calls are extracted from UMLs, and syntax for class instantiations and method calls are accumulated from source code to generate unit and integration tests. A case study as well as experiments, conducted on sample Java projects, conform the competence of the generation process along with the generated test scripts.
Keywords: software testing; test automation; automatic test generation; unit testing; integration testing.
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.