True Concurrency Semantics: Towards a Verification of Timed Systems

True Concurrency Semantics: Towards a Verification of Timed Systems

Souad Guellati (Université Constantine II, Constantine, Algeria), Ilham Kitouni (Université Constantine II, Constantine, Algeria), Riad Matmat (Université Constantine II, Constantine, Algeria) and Djamel-Eddine Saidouni (Université Constantine II, Constantine, Algeria)
DOI: 10.4018/ijertcs.2014040103
OnDemand PDF Download:
$37.50

Abstract

The model checking algorithms have been widely studied for timed automata, it's a validation technique for automatically verifying correctness properties of finite-state systems, which are based on interleaving semantics. Therefore the actions are assumed instantaneous. To overcome the hypothesis of temporal and structural atomicity of actions, we use the durational actions timed automata model (daTA). This model is based on the maximality semantics. Properties to be verified are expressed using the Timed Computation Tree Logic (TCTL). For dealing with formal verification, the Maximality-based Region Graph (MRG) is defined and an adaptation of the model checking algorithm is proposed. The use of the maximality semantics based verification provides new class of properties related to simultaneous progress of actions at different states.
Article Preview

Introduction

In hard real-time systems, the correctness of the system depends on both logical result of the system behavior and the time at which the results are produced. Such systems are part of many safety critical applications like nuclear reactors, communication networks and avionics systems. Hence, verifying the system properties is needed. Both model checking (Clarke & Emerson, 1981; Queille & Sifakis, 1982; Baier & Katoen, 2008) and theorem proving (Rushby, 2001) may be used for this task.

Several models have been defined for modelling real-time systems. In general, the system is specified using a high-level model, like Petri net based models, real-time process algebra or timed automata model. The specification is then translated to a low-level representation, generally a transition system.

The low-level representation is used for properties verification.

In this paper we are concerned on a model checking validation technique. It’s an automated technique that, given a specification (using a finite state based model) of a system and a property written in some appropriate logical formalism, systematically checks the validity of property.

Real-time model checking (Bernard et al., 2001; Clarke et al., 2000; Baier & Katoen, 2008) has been mostly studied and developed in the framework of timed automata (Alur & Dill, 1994) under the hypothesis that transitions represent atomic actions executions (actions are instantaneous and indivisible). Modelling non atomic actions using timed automata may be done by considering two sequential transitions, the first one models the action start and the second the action end. The action duration is captured by the elapse of time in the intermediate state.

In practice, splitting non atomic actions into start and end actions amplify the problem of state space explosion problem. Modelling non atomic actions without splitting them may be realised under a true concurrency models.

In the literature, the durational actions Timed Automata model (daTA) was proposed in the respect of those requirements, (Saidouni & Belala, 2006; Kitouni et al., 2012; Belala et al., 2013) they are a form of timed automata that admit a more natural representation of action durations and advocates carrying true concurrency. It’s based on maximality semantics (Saidouni et al., 2008).

Maximality semantics has been proved necessary and sufficient for both the refinement process and duration of actions (Saidouni et al., 2008). In (Saidouni & Courtiat, 2003) a real-time process language D-LOTOS is proposed supporting maximality semantics and daTA model has been defined (Saidouni & Belala, 2006). A nice characterization of the model was presented in (Kitouni et al., 2012) concerning determinizability and decidability of the model. More recently, daTA is defined as a semantic support of temporally timed Petri nets (Belala et al., 2013).

Interleaved interpretations of concurrency are justified by assumption that all actions are atomic a direct consequence is that no two actions can occur simultaneously. In the opposite, models based on maximality semantics present concurrent actions differently from choice. So daTA model allows i) to carry duration of actions, which is realistic assumption for specifying in a natural way systems and ii) to consider true concurrency.

Complete Article List

Search this Journal:
Reset
Open Access Articles: Forthcoming
Volume 8: 2 Issues (2017)
Volume 7: 2 Issues (2016)
Volume 6: 2 Issues (2015)
Volume 5: 4 Issues (2014)
Volume 4: 4 Issues (2013)
Volume 3: 4 Issues (2012)
Volume 2: 4 Issues (2011)
Volume 1: 4 Issues (2010)
View Complete Journal Contents Listing