Workshop en el marco del proyecto DATE SticAmSud

El próximo día Viernes 1 de Noviembre desde las 9:30hs en la Salita Smith, realizaremos un workshop en el marco del projecto DATE (Distributed DiAgnosability and TEstability of Faulty Systems) SticAmSud.

Dicho workshop está dirigido a investigadores y alumnos de postgrado. Los temas que se tocarán están relacionados con el testing formal y el análisis de la diagnosticabilidad de sistemas.

Organiza: Laura Brandán Briones

Programa tentativo:

9:30 - "Unfolding-based Test Selection for Concurrent Conformance" (Hernan Ponce de Leon)
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!" (Stefan 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 R. 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.
Powered by Drupal