General

Committees

Workshop

Useful Links

Invited Speakers

  • Compositional Verification of Timed Systems
    Saddek Bensalem, University Joseph Fourier, Verimag Lab, France


    Abstract: Compositional methods in verification have been developed to cope with state explosion. Generally based on divide-and-conquer principles, these methods attempt to break monolithic verification problems into smaller sub-problems by exploiting either the structure of the system or of the property or both. Compositional reasoning can be used in different manners e.g., for deductive verification, assume-guarantee, contract-based verification, compositional generation, etc. The development of compositional verification for timed systems remains however challenging. State-of-the-art tools for the verification of such systems are mostly based on symbolic state space exploration, using efficient data structures and particularly involved exploration techniques. In the timed context, the use of compositional reasoning is inherently difficult due to the synchronous model of time. Time progress is an action that synchronizes continuously all the components of the system. Getting rid of the time synchronization is necessary for analyzing independently different parts of the system (or of the property) but become problematic when attempting to re-compose the partial verification results. Nonetheless, compositional verification is actively investigated and several approaches have been recently developed exploiting timed interfaces and contract-based assume-guarantee reasoning.

    In this talk, we propose a different approach for exploiting compositionality for analysis of timed systems using invariants. In contrast to exact reachability analysis, invariants are symbolic approximations of the set of reachable states of the system. We show that rather precise invariants can be computed compositionally, from the separate analysis of the components in the system and from their composition glue. This method is proved to be sound for the verification of safety properties. However, it is not complete.


    • Towards a Statistical System Analysis
      Bernd Heidergott, VU Amsterdam University, the Netherlands


      Abstract : This lecture is aimed at stimulating a discussion on the relation between statistics and applied probability/operations research. Academic applied probability/operations research is mainly focused on the mathematical analysis of models that find their motivation in the outside (read, non-academic) world. In preparing a real-life problem for mathematical analysis, a "model" has to be distilled, and once this is done, reality is replaced by this model, which is subsequently analyzed with much energy and analytical rigor. However, hardly ever are the exact model specifications known, and defining parameters of the model under consideration, such as arrival rates in queueing networks, failure rates of servers in reliability models, or demand rates in inventory systems, are only revealed to the analyst by statistics. The classical approach for dealing with such parameter insecurity is to integrate out the system performance with respect to the assumed/estimated distribution of the unknown parameter. We believe that this frequentialistic interpretation of parameter insecurity falls short in addressing the needs of the analyst. This lecture will advocate supporting the analyst by studying the risk incurred by parameter insecurity. Rather than taking an entirely statistical point of view by dismissing "model building" at all, we want to integrate the data-driven statistical nature of model building into the analytical analysis. We will discuss an analytical framework for doing so that allows for separating (i) the (analytical) analysis of the system from (ii) the statistical model for the parameter insecurity. For an inventory example, we will present numerical results illustrating our approach.

      • Fault diagnosis of discrete event systems using Petri nets
        Carla Seatzu, University of Cagliari, Italy


        Abstract : This talk is devoted to the problem of fault diagnosis of discrete event systems. Labeled Petri nets are considered as the reference formalism. A brief state of the art is first proposed, then the attention is focused on an approach to on-line diagnosis based on the notion of basis markings and justifications. Such an approach can be applied both to bounded and unbounded Petri nets whose unobservable subnet is acyclic. In the case of bounded Petri nets it presents the main advantage that the most burdensome part of the procedure may be moved off-line, computing a particular graph called Basis Reachability Graph. Diagnosability analysis is also discussed. In particular, necessary and sufficient conditions for diagnosability are given and a test to study diagnosability is presented. Such a test is based on the analysis of the coverability graph of a special Petri net, called Verifier Net that is built starting from the initial system.