Skip to main content



Invited Talk

Formal Software Verification: How Close Are We?

Spin and its immediate predecessors were originally designed for the verification of data communication protocols. It didn’t take long, though, for us to realize that a data communications protocol is just a special case of a general distributed process system, with asynchronously executing and interacting concurrent processes. This covers both multi-threaded software systems with shared memory, and physically distri- buted systems, interacting via network channels.
The tool tries to provide a generic capability to prove (or as the case may be, to disprove) the correctness of interactions in complex software systems. This means a reliable and easy-to-use method to discover the types of things that are virtually impossible to detect reliably with traditional software test methods, such as race conditions and deadlocks.
As initially primarily a research tool, Spin has been remarkably successful, with well over one million downloads since it was first made available by Bell Labs in 1989. But our goal is te development of a tool that is not only grounded in foundational theory, but also usable by all developers of multi-threaded software, not requiring specialized knowledge of formal methods.
In this talk we try to answer the question how close we have come to reach these goals, and where especially we are still lacking. We will see that our understanding has changed of what a verification tool can do – and what it should do.
Gerard J. Holzmann

Formal UML Modeling

Exploiting the Hierarchical Structure of Rule-Based Specifications for Decision Planning

Rule-based specifications have been very successful as a declarative approach in many domains, due to the handy yet solid foundations offered by rule-based machineries like term and graph rewriting. Realistic problems, however, call for suitable techniques to guarantee scalability. For instance, many domains exhibit a hierarchical structure that can be exploited conveniently. This is particularly evident for composition associations of models. We propose an explicit representation of such structured models and a methodology that exploits it for the description and analysis of model- and rule-based systems. The approach is presented in the framework of rewriting logic and its efficient implementation in the rewrite engine Maude and is illustrated with a case study.
Artur Boronat, Roberto Bruni, Alberto Lluch Lafuente, Ugo Montanari, Generoso Paolillo

Reactive Semantics for Distributed UML Activities

We define a reactive semantics for a subset of UML activities that is suitable as precise design language for reactive software systems. These semantics identify run-to-completion steps for execution on the level of UML activities as so-called activity steps. We show that activities adhering to these semantics and a set of rules lead to event-driven and bounded specifications that can be implemented automatically by model transformations and executed efficiently using runtime support systems.
Frank Alexander Kraemer, Peter Herrmann

Components and Architecture

Statistical Abstraction and Model-Checking of Large Heterogeneous Systems

We propose a new simulation-based technique for verifying applications running within a large heterogeneous system. Our technique starts by performing simulations of the system in order to learn the context in which the application is used. Then, it creates a stochastic abstraction for the application, which takes the context information into account. This smaller model can be verified using efficient techniques such as statistical model checking. We have applied our technique to an industrial case study: the cabin communication system of an airplane. We use the BIP toolset to model and simulate the system. We have conducted experiments to verify the clock synchronization protocol i.e., the application used to synchronize the clocks of all computing devices within the system.
Ananda Basu, Saddek Bensalem, Marius Bozga, Benoît Caillaud, Benoît Delahaye, Axel Legay

Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude

AADL is a standard for modeling embedded systems that is widely used in avionics and other safety-critical applications. However, AADL lacks a formal semantics, and this severely limits both unambiguous communication among model developers, and the development of simulators and formal analysis tools. In this work we present a formal object-based real-time concurrent semantics for a behavioral subset of AADL in rewriting logic, which includes the essential aspects of its behavior annex. Our semantics is directly executable in Real-Time Maude and provides an AADL simulator and LTL model checking tool called AADL2Maude. AADL2Maude is integrated with OSATE, so that OSATE’s code generation facility is used to automatically transform AADL models into their corresponding Real-Time Maude specifications. Such transformed models can then be executed and model checked by Real-Time Maude. We present our semantics, and two case studies in which safety-critical properties are analyzed in AADL2Maude.
Peter Csaba Ölveczky, Artur Boronat, José Meseguer

Testing Probabilistic Distributed Systems

There has been much interest in the testing of systems that have physically distributed interfaces and this has been encouraged by recent trends towards the use of such systems. Most formal work in this area has considered the testing of deterministic systems based on deterministic models. However, distributed systems are usually nondeterministic and often can be seen as probabilistic systems in which required or expected probabilities can be attached to the allowable events. This paper provides a formal testing framework for systems with physically distributed interfaces where nondeterministic decisions among alternatives are probabilistically quantified. It first considers testing from systems where there is a unique type of action. In this setting, a generative interpretation of probabilities is adequate and a formal framework to test these systems is provided. However, the observable events of a system are usually divided into inputs and outputs. In such situations it is necessary to use the reactive interpretation of probabilities.
Robert M. Hierons, Manuel Núñez

Specification and Testing of E-Commerce Agents Described by Using UIOLTSs

In this paper we expand our work in our specification formalism UIOLTSs. We present three implementation relations and provide alternative characterizations of these relations in terms of the tests that the implementation under test successfully passes. In addition, we present the main ideas to obtain an algorithm to derive complete test suites from specifications.
Juan José Pardo, Manuel Núñez, M. Carmen Ruiz

Testing Attribute-Based Transactions in SOC

We set the basis for a theory of testing for distributed transactions in service oriented systems where each service definition is decorated with a transactional attribute (inspired by the Java Transaction API). Transaction attributes discipline how services are executed with respect to the transactional scope of the invoking party.
We define a language of observers and show that, in general, the choice of different transactional attributes causes different system’s behaviours wrt the testing equivalences induced by the observers.
Laura Bocchi, Emilio Tuosto

Joint DisCoTec Session

Grouping Nodes in Wireless Sensor Networks Using Coalitional Game Theory

Wireless sensor networks are typically ad-hoc networks of resource-constrained nodes; in particular, the nodes are limited in power resources. It can be difficult and costly to replace sensor nodes, for instance when implanted in the human body. Data transmission is the major consumer of power, so it is important to have power-efficient protocols. In order to reduce the total power consumption in the network, we consider nodes which cooperate to transmit data. Nodes which cooperate, form a group. A mobile node may at some point be without a group, in which case it is desirable for the node to be able to join a group. In this paper we propose a modification of the AODV protocol to decide whether a node should join a given group, using coalitional game theory to determine what is beneficial in terms of power consumption. The protocol is formalized in rewriting logic, implemented in the Maude tool, and validated by means of Maude’s model exploration facilities.
Fatemeh Kazemeyni, Einar Broch Johnsen, Olaf Owe, Ilangko Balasingham

Timed Process Algebra

Forgetting the Time in Timed Process Algebra

Timeless Behaviour in a Timestamped World
In this paper, we propose the notion of partial time abstraction for timed process algebras, which introduces the possibility to abstract away parts of the timing of system behaviour. Adding this notion leads to so-called partially timed process algebras and partially timed labelled transition systems. We describe these notions, and generalise timed branching bisimilarity to partially timed branching bisimilarity, allowing the comparison of systems with partial timing. Finally, with several examples and a case study, we demonstrate how partial time abstraction can be a useful modelling technique for timed models, which can lead to rigorous minimisations of state spaces.
Anton Wijs

Theory and Implementation of a Real-Time Extension to the π-Calculus

We present a real-time extension to the π-calculus and use it to study a notion of time-bounded equivalence. We introduce the notion of timed compositionality and the associated timed congruence which are useful to reason about the timed behaviour of processes under hard constraints. In addition to this meta-theory we develop an abstract machine for our calculus based on event-scheduling and establish its soundness w.r.t. the given operational semantics. We have built an implementation for a realistic language called kiltera based on this machine.
Ernesto Posse, Juergen Dingel

Timed and Hybrid Automata

Fuzzy-Timed Automata

Timed automata theory is well developed in literature. This theory provides a formal framework to model and test real-time systems. This formal framework supplies a way to describe transitions among states with timing constrains. These constraints are usually expressed with logic formulas involving the system clocks. The time domain of these clocks usually is considered dense, that is, the clocks take values in the real or rational numbers. Dealing with a domain like this can be hard, specially if we consider end points of intervals.
In this paper, we present a modification of the model that allows to use real time in an easier, more powerful and reliable approach for computing systems. Our proposed model exploits the concepts of fuzzy set theory and related mathematical frameworks to get a more flexible approach.
F. Javier Crespo, Alberto de la Encina, Luis Llana

Model Checking of Hybrid Systems Using Shallow Synchronization

Hybrid automata are a widely accepted modeling framework for systems with discrete and continuous variables. The traditional semantics of a network of automata is based on interleaving, and requires the construction of a monolithic hybrid automaton based on the composition of the automata. This destroys the structure of the network and results in a loss of efficiency, especially using bounded model checking techniques. An alternative compositional semantics, called “shallow synchronization”, exploits the locality of transitions and relaxes time synchronization. The semantics is obtained by composing traces of the local automata, and superimposing compatibility constraints resulting from synchronization.
In this paper, we investigate the different symbolic encodings of the reachability problem of a network of hybrid automata. We propose a novel encoding based on the shallow synchronization semantics, which allows different strategies for searching local paths that can be synchronized. We implemented a bounded reachability search based on the use of an incremental Satisfiability-Modulo-Theory solver. The experimental results confirm that the new encoding often performs better than the one based on interleaving.
Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, Stefano Tonetta

Program Logics and Analysis

Heap-Dependent Expressions in Separation Logic

Separation logic is a popular specification language for imperative programs where the heap can only be mentioned through points-to assertions. However, separation logic’s take on assertions does not match well with the classical view of assertions as boolean, side effect-free, potentially heap-dependent expressions from the host programming language familiar to many developers.
In this paper, we propose a variant of separation logic where side effect-free expressions from the host programming language, such as pointer dereferences and invocations of pure methods, can be used in assertions. We modify the symbolic execution-based verification algorithm used in Smallfoot to support mechanized checking of our variant of separation logic. We have implemented this algorithm in a tool and used the tool to verify some interesting programming patterns.
Jan Smans, Bart Jacobs, Frank Piessens

Static Type Analysis of Pattern Matching by Abstract Interpretation

Pattern matching is one of the most attractive features of functional programming languages. Recently, pattern matching has been applied to programming languages supporting the main current object oriented features. In this paper, we present a static type analysis based on the abstract interpretation framework aimed at proving the exhaustiveness of pattern matchings and the safety of type casts. The analysis is composed by two distinct abstract domains. The first domain collects information about dynamic typing, while the second one tracks the types that an object cannot be instance of. The analysis has been implemented and applied to all the Scala library. The experimental results underline that our approach scales up since it analyzes a method in 90 msec in average. In addition, the analysis is precise in practice as well, since we prove the exhaustiveness of 42% of pattern matchings and 27% of the type casts without any manual annotation on the code.
Pietro Ferrara

Reasoning about Distributed Systems

On-the-Fly Trace Generation and Textual Trace Analysis and Their Applications to the Analysis of Cryptographic Protocols

Many model checking methods have been developed and applied to analyze cryptographic protocols. Most of them can analyze only one attack trace of a found attack. In this paper, we propose a very simple but practical model checking methodology for the analysis of cryptographic protocols. Our methodology offers an efficient analysis of all attack traces for each found attack, and is independent to model checking tools. It contains two novel techniques which are on-the-fly trace generation and textual trace analysis. In addition, we apply our method to two case studies which are TMN authenticated key exchanged protocol and Micali’s contract signing protocol. Surprisingly, it turns out that our simple method is very efficient when the numbers of traces and states are large. Also, we found many new attacks in those protocols.
Yongyuth Permpoontanalarp

On Efficient Models for Model Checking Message-Passing Distributed Protocols

The complexity of distributed algorithms, such as state machine replication, motivates the use of formal methods to assist correctness verification. The design of the formal model of an algorithm directly affects the efficiency of the analysis. Therefore, it is desirable that this model does not add “unnecessary” complexity to the analysis. In this paper, we consider a general message-passing (MP) model of distributed algorithms and compare different ways of modeling the message traffic. We prove that the different MP models are equivalent with respect to the common properties of distributed algorithms. Therefore, one can select the model which is best suited for the applied verification technique.
We consider MP models which differ regarding whether (1) the event of message delivery can be interleaved with other events and (2) a computation event must consume all messages that have been delivered after the last computation event of the same process. For generalized MP distributed protocols and especially focusing on fault-tolerance, we show that our proposed model (without interleaved delivery events and with relaxed semantics of computation events) is significantly more efficient for explicit state model checking. For example, the model size of the Paxos algorithm is 1/13 th that of existing equivalent MP models.
Péter Bokor, Marco Serafini, Neeraj Suri

Logics for Contravariant Simulations

Covariant-contravariant simulation and conformance simulation are two generalizations of the simple notion of simulation which aim at capturing the fact that it is not always the case that “the larger the number of behaviors, the better”. Therefore, they can be considered to be more adequate to express the fact that a system is a correct implementation of some specification. We have previously shown that these two more elaborated notions fit well within the categorical framework developed to study the notion of simulation in a generic way. Now we show that their behaviors have also simple and natural logical characterizations, though more elaborated than those for the plain simulation semantics.
Ignacio Fábregas, David de Frutos Escrig, Miguel Palomino


Weitere Informationen

Premium Partner