Catálogo de publicaciones - libros

Back and von Wright have developed algebraic laws for reasoning about loops in the refinement calculus. We extend their work to reasoning about probabilistic loops in the probabilistic refinement calculus. We apply our algebraic reasoning to derive transformation rules for probabilistic action systems. In particular we focus on developing data refinement rules for probabilistic action systems. Our extension is interesting since some well known transformation rules that are applicable to standard programs are not applicable to probabilistic ones: we identify some of these important differences and we develop alternative rules where possible. In particular, our probabilistic action system data refinement rules are new.

In order to ensure memory properties of an operating system, it is important to verify the implementation of its heap manager. In the case of an existing operating system, this is a difficult task because the heap manager is usually written in a low-level language that makes use of pointers, and it is usually not written with verification in mind. In this paper, our main contribution is the formal verification of the heap manager of an existing embedded operating system, namely Topsy. For this purpose, we develop in the Coq proof assistant a library for separation logic, an extension of Hoare logic to deal with pointers. Using this library, we were able to verify the C source code of the Topsy heap manager, and to find and correct bugs.

Reasoning about multithreaded object-oriented programs is difficult, due to the non-local nature of object aliasing, data races, and deadlocks. We propose a programming model that prevents data races and deadlocks, and supports local reasoning in the presence of object aliasing and concurrency. Our programming model builds on the multi-threading and synchronization primitives as they are present in current mainstream languages. Java or C# programs developed according to our model can be annotated by means of stylized comments to make the use of the model explicit. We show that such annotated programs can be formally verified to comply with the programming model. In other words, if the annotated program verifies, the underlying Java or C# program is guaranteed to be free from data races and deadlocks, and it is sound to reason locally about program behavior. We have implemented a verifier for programs developed according to our model in a custom build of the Spec# programming system, and have validated our approach on a case study.

UML is widely accepted and extensively used in software modeling. However, using different diagrams to model different aspects of a system brings the risk of inconsistency among diagrams. In this paper, we investigate an approach to check the consistency between the sequence diagrams and statechart diagrams using the SPIN model checker. To deal with the hierarchy structure of statechart diagrams, we propose a formalism called Split Automata, a variant of automata, which is helpful to bridge the statechart diagrams to SPIN efficiently. Compared with the existing work on model checking UML which do not have formal verification for their translation from UML to the model checker, we formally define the semantics and prove that the automatically translated model (i.e. Split Automata) does simulate the UML model. In this way, we can guarantee that the translated model does represent the original model.

Finite-state-machine-based conformance testing has been extensively studied in the literature in the context of centralized test architecture. With a distributed test architecture which involves multiple remote testers, the application of a test sequence may encounter controllability problems. This problem can be overcome by introducing additional external coordination messages exchanged among remote testers. Such an approach requires for extra resources for the communication among remote testers and sometimes suffers from unexpected delay. It is thus desirable to avoid the controllability problem by selecting suitable test sequences. However, this is not always possible. For some finite state machines, we cannot generate a test sequence without using external coordination messages and apply it without encountering controllability problems during testing. In this paper, we present sufficient and necessary conditions on a given finite state machine for constructing test sequences so that it does not involve external coordination messages and its application to the implementation under test is free from controllability problems.

Constraint automata are a semantic model for Reo modeling language. Testing correctness of mapping black-box components in Reo to constraint automata is an important problem in analyzing the semantic model of Reo. This testing requires a suite of test cases that cover the automaton states and transitions and also examine different paths. In this paper, Genetic Algorithm (GA) is employed to generate such suite of test cases. This test data generation is improved by Genetic Symbiosis Algorithm (GSA). The results show that GSA approach brings us a suite of test cases with full coverage of automata states and transitions and also diversity of examined paths.

We present and evaluate an approach for the run-time conformance checking of Java classes against property-driven algebraic specifications. Our proposal consists in determining, at run-time, whether the classes subject to analysis behave as required by the specification. The key idea is to reduce the conformance checking problem to the runtime monitoring of contract-annotated classes, a process supported today by several runtime assertion-checking tools. Our approach comprises a rather conventional specification language, a simple language to map specifications into Java types, and a method to automatically generate monitorable classes from specifications, allowing for a simple, but effective, runtime monitoring of both the specified classes and their clients.

Slicing is one of a number of techniques for reducing the state space of specifications during verification. Unlike techniques as e.g. data abstraction slicing is precise : the slice exactly reflects the property to be verified. This necessitates keeping large parts of the specification. In this paper we relax this requirement and instead compute slices overapproximating the behaviour of the specification. This can lead to substantially smaller slices. We consequently adapt the technique of abstraction refinement to slicing as to improve the slice once a false negative is detected. Slicing thus becomes an incremental method: it starts with a small, minimal part of the specification and successively adds further parts until either the property under interest holds on the slice or a real counterexample is found. We show correctness and termination of our technique.

We show how game semantics, counterexample-guided abstraction refinement, assume-guarantee reasoning and the L ^* algorithm for learning regular languages can be combined to yield a procedure for compositional verification of safety properties of open programs. Game semantics is used to construct accurate models of subprograms compositionally. Overall model construction is avoided using assume-guarantee reasoning and the L ^* algorithm, by learning assumptions for arbitrary subprograms. The procedure has been implemented, and initial experimental results show significant space savings.

Java PathFinder (JPF) is an explicit-state model checker for Java programs. It explores all executions that a given program can have due to different thread interleavings and nondeterministic choices. JPF implements a backtracking Java Virtual Machine (JVM) that executes Java bytecodes using a special representation of JVM states. This special representation enables JPF to quickly store, restore, and compare states; it is crucial for making the overall state exploration efficient. However, this special representation creates overhead for each execution, even execution of deterministic blocks that have no thread interleavings or nondeterministic choices. We propose mixed execution , a technique that reduces execution time of deterministic blocks in JPF. JPF is written in Java as a special JVM that runs on top of a regular, host JVM. mixed execution works by translating the state between the special JPF representation and the host JVM representation. We also present lazy translation , an optimization that speeds up mixed execution by translating only the parts of the state that a specific execution dynamically depends on. We evaluate mixed execution on six programs that use JPF for generating tests for data structures and on one case study for verifying a network protocol. The results show that mixed execution can improve the overall time for state exploration up to 36.98%, while improving the execution time of deterministic blocks up to 69.15%. Although we present mixed execution in the context of JPF and Java, it generalizes to any model checker that uses a special state representation.