54 datasets found

In this report, we present the application of the CADP verification toolbox to check the correctness of an industrial protocol for deploying and configuring...

tau-confluence is a reduction technique used in explicit state model-checking of labeled transition systems to avoid the state explosion problem. In this report, we...

In prior work, Fournet et al. proposed an extension of the join calculus with class-based inheritance, aiming to provide a precise semantics for concurrent objects....

We consider products of transition systems, that we representas tile systems. Tile systems can be viewed as Petri nets¸: places are replaced by (state) variables, and...

This article introduces probabilistic cluster branching processes, a probabili- stic unfolding semantics for untimed Petri nets with no structural or safety...

This article introduces a probabilistic unfolding semantics for untimed Petri nets. No structural or safety assumptions are made. We show that cluster semantics is an...

We propose a type system to ensure the property of noninterference in a system of concurrent programs, described in a standard imperative language enriched with...

Compositional verification is a way to avoid state explosion for the enumerative verification of complex concurrent systems. Process algebras such as Lotos are...

Fair threads are cooperative threads run by a fair scheduler which gives them equal access to the processor. Fair threads can communicate using broadcast events, and...

In this paper we study an asynchronous distributed $\pi$-calculus, with constructs for localities and migration. We show that a simple static analysis ensures the...

One describes the way to produce finite states machines from programs written in Junior, a formalism for reactive programming in Java. The paper proposes the notion of...

Projet MCR

We introduce the programming model consisting of pre-ordered transition systems (Spots) for modeling synchronous and asynchronous concurrent systems in the presence of...

We define Junior as a Java framework kernel for reactive programming with broadcast events. We give Junior a formal semantics based on rewriting rule. We also describe...

This paper investigates structural properties of occurrence (Petri) nets and their interpretation as unfolding semantics of Petri net systems. Occurrence nets (ONs)...

We present a concurrent Completion procedure based on the use of a SOUR graph as data structure. The procedure has the following characteristics. It is asynchronous,...

We present a new synchronous programming language named \Name{SL} based on \Name{Esterel}, in which hypothesis about signal presences or absences are not allowed....

When analyzing, testing or debugging a distributed program, an important question one has to answer is: ``Does this computation satisfy a given property~?''. We are...

Most computer programs are concurrent ones: they need to perform several tasks at the same time. Threads and events are two common techniques to implement concurrency....

Concurrency is concerned with systems of multiple computing agents that interact with each other. Bisimilarity is one of the main representatives of these. Concurrent...