Catálogo de publicaciones - libros

This paper presents , a model checker for Multi-Agent Systems (MAS). Differently from traditional model checkers, permits the automatic verification of specifications that use epistemic, correctness, and cooperation modalities, in addition to the standard temporal modalities. These additional modalities are used to capture properties of various scenarios (including communication and security protocols, games, etc.) that may be difficult or unnatural to express with temporal operators only; a small number of applications are presented in Section[4]. Agents are described in by means of the dedicated programming language ISPL (Interpreted Systems Programming Language). The approach is symbolic and uses ordered binary decision diagrams (s), thereby extending standard techniques for temporal logic to other modalities distinctive of agents. and all the examples presented in this paper are available for download [14] under the terms of the GPL license.

We present the tool , which supports MSC-based system development. In particular, it automatically checks high-level MSC specifications for implementability.

Predicate abstraction is a method of synthesizing the strongest inductive invariant of a system expressible as a Boolean combination of a given set of atomic predicates. A predicate selection method can be said to be complete for a given theory if it is guaranteed to eventually find atomic predicates sufficient to prove a given property, when such exist. Current heuristics are incomplete, and often diverge on simple examples. We present a practical method of predicate selection that is complete in the above sense. The method is based on interpolation and uses a “split prover”, somewhat in the style of structure-based provers used in artificial intelligence. We show that it allows the verification of a variety of simple programs that cannot be verified by existing software model checkers.

Abstract interpretation techniques prove properties of programs by computing abstract fixpoints. All such analyses suffer from the possibility of false errors. We present a new counterexample driven refinement technique to reduce false errors in abstract interpretations. Our technique keeps track of the precision losses during forward fixpoint computation, and does a precise backward propagation from the error to either confirm the error as a true error, or identify a refinement so as to avoid the false error.

Our technique is quite simple, and is independent of the specific abstract domain used. An implementation of our technique for affine transition systems is able to prove invariants generated by the StInG tool [19] without doing any specialized analysis for linear relations. Thus, we hope that the technique can work for other abstract domains as well. We sketch how our technique can be used to perform shape analysis by simply defining an appropriate widening operator over shape graphs.

Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model-checking. In this paper, we investigate this concept in the context of sequential (possibly recursive) programs whose statements are given as BDDs. We examine how Craig interpolants can be computed efficiently in this case and propose a new, special type of interpolants. Moreover, we show how to treat multiple counterexamples in one refinement cycle. We have implemented this approach within the model-checker Moped and report on experiments.