Catálogo de publicaciones - libros

For specifying and verifying branching-time requirements, a reactive system is traditionally modeled as a labeled tree, where a path in the tree encodes a possible execution of the system. We propose to enrich such tree models with “jump-edges” that capture observational indistinguishability: for an agent , an -labeled edge is added between two nodes if the observable behaviors of the agent along the paths to these nodes are identical. We show that it is possible to specify information flow properties and partial information games in temporal logics interpreted on this enriched structure. We study complexity and decidability of the model checking problem for these logics. We show that it is PSPACE-complete and EXPTIME-complete respectively for fragments of CTL and -calculus-like logics. These fragments are expressive enough to allow specifications of information flow properties such as “agent does not reveal (a secret) until agent reveals (a password)” and of partial information games.

is an extension of which provides generic heuristics for directed model checking. In this approach, the traversal of the state space is guided by a heuristic function which estimates the distance of a search state to the nearest error state. Our tool combines two recent approaches to design such estimation functions. Both are based on computing an abstraction of the system and using the error distance in this abstraction as the heuristic value. The abstractions, and thus the heuristic functions, are generated fully automatically and do not need any additional user input. needs less time and memory to find shorter error paths than ’s standard search methods.

Models in process algebra with abstract data types can be analysed by state space generation and reduction tools. The CRL toolset implements a suite of distributed verification tools for clusters of workstations. We illustrate their application to large case studies from a wide range of application areas, such as functional analysis, scheduling, security analysis, test case generation and game solving.

We propose a framework for reasoning about unbounded dynamic networks of infinite-state processes. We propose Constrained Petri Nets (CPN) as generic models for these networks. They can be seen as Petri nets where tokens (representing occurrences of processes) are colored by values over some potentially infinite data domain such as integers, reals, etc. Furthermore, we define a logic, called CML (colored markings logic), for the description of CPN configurations. CML is a first-order logic over tokens allowing to reason about their locations and their colors. Both CPNs and CML are parametrized by a color logic allowing to express constraints on the colors (data) associated with tokens.

We investigate the decidability of the satisfiability problem of CML and its applications in the verification of CPNs. We identify a fragment of CML for which the satisfiability problem is decidable (whenever it is the case for the underlying color logic), and which is closed under the computations of post and pre images for CPNs. These results can be used for several kinds of analysis such as invariance checking, pre-post condition reasoning, and bounded reachability analysis.

Our main objective is to combine partial-order methods with verification techniques for infinite-state systems in order to obtain efficient verification algorithms for concurrent infinite-state systems. Partial-order methods are commonly used in the analysis of finite systems consisting of many parallel components. In this paper we propose an extension of these methods to parallel compositions of infinite-state systems. We argue that it is advantageous to model each component by an event structure as this allows us to exhibit the concurrency present implicitly in some infinite-state systems such as automata with queues or counters. We generalize the notion of complete prefix from 1-safe Petri nets to all well-structured transition systems. We give an on-the-fly unfolding algorithm which given event structures representing the components produces an event structure representing their synchronized product. A prototype implementation demonstrates the benefits of our approach.

We give a simple and efficient method to prove safety properties for parameterized systems with linear topologies. A process in the system is a finite-state automaton, where the transitions are guarded by both local and global conditions. Processes may communicate via broadcast, rendez-vous and shared variables. The method derives an over-approximation of the induced transition system, which allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency. We have implemented a prototype which works well on several mutual exclusion algorithms and cache coherence protocols.