DATE

Distributed DiAgnosability and TEstability of Faulty Systems

DATE is a scientific-technological cooperation program between Argentina, Chile and France, funded by the regional program STIC-AmSud (No.13STIC-04).

Institutions involved

  • FaMAF, Universidad Nacional de Córdoba, Argentina
  • UACH, Universidad Austral de Chile, Chile
  • LRI, Université Paris-Sud, France

Reserchers involved

  • Laura Brandán Briones (FaMAF, Universidad Nacional de Córdoba)
  • Gonzalo Bonigo (FaMAF, Universidad Nacional de Córdoba)
  • Patricio Hubmann (FaMAF, Universidad Nacional de Córdoba)
  • Agnes Madalinski (UACH, Universidad Austral de Chile)
  • Philippe Dague (LRI, Université Paris-Sud)
  • Delphine Longuet (LRI, Université Paris-Sud)
  • Fatiha Zaïdi (LRI, Université Paris-Sud)
  • Huu Nghia Nguyen (LRI, Université Paris-Sud)
  • Lina Ye (LRI, Université Paris-Sud)

Research domain

Formal analysis of diagnosability and testability in distributed and concurrent systems, formally modelled with labelled transition systems and Petri nets.

Project goals

  • Distributed testing of concurrent systems
    • Studying and designing analysis techniques for decentralised and distributed testing. Developing algorithms for test generation.
    • Investigating the verification of testability in decentralised and distributed domains.
  • Distributed diagnosability
    • Investigating distributed diagnosability using different formal methods such as automata based techniques and Petri net based analysis methods.
    • Analysing diagnosability in distributed systems with different synchronisations between their sub-systems
  • Developing a formal framework to describe both properties (testability and diagnosability)
    • Investigating and integrating formal frameworks of testing and diagnosability in the centralised and distributed domains.
    • Implementing a tool in the centralised and distributed domains.

Abstract

We are facing a numeric world where interleaved embedded devices, such as mechatronic, electronic and software functions, increase considerably inside systems, making them more and more complex. In addition most of these systems are distributed, either by nature (networks, Web applications, etc.) or for privacy reasons (each subsystem model being hidden from other subsystems). They also interact with other subsystems and the environment (physical or human). And a lot are critical. The tasks of formally validating that these systems will operate properly, according to their specifications at design stage, during their functioning, and that any dysfunction due to the occurrence at any moment of some - hardware of software - fault (from a given list of anticipated faults) will be identified without ambiguity in finite time (in order to trigger recovery functions) are thus a major socio-economic concern and a real challenge. They are respectively addressed by testability and diagnosability methods. Both are model-based approaches (using a specification model, correct and faulty models of the system, an observation model, etc.) and rely on model checking techniques ensuring formally that some given properties are satisfied by a model. Though close in their objectives and methods, no unifying framework has been proposed up to now for testability and diagnosability. And attempts to adapt these two methods, traditionally developed for centralized systems, to decentralised or distributed ones are very recent and still preliminary. The aim of the present project is precisely twofold: 1) investigating and designing formal techniques for testability analysis and for diagnosability analysis in distributed concurrent discrete-event systems (modelled with label transition systems or with Petri nets); 2) developing a unifying framework for both testability and diagnosability analysis and implementing a tool according to this framework.

Publications related to the project

  • Lina Ye and Philippe Dague, Undecidable Case and Decidable Case of Joint Diagnosability in Distributed Discrete Event Systems, (journal paper ready for submission).

  • Lina Ye, Philippe Dague and F. Nouioua. Predictability analysis of distributed discrete event systems. 52nd IEEE Conference on Decision and Control CDC 2013, Firenze, Italy, December 2013. [pdf]

  • Laura Brandán Briones and Agnes Madalinski. Distributed Bounded Predictability. Jornadas Chilenas de Computación, the 32nd International Conference of the Chilean Computer Society (SCCC), Temuco, Chile, November 13-15, 2013. [pdf]

  • Hernán Ponce de León, Stefan Haar and Delphine Longuet. Unfolding-based Test Selection for Concurrent Conformance. International Conference on Testing Software and Systems, Istanbul, Turkey, November 13-15, 2013.

  • Hernán Ponce de León, Gonzalo Bonigo and Laura Brandán Briones. Distributed Analysis for Diagnosability in Concurrent Systems. Workshop on Principles of Diagnosis (DX-2013), Jerusalem, Israel, October 2013.

  • Gonzalo Bonigo and Laura Brandán Briones. Diagnosability Behaviour over Faulty Concurrent Systems, Conferencia Latinoamericana en Informática (CLEI 2013), Naiguatá, Venezuela, October 2013.

Organization of events

Workshop held in FaMAF, Universidad Nacional de Córdoba, October 29th and November 1st, 2013.
  • October 29th: Tutorial by Stefan Haar, Introduction to Petri Nets.

  • November 1st: Research talks.

    • 9:30 Unfolding-based Test Selection for Concurrent Conformance (Hernán Ponce de León)
      Model-based testing has mainly focused on models where concurrency is interpreted as interleaving (like the ioco theory for labeled transition systems), which may be too coarse when one wants concurrency to be preserved in the implementation. In order to test such concurrent systems, we choose to use Petri nets as specifications and define a concurrent conformance relation named co- ioco. We propose a test generation algorithm based on Petri net unfolding able to build a complete test suite w.r.t our co-ioco conformance relation. In addition we propose a coverage criterion based on a dedicated notion of complete prefixes that selects a manageable test suite.

    • 10:00 Global and Local Testing from Message Sequence Charts (Delphine Longuet)
      Message Sequence Charts are a widely used formalism for describing scenarios a communicating system must be able to perform. We show in this talk different formal frameworks for testing from MSCs. We first consider a setting where all the processes of the system can be controlled and observed globally. Then we study a setting where the system is tested from the point of view of each process individually, observations remaining local or being gathered at the end of each test. In each setting, we define a conformance relation based on global or local observations, for which we build an exhaustive test set. Moreover, we gather the conditions making local testing as powerful as global testing.

    • 10:30 Verification of diagnosability and predictability with Parallel LTL-X Model Checking Based on Petri Net Unfoldings (Agnes Madalinski)
      Fault diagnosis consists in detecting abnormal behaviours of a physical system. Within the fault diagnosis framework, predictability is a property describing the possibility of predicting a fault before it actually occurs by monitoring the observable behaviour of the system. Predictability implies diagnosability --- an important property that determines the possibility of detecting faults by monitoring the observable behaviour. The difference is that diagnosability ensures that the fault can be eventually detected, maybe long time after its occurrence, while predictability allows to detect the fault before it actually occurs. Predictability makes it possible to react before the fault causes the system to malfunction, e.g. by issuing a warning or taking some preventing measures. We show that the diagnosability and the predictability problem on a Petri net can be re-formulated in terms of LTL-X model checking. The advantage of this is that existing efficient methods and tools can be employed, in particular parallel model checking based on Petri net unfoldings. The experimental results show that this approach is efficient, and a good level of parallelisation can be achieved.

    • 11:30 Reveal your Faults: it's only fair! (Stefar Haar)
      We present a methodology for fault diagnosis in concurrent, partially observable systems with additional fairness constraints. In this weak diagnosis, one asks whether a concurrent chronicle of observed events allows to determine that a non-observable fault will inevitably occur, sooner or later, on any maximal system run compatible with the observation. The approach builds on strengths and techniques of unfoldings of safe Petri nets, striving to compute a compact prefix of the unfolding that carries sufficient information for the diagnosis algorithm. Our work extends and generalizes the unfolding-based diagnosis approaches by Benveniste et al. as well as Esparza and Kern. Both of these focused mostly on the use of sequential observations, in particular did not exploit the capacity of unfoldings to reveal inevitable occurrences of concurrent or future events studied by Balaguer et al.. Our diagnosis method captures such indirect, revealed dependencies. We develop theoretical foundations and an algorithmic solution to the diagnosis problem, and present a SAT solving method for practical diagnosis with our approach.

    • 12:00 Security analysis in probabilistic distributed protocols via bounded reachability (Pedro D'Argenio)
      Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if in addition the system is intended to protect private information. In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze time-bounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.

Participation to seminars and congresses

  • Lina Ye, Conference on Decision and Control CDC 2013, Firenze, Italy, December 2013.
  • Agnes Madalinski, International Conference of the Chilean Computer Society (SCCC), Temuco, Chile, November 13-15, 2013.
  • Laura Brandán Briones, Conferencia Latinoamericana en Informática CLEI 2013, Naiguatá, Venezuela, October 2013.
  • Laura Brandán Briones, Agnes Madalinski, Delphine Longuet, Fatiha Zaïdi and Philippe Dague, DigiCosme (Digital worlds: distributed data, programs and architectures) research day, Paris-Saclay, July 10th, 2013.