SENVA 2006 Workshop
Venosc (Isère)

Monday June 12, 2006

9h45

Workshop Opening

10h15 – 11h30

Jaco van de Pol (SENVA)

Fixpoint Equation Systems

Both Boolean Equation Systems (BES) and Parameterized Boolean Equation Systems (PBES) are instances of Fixpoint Equation Systems (FES) over arbitrary complete lattices. We show how a number of basic theorems can be proved for FES, generalizing some results from the literature on BES and PBES. These results include the basic ingredients for Gauss elimination. We claim that the theory and proofs are smoother at the FES level than at PBES level. FESs can be easily formalized in higher-order logic. With relatively little effort, we could verify all our proofs in the interactive theorem prover PVS.

Coffee Break

11h45 – 13h00

Hubert Garavel (SENVA) — on behalf of the VASY team

An Overview of CADP 2006

In this talk, we present the essential features of CADP 2006, the next stable version of the CADP (Construction and Analysis of Distributed Processes) toolbox. CADP 2006 provides advanced verification and performance evaluation features and, above all, a unified framework in which the major state space reduction techniques can be combined (including compositional verification, on-the-fly verification, partial order reduction, static analysis, and massively parallel verification). We summarize the main evolutions of the toolbox since 2001 and present the new CADP tools as well as significant enhancements brought to existing tools. Finally, we list a few directions for the post-2006 versions of CADP.

Lunch

14h45 – 16h00

Rodolfo S. Gomez (University of Kent) — joint work with Howard Bowman

Timelocks in Timed Automata

Formal verification of timed automata models (and models for real-time systems in general) cannot be trusted unless the model is timelock-free. A timelock is a state where time cannot diverge; i.e., once a timelock is reached, executions cannot pass time beyond a certain bound.

Clearly, timelocks are counterintuitive (real systems cannot stop time) and are caused by errors in the model (and the interpretation of urgency and synchronisation in timed automata). Timelocks upset verification because states of interest may become unreachable after a timelock occurs. For instance, a safety property may hold in a model just because time stops before a "bad" state could be reached. However, timelocks are not implementable, and so this bad state may still occur in some implementation of the model. Moreover, in general, non-divergent executions should be avoided during verification.

Some real-time model-checkers provide support for timelock detection (based on liveness properties), but there is room for improvement. This talk gives an overview on the problem of timelocks and available detection methods, and explores other ways to guarantee timelock-freedom which exploit the syntax of loops in timed automata.

16h05 – 16h35

Gwen Salaün (SENVA) — joint work with Jeff Kramer (Imperial College), Frédéric Lang, and Jeff Magee (Imperial College)

Translating FSP into LOTOS

Process algebras are abstract and formal languages widely used to describe concurrent systems. Many process algebras have already been proposed since Robin Milner and Tony Hoare opened the way 25 years ago. However, although they are based on the same core of behavioural operators, most of them are incompatible in practice. We aim at filling the gap between process algebras, and especially making possible the joint use of underlying tool support.

In this presentation, we focus on FSP and LOTOS. FSP is a very popular process algebra equipped with LTSA, a graphical and user-friendly tool. LOTOS is the only process algebra that has led to an international standard, and was applied successfully to many complex systems in several application domains. LOTOS is supported by CADP, a toolbox made up of many validation and verification tools.

We propose a translation from FSP to LOTOS which is automated by a prototype we are implementing. We chose this direction because (i) FSP is a simple yet expressive notation to easily write specifications (ii) CADP is a rich verification toolbox. Our goal is to enable one to use jointly LTSA and CADP to analyse FSP specifications.

Coffee Break

17h05 – 17h45

Manuel Baclet (ENSEEIHT)

Around Hopcroft's Algorithm

We propose a reflection on an indeterminism inherent to Hopcroft's minimization algorithm: the splitter choice. We have implemented two natural policies (FIFO and FILO) for managing the set of splitters for which we obtain the following practical results: the FILO strategy performs better than the FIFO strategy. In the case of a one letter alphabet, the FILO practical complexity never exceeds a linear one and our implementation is more efficient than the minimization algorithm of the FSM tool. This implementation is being integrated in a finite automata library, the Dash library. Thus, we present an efficient manner to manipulate automata by using canonical minimal automata.

17h45 – 19h00

David Champelovier and Frédéric Lang (SENVA)

Translating the LOTOS NT Data Part into LOTOS Abstract Data Types

Process algebras such as LOTOS and mCRL are aimed to model realistic asynchronous concurrent systems. They contain both a process part to represent the ordering of process events and a data part to represent the data manipulated by processes, either internally or via message exchanges.

LOTOS and mCRL's data parts are based on ADTs (Abstract Data Types), in which operations are defined by mathematical equations. There exist powerful tools for dealing with ADTs, such as the CAESAR.ADT code generator for model checking developed by VASY or the theorem provers developed by SEN2. However, in industry, ADTs are not as popular as algorithmic or object-oriented programming languages. It is therefore difficult to find trained ADTs specifiers that can take advantage of the tools developed in SENVA.

To overcome this situation, the VASY team defined in 1998 a new language called LOTOS NT, whose syntax and semantics are closer to standard algorithmic languages. In many respects, LOTOS NT is close to (but simpler than) the E(nhanced)-LOTOS language defined in the ISO standard 15437 adopted in 2001. In 2003, the SENVA team launched the SPART initiative, which aimed at re-thinking LOTOS NT to make it suitable for both formal reasoning and industrial dissemination.

In this talk, following the motivations of SPART, we will present an algorithm and demonstrate a tool called Lnt2Lotos that translate the data part of LOTOS NT into LOTOS ADTs. The algorithm is based on a previous algorithm proposed in 2005 by Ponsini, Fedele, and Kounalis (University of Nice) to translate a subset of C into equational theories. We extended this algorithm to handle additional features, such as constructor types, ``case'' statements, “out” and “inout” (reference passing) function parameters, operator overloading, break statements, return statements, and “uncatchable” exceptions.

Lnt2Lotos is currently used by BULL to model the critical parts of its next generation high-end servers.

Dinner

Tuesday June 13, 2006

9h10 – 10h00

Michael Weber (SENVA) — joint work with Moritz Hammer

"To Store or Not To Store" Replayed

Behrmann et al. posed the question whether “To Store or Not To Store” states during reachability analysis, in order to counter the effects of the well-known state space explosion problem. Their answer was to store not all but only some strategical states. They pay in run-time if the answer too often is “Not To Store”. We propose a different strategy to adaptively trade time for space: “To Store” as many states as memory limits permit. If free memory becomes scarce, we gradually swap states out to secondary storage. We are careful to minimize revisits, and I/O overhead, and also stay sound, i.e. on termination it is guaranteed that the full state space has been explored. It is also available for counterexample reconstruction. In our experiments we tackled state spaces of industrial-scale models with more than 10^9 explicit states with still modest storage requirements.

10h00 – 11h10

Anton Wijs (SENVA) — joint work with Mohammad Torabi Dashti

Guided State Space Exploration Using Beam Search

State space explosion is still the main problem in the area of model checking. This paper focuses on using beam search, a heuristic search algorithm, for pruning state spaces while generating. Original beam search is adapted to the state space generation setting and two new variants, motivated by some practical case studies, are devised. To show the flexibility of the proposed framework, a partial order reduction algorithm for security protocols is extended and then represented as a variant of beam search. These techniques have all been implemented in the mCRL toolset. A case study on a fair exchange protocol is also illustrated.

Coffee Break

11h30 – 12h00 

Manuel Baclet (ENSEEIHT)

An Automata-Based Framework to Simulate and Verify SoC at the Transaction Level

As the complexity of designed Systems on Chip (SoC) augments, due to the ever growing number of transistors that can be integrated on a chip, the demand for formal methods to validate designs before their manufacturing is increasing.  Currently, the method that is the most used is based on software simulation.

We propose an automaton-based high level formalism that allows to model a SoC at the transaction level i.e. by abstracting the labels and the data values. Models of complex components can be obtained in a modular way from models of their sub-components thanks to a particular suitable automata product. Due to classical results on automata theory, components can thus be compared automatically at the transition level. Our modelization process allows also to derive (in a modular way) a program that simulates a given component.

We illustrate the interest of our approach on the example of an IDCT (Inverse Discrete Cosinus Transform) chip, signal processing component.

12h00 – 12h25

Abdul-Malik Khan (SENVA) — joint work with Gregor Gößler and Frédéric Lang

Combination of Compositional Verification Techniques for Embedded Systems

This talk is related to verification of concurrent systems, which contain many components running in parallel and interacting with each other.

One of the problems of verification is the explosion of state space as the number of components increases. To address this problem, compositional verification method is used, which generates the state space for each component separately, reduces them and combine them in parallel. The resultant system is once again reduced using some equivalence relations like bisimulation. Our objective is to combine two different verification tools, namely Prometheus and CADP, so as to get better results of verification by using both tools.

Prometheus uses symbolic verification method, while CADP uses enumerative verification method.

The entry model of Prometheus consists of three layers each describing the behaviour of components, their interaction with each other and the restrictions on the system's actions and states, respectively.

The strategy used in this project is to translate each of the models separately into a respective equivalent model in the CADP tool. The behaviour part is translated into an equivalent behaviour specified in a portion of LOTOS, which we call XLOTOS for our purpose here. The interaction and execution models are translated into Exp language, which uses the Exp.Open compiler of CADP to be further translated to BCG (binary coded graph) format.

12h25 – 13h00

Wendelin Serwe (SENVA) — joint work with Hubert Garavel and Gwen Salaün

Translating CHP’s Probe Operation to LOTOS

Hardware Process Algebras, such as Balsa, CHP (Communicating Hardware Processes), or HASTE, are a natural approach for the description of asynchronous hardware designs. These algebras extend classical process algebras with particular operations, in the case of CHP the "probe", exploiting the hardware implementation of synchronisation using handshake protocols. In the context of the system-on-chip design center INRIA/Leti, we are developing a translation from CHP to LOTOS, so as to allow the use of CADP for the analysis of CHP designs. In this talk, we present different translation schemes for the probe operation, and show the benefits of using specialised translations of the probe operation.

Lunch

14h40 – 15h45

Li Su (University of Kent) — joint work with Howard Bowman and Phil Barnard

Process Algebraic Modelling of Human Cognition

For a long time, cognitive psychologists have been developing cognitive theories, which are both broad in scope and practically applicable. Such theories are aimed at understanding how all the different components of the mental mechanism are configured, what representations those components use and the overall dynamics of their interactions in real time. Interacting Cognitive Subsystems or ICS is one of these theories. However, such theories present a challenge for computational modelling. In order to account for the distributed control, compositionality and interaction required by such theories, we use process algebra (LOTOS) to model the attentional blink effect following the framework of ICS. The model explains how semantic similarity and emotion can affect human's ability to attention. The model was simulated with CADP toolbox using EXEC/CAESAR environment.

15h45 – 16h20

Wan Fokkink (SENVA)

Analysis of a Distributed Lift System

In 2001, Groote, Pang, and Wouters analyzed an existing distributed lift system in mCRL. In 2003, Pang, Karstens, and Fokkink analyzed a redesign of this system using both mCRL and UPPAAL. Recently, Fokkink, Kakebeen, and Pang adapted and extended the UPPAAL model. Firstly, we refined the synchronization mechanism between lifts, to explain a new problem that was reported by the developers of the lift system, and to propose a solution for it. Secondly, we allow a lift to enter a halt state, after which the entire system should make an emergency stop, for instance because a lift meets a maximum height threshold. Using the UPPAAL model checker it was verified that the adapted lift system satisfies the system requirements.

I will give an overview of these three case studies (with emphasis on the last one) and of the lessons learned.

Coffee Break

16h25 – 16h50

Jerôme Fereyre (SENVA) — joint work with Hubert Garavel, and Radu Mateescu

Distributed Verification : Ongoing Work at VASY

A way to fight against the complexity of verification is to distribute the verification task on a set of machines. The VASY team has already developed tools which take advantage of distributed computing to solve some verification issues. We will first describe the distributed tools available in the CADP toolbox and their evolution. Then, we will present our current work on the distributed resolution of Boolean Equation Systems, in the continuation of Radu Mateescu's work and Christophe Joubert's PhD thesis. Finally, we will give insight about our future steps until the end of the year.

16h50 – 17h30

Nathalie Lépy (SENVA)

Developing an Eclipse Plug-In for CADP

I will explain why developing an eclipse plug-in is relevant for the Vasy project and what the issues are. A short presentation of what Eclipse is and a description of its architecture and workbench will be given. I will describe in more detail the Eclipse plug-in extension, the main Eclipse concept. I will illustrate it with the Eclipse CADP plug-in I'm currently developing. To conclude, a list of the present functionalities and of what it remains to do will be made out.

17h30 – 18h10

Jens Calamé (SENVA) — joint work with Natalia Ioustinova and Jaco van de Pol

Towards Automatic Generation of Parameterized Test Cases from Abstractions

For a software test, test cases must be developed, which is a costly and error-prone process. Model-based test generation tools support this process by automatically generating test cases from a system model given, for instance, in UML. However, these tools usually can handle systems of a rather limited size only. The introduction of data can lead to the well-known problem of state space explosion, which limits the applicability of enumerative tools.

Here, we propose an approach to generate test cases combining data abstraction, enumerative test generation methods and constraint solving. Given the concrete specification of a possibly infinite system, data abstraction allows to derive an abstract system, which is finite w.r.t. input and output data. This is suitable for the automatic generation of abstract test cases with enumerative tools like TGV. The abstract test cases then need to be parameterized with actual test data, in order to execute them. For data selection, we make use of constraint solving techniques: a set of constraints is derived from the system specification and then solved by a constraint solver. The parameterized test cases can then be executed by, for instance, TTCN-3.

Dinner

Wednesday June 14, 2006

9h00 – 10h00

Sylvain Peyronnet (EPITA) — joint work with Richard Lassaigne and Thomas Hérault

Approximate Probabilistic Verification

We study the existence of efficient approximation methods to verify quantitative specifications of probabilistic systems. Models of such systems are labelled discrete time Markov chains and checking specifications consists of computing satisfaction probabilities of linear temporal logic formulas. We prove that, in general, there is no polynomial time randomized approximation scheme for probabilistic verification. However, in many applications, specifications can be expressed by monotone formulas or negation of monotone formulas. We show how some simple randomized approximation algorithms can improve the efficiency of verification of such probabilistic specifications. Moreover, we give some possible extensions of our algorithms and demo a tool (APMC) that implements such algorithms in a distributed framework.

10h00 – 10h30

Natalia Ioustinova (SENVA) — joint work with Jens Calamé and Jaco van de Pol

Bug Hunting with False Negatives

Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs.

Here we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from an abstract violation scenario. The violation pattern represents multiple violation scenarios, increasing the chance that a corresponding concrete violation exists. Then we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques.

Coffee Break

10h45 – 11h45

Radu Mateescu and Damien Thivolle (SENVA)

MCL: A Model Checking Language for Concurrent Value-Passing Systems 

Model checking is a successful technique for verifying automatically temporal properties of concurrent finite-state programs represented as Labelled Transition Systems (LTSs). Among the various formalisms used for specifying properties, an outstanding candidate is the modal mu-calculus, a very powerful fixed point-based temporal logic. However, in spite of its theoretical expressiveness, standard modal mu-calculus is a too low-level formalism for end-users, making the specification of complex properties tedious and error-prone. In this talk, we propose MCL (Model Checking Language), an extension of the modal mu-calculus with high-level, data-based constructs inspired from programming languages, which substantially increase its expressive power as well as the conciseness and readability of properties. We also present an on-the-fly model checking method for verifying MCL formulas on LTSs, based upon translating the verification problem into the resolution of a boolean equation system. The MCL language and the associated verification method are supported by the EVALUATOR 4.0 model checker, developed within the CADP verification toolbox using the generic OPEN/CAESAR environment for on-the-fly exploration of LTSs.

Lunch

13h00

Workshop Closing