Forthcoming articles

 


International Journal of Critical Computer-Based Systems

 

These articles have been peer-reviewed and accepted for publication in IJCCBS, but are pending final changes, are not yet published and may not appear here in their final order of publication until they are assigned to issues. Therefore, the content conforms to our standards but the presentation (e.g. typesetting and proof-reading) is not necessarily up to the Inderscience standard. Additionally, titles, authors, abstracts and keywords may change before publication. Articles will not be published until the final proofs are validated by their authors.

 

Forthcoming articles must be purchased for the purposes of research, teaching and private study only. These articles can be cited using the expression "in press". For example: Smith, J. (in press). Article Title. Journal Title.

 

Articles marked with this shopping trolley icon are available for purchase - click on the icon to send an email request to purchase.

 

Articles marked with this Open Access icon are freely available and openly accessible to all without any restriction except the ones stated in their respective CC licenses.

 

Register for our alerting service, which notifies you by email when new issues of IJCCBS are published online.

 

We also offer RSS feeds which provide timely updates of tables of contents, newly published articles and calls for papers.

 

International Journal of Critical Computer-Based Systems (5 papers in press)

 

Regular Issues

 

  • Using Temporal Logics for Specifying Weak Memory Consistency Models   Order a copy of this article
    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 Veri fication of Randomly-scheduled Wireless Sensor Networks   Order a copy of this article
    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   Order a copy of this article
    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   Order a copy of this article
    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 multimedia applications.
    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   Order a copy of this article
    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.
    DOI: 10.1504/IJCCBS.2018.10011234