Integrated Formal Methods

We study the use of some verification techniques for reasoning about temporal properties of CommUnity designs. We concentrate on the verification of temporal properties in the context of branching-time temporal logic using the SMV tool.

We also discuss ways of modularising the temporal reasoning, by exploiting the various kinds of morphisms between designs available in CommUnity. Moreover, we combine SMV verification with some abstract interpretation mechanisms to overcome a limitation, with respect to the use of structure for simplification of verification, of CommUnity’s refinement morphisms, the lack of support for data refinement.

A formal specification, written in a mathematical notation, is beyond the comprehension of the average software customer. As a result, the customer cannot provide useful feedback regarding its correctness and completeness. To address this problem, we suggest the formalism expert to work with the customer to create precise scenarios. With only a few simple Z concepts, a precise scenario describes an operation by its effects on the system state. The customer would find a concrete precise scenario easier to understand than its corresponding abstract schema. The Z expert derives schemas based on the precise scenarios. Precise scenarios afford user involvement that improves the odds of a formal specification fully capturing the user requirements.

This paper describes an approach for the automated verification of mobile programs. Mobile systems are characterized by the explicit notion of locations (e.g., sites where they run) and the ability to execute at different locations, yielding a number of security issues. We give formal semantics to mobile systems as Labeled Kripke Structures, which encapsulate the notion of the location net. The location net summarizes the hierarchical nesting of threads constituting a mobile program and enables specifying security policies. We formalize a language for specifying security policies and show how mobile programs can be exhaustively analyzed against any given security policy by using model checking techniques.

We developed and experimented with a prototype framework for analysis of mobile code, using the SATABS model checker. Our approach relies on SATABS’s support for unbounded thread creation and enhances it with location net abstractions, which are essential for verifying large mobile programs. Our experimental results on various benchmarks are encouraging and demonstrate advantages of the model checking-based approach, which combines the validation of security properties with other checks, such as for buffer overflows.

The high-level specification language CSP-OZ-DC has been shown to be well-suited for modelling and analysing industrially relevant concurrent real-time systems. It allows us to model each of the most important functional aspects such as control flow, data, and real-time requirements in adequate notations, maintaining a common semantic foundation for subsequent verification. Slicing on the other hand has become an established technique to complement the fight against state space explosion during verification which inherently accompanies increasing system complexity. In this paper, we exploit the special structure of CSP-OZ-DC specifications by extending the dependence graph—which usually serves as a basis for slicing—with several new types of dependencies, including timing dependencies derived from the specification’s DC part. Based on this we show how to compute a specification slice and prove correctness of our approach.

We present a generic framework of UTP theories for describing systems whose behaviour is characterised by regular time-slots, compatible with the general structure of the

Circus

language [WC01a]. This “slotted-

Circus

” framework is parameterised by the particular way in which event histories are observable within a time-slot, and specifies what laws a desired parameterisation must obey in order for a satisfactory theory to emerge.

Two key results of this work are: the need to be very careful in formulating the healthiness conditions, particularly

R2

; and the demonstration that synchronous theories like SCSP [Bar93] do not fit well with the way reactive systems are currently formulated in UTP and

Circus

.

Safe data abstractions are widely used for verification purposes. Positive verification results can be transferred from the abstract to the concrete system. When a property is violated in the abstract system, one still has to check whether a concrete violation scenario exists. However, even when the violation scenario is not reproducible in the concrete system (a false negative), it may still contain information on possible sources of bugs.

Here, we propose a bug hunting framework based on abstract violation scenarios. We first extract a violation pattern from one abstract violation scenario. The violation pattern represents multiple abstract violation scenarios, increasing the chance that a corresponding concrete violation exists. Then, we look for a concrete violation that corresponds to the violation pattern by using constraint solving techniques. Finally, we define the class of counterexamples that we can handle and argue correctness of the proposed framework.

Our method combines two formal techniques, model checking and constraint solving. Through an analysis of contracting and precise abstractions, we are able to integrate overapproximation by abstraction with concrete counterexample generation.

This paper illustrates a technique to automatically derive intra-object behaviours (in the form of state diagrams) from an object model. We demonstrate how we may take specifications, written in a restricted language of pre- and postconditions, and generate protocols of usage that represent possible behaviours of the generated program. We discuss how to use these state diagrams to analyse the specification for errors, and how to produce correct abstractions to show a particular class of properties of a system. This approach proves successful and scalable for specific domains of application such as database systems and e-commerce websites.

This paper studies the laws of communicating sequential processes (CSP) with Z-like initial and final states. Instead of defining a large semantics including all observable aspects, we incrementally develop the model in three stages: partially correct relational model, then totally correct sequential model and finally the reactive-process model with states. The properties of each model are captured as algebraic laws. A law in one model may or may not be true in its submodels. We apply a technique based on healthiness conditions to identify the conditions for law inheritance. Such abstract conditions themselves can be captured as pattern laws of commutativity. The model uses a new approach to define parallel compositions using just the primitive commands, nondeterministic choice, conjunction and some unary (hiding) operators.

The

Behavior Tree

notation has been developed as a method for systematically and traceably capturing user requirements. In this paper we extend the notation with

probabilistic

behaviour, so that reliability, performance, and other dependability properties can be expressed. The semantics of probabilistic timed Behavior Trees is given by mapping them to probabilistic timed automata. We gain advantages for requirements capture using Behavior Trees by incorporating into the notation an existing elegant specification formalism (probabilistic timed automata) which has tool support for formal analysis of probabilistic user requirements.

Finding inductive invariants is a key issue in many domains such as program verification, model based testing, etc. However, few approaches help the designer in the task of writing a correct and meaningful model, where correction is used for consistency of the formal specification w.r.t. its inner invariant properties. Meaningfulness is obtained by providing many explicit views of the model, like animation, counter-example extraction, and so on. We propose to ease the task of writing a correct and meaningful formal specification by combining a panel of provers, a set-theoretical constraint solver and some model-checkers.

Linearizability is a correctness criterion for concurrent objects. In this paper, we prove linearizability of a concurrent lock-free stack implementation by showing the implementation to be a

non-atomic refinement

of an abstract stack. To this end, we develop a generalisation of non-atomic refinement allowing one to refine a single (Z) operation into a CSP process. Besides this extension, the definition furthermore embodies a termination condition which permits one to prove

starvation freedom

for the concurrent processes.

Commands interpreted in general correctness are usually characterised by their wp and wlp predicate transformer effects. We describe a way to ascribe to such commands a

single

predicate transformer semantics which embodies both their wp and wlp characteristics. The new single predicate transformer describes an everywhere-terminating “lifted” computation in an

ok

-enriched variable space, where

ok

is inspired by Hoare and He’s UTP but has the novelty here that it enjoys the same status as the other state variables, so that it can be manipulated directly in the lifted computation itself.

The relational model of this lifted computation is not, however, simply the canonical UTP relation of the original underlying computation, since this turns out to yield too cumbersome a lifted computation to permit reasoning about efficiently with the mechanised tools available. Instead we adopt a slightly less constrained model, which we are able to show is nevertheless still effective for our purpose, and yet admits a much more efficient form of mechanised reasoning with the tools available.

We extend existing verification methods for CSP-OZ-DC to reason about real-time systems with complex data types and timing parameters. We show that important properties of systems can be encoded in well-behaved logical theories in which hierarchic reasoning is possible. Thus, testing invariants and bounded model checking can be reduced to checking satisfiability of ground formulae over a simple base theory. We illustrate the ideas by means of a simplified version of a case study from the European Train Control System standard.

In this paper we report on modelling and verification of a medium access control protocol for wireless sensor networks, the LMAC protocol. Our approach is to systematically investigate all possible connected topologies consisting of four and of five nodes. The analysis is performed by timed automaton model checking using Uppaal. The property of main interest is detecting and resolving collision. Evaluation of this property for all connected topologies requires more than 8000 model checking runs. Increasing the number of nodes would not only lead increase the state space, but to a greater extent cause an instance explosion problem. Despite the small number of nodes this approach gave valuable insight in the protocol and the scenarios that lead to collisions not detected by the protocol, and it increased the confidence in the adequacy of the protocol.

Different analysis problems for state-transition models can be uniformly treated as instances of temporal logic query-checking, where solutions to the queries are restricted to states. In this paper, we propose a symbolic query-checking algorithm that finds exactly the state solutions to a query. We argue that our approach generalizes previous specialized techniques, and this generality allows us to find new and interesting applications, such as finding stable states. Our algorithm is linear in the size of the state space and in the cost of model checking, and has been implemented on top of the model checker NuSMV, using the latter as a black box. We show the effectiveness of our approach by comparing it, on a gene network example, to the naive algorithm in which all possible state solutions are checked separately.

Event-B is a notation and method for discrete systems modelling by refinement. We introduce a small but very useful construction: qualitative probabilistic choice. It extends the expressiveness of Event-B allowing us to prove properties of systems that could not be formalised in Event-B before. We demonstrate this by means of a small example, part of a larger Event-B development that could not be fully proved before. An important feature of the introduced construction is that it does not complicate the existing Event-B notation or method, and can be explained without referring to the underlying more complicated probabilistic theory. The necessary theory [18] itself is briefly outlined in this article to justify the soundness of the proof obligations given. We also give a short account of alternative constructions that we explored, and rejected.

We present

Prosecco

, a formal model for security protocols of smart card applications, based on Abstract State Machines (ASM) [BS03],[Gur95], and a suitable method for verifying security properties of such protocols. The main part of this article describes the structure of the protocol ASM and all its relevant parts. Our modeling technique enables an attacker model exactly tailored to the application, instead of only an attacker similar to the Dolev-Yao model. We also introduce a proof technique for security properties of the protocols. Properties are proved in the KIV system using symbolic execution and invariants. Furthermore we describe a graphical notation based on UML diagrams that allows to specify the important parts of the application in a simple way.

Our formal approach is exemplified with a small e-commerce application. We use an electronic wallet to demonstrate the ASM-based protocol model and we also show what the proof obligations of some of the security properties look like.

Traditionally, computer simulation techniques are used to perform probabilistic analysis. However, they provide inaccurate results and cannot handle large-scale problems due to their enormous CPU time requirements. To overcome these limitations, we propose to complement simulation based tools with higher-order-logic theorem proving so that an integrated approach can provide exact results for the critical sections of the analysis in the most efficient manner. In this paper, we illustrate the practical effectiveness of our idea by verifying numerous probabilistic properties associated with random variables in the HOL theorem prover. Our verification approach revolves around the fact that any probabilistic property associated with a random variable can be verified using the classical

Cumulative Distribution Function

(CDF) properties, if the CDF relation of that random variable is known. For illustration purposes, we also present the verification of a couple of probabilistic properties, which cannot be evaluated precisely by the existing simulation techniques, associated with the Continuous Uniform random variable in HOL.

Web services are increasingly being applied in solving many universal interoperability problems. Business Process Execution Language (BPEL) is a de facto standard for specifying the behaviour of business process. It contains several interesting features, including scope-based compensation, fault handling and shared label synchronisation. This paper presents a design-based formalism for specifying the behaviour of Web services, and provides new healthiness conditions to capture these new programming features. The new models for handling fault and compensation are built as conservative extension of the standard relational model in the sense that the algebraic laws presented in [14] remain valid. The paper also discusses the links between the new model with the design model, and shows that programs can be transformed to the normal forms within the algebraic framework.

Our work is motivated by practice in Peer-to-Peer networks and Object-Oriented systems where instantiation and dynamically reconfigurable interconnection are essential paradigms. For example, in a Peer-to-Peer network nodes can exchange data to complete tasks. Nodes can leave or join the network at any time. In Object-Oriented systems, an object can be uniquely identified and will communicate with other objects. In this paper we outline a formal framework which supports this kind of interaction so that the integrity of each active object or node is preserved, and so that we can reason about the overall behaviour of the system. The formal framework is based on a combination of the

π

-calculus and the B-Method.

Mondex is a payment system that utilizes smart cards as electronic purses for financial transactions. This paper first reports on how the Mondex system can be modeled, specified and interactively verified using an equation-based method – the OTS/CafeOBJ method. Afterwards, the paper reports on, as a complementarity, a way of automatically falsifying the OTS/CafeOBJ specification of the Mondex system, and how the falsification can be used to facilitate the verification. Differently from related work, our work provides alternative ways of (1) modeling the Mondex system using an OTS (Observational Transition System), a kind of transition system, and (2) expressing and verifying (and falsifying) the desired security properties of the Mondex system directly in terms of invariants of the OTS.

Traditionally, developers of concurrent systems have adopted two distinct approaches: those with

truly concurrent

semantics and those with

interleaving

semantics. In the coarser interleaving interpretation parallelism can be captured in terms of non-determinism whereas in the finer, truly concurrent interpretation it cannot. Thus processes

a

 ∥ 

b

and

a

.

b

 + 

b

.

a

are identified within the interleaving approach but distinguished within the truly concurrent approach.

In [5] we explored the truly concurrent notions of

conflict

, whereby transitions can occur individually but not together from a given state, and

confusion

, whereby the conflict set of a given transition is altered by the occurrence of another transition with which it does not interfere. We presented a translation from the truly concurrent formalism of Petri nets to the interleaving process algebra CSP and demonstrated how the CSP model-checker FDR can be used to detect the presence of both conflict and confusion in Petri nets. This work is of interest firstly because, to the author’s knowledge, no existing tool for Petri nets can perform these checks, and secondly (and perhaps more significantly) because we bridged the gap between truly concurrent and interleaving formalisms, demonstrating that true concurrency can be captured in what is typically considered to be an interleaving language.

In this paper we build on the work presented in [5] further embedding the truly concurrent notions of conflict and confusion in the interleaving formalism CSP by extending the domain of our translation from the simplistic subset of

safe

Petri nets, in which each place can hold at most one token, to standard Petri nets, in which the number of tokens in each place is unbounded.

This paper investigates the use of the probabilistic and continuous extensions of action systems in the development and calculation of reliability of continuous, real-time systems. Rather than develop a new semantics to formally combine the existing extensions, it investigates a methodology for using them together, and the conditions under which this methodology is sound. A key feature of the methodology is that it simplifies the development process by separating the probabilistic calculations of system reliability from the details of the system’s real-time, continuous behaviour.

Integrated formal specifications are intrinsically difficult to (automatically) verify due to the combination of complex data and behaviour. In this paper, we present a method for

decomposing

specifications into several smaller parts which can be independently verified. Verification results can then be combined to make a global result according to the original specification.

Instead of relying on an

a priori

given structure of the system such as a parallel composition of components, we compute the decomposition by ourselves using the technique of

slicing

. With less effort, significant properties can be verified for the resulting specification parts and be applied to the full specification. We prove correctness of our method and exemplify it according to a specification from the rail domain.

We present the architecture and implementation of the

proz

tool to validate high-level Z specifications. The tool was integrated into

prob

, by providing a translation of Z into B and by extending the kernel of

prob

to accommodate some new syntax and data types. We describe the challenge of going from the tool friendly formalism B to the more specification-oriented formalism Z, and show how many Z specifications can be systematically translated into B. We describe the extensions, such as record types and free types, that had to be added to the kernel to support a large subset of Z. As a side-effect, we provide a way to animate and model check records in

prob

. By incorporating

proz

into

prob

, we have inherited many of the recent extensions developed for B, such as the integration with CSP or the animation of recursive functions. Finally, we present a successful industrial application, which makes use of this fact, and where

proz

was able to discover several errors in Z specifications containing higher-order recursive functions.

Multi-agent systems provide an increasingly popular solution in problem domains that require management of uncertainty and a high degree of adaptability. Robustness is a key design criterion in building multi-agent systems. We present a novel approach for the design of robust multi-agent systems. Our approach constructs a model of the design of a multi-agent system in Alloy, a declarative language based on relations, and checks the properties of the model using the Alloy Analyzer, a fully automatic analysis tool for Alloy models. While several prior techniques exist for checking properties of multi-agent systems, the novelty of our work is that we can check properties of coordination and interaction, as well as properties of complex data structures that the agents may internally be manipulating or even sharing. This is the first application of Alloy to checking properties of multi-agent systems. Such unified analysis has not been possible before. We also introduce the use of a formal method as an integral part of testing and validation.

We port verification techniques for device drivers from the Windows domain to Linux, combining several tools and techniques into one integrated tool-chain. Building on ideas from Microsoft’s

Static Driver Verifier

(SDV) project, we extend their specification language and combine its implementation with the public domain bounded model checker CBMC as a new verification back-end. We extract several API conformance rules from Linux documentation and formulate them in the extended language SLICx. Thus SDV-style verification of temporal safety specifications is brought into the public domain. In addition, we show that SLICx, together with CBMC, can be used to simulate preemption in multi-threaded code, and to find race conditions and to prove the absence of deadlocks and memory leaks.

The verification of cryptographic protocol

specifications

is an active research topic and has received much attention from the formal verification community. By contrast, the black-box testing of actual

implementations

of protocols, which is, arguably, as important as verification for ensuring the correct functioning of protocols in the “real” world, is little studied. We propose an approach for checking secrecy and authenticity properties not only on protocol specifications, but also on black-box implementations. The approach is compositional and integrates ideas from verification, testing, and learning. It is illustrated on the Basic Access Control protocol implemented in biometric passports.

Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although they are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support.

Fsp

is a widely-used calculus equipped with

Ltsa

, a graphical and user-friendly tool.

Lotos

is the only process calculus that has led to an international standard, and is supported by the

Cadp

verification toolbox. We propose a translation from

Fsp

to

Lotos

. Since

Fsp

composite processes are hard to encode into

Lotos

, they are translated into networks of automata which are another input language accepted by

Cadp

. Hence, it is possible to use jointly

Ltsa

and

Cadp

to validate

Fsp

specifications. Our approach is completely automated by a translator tool we implemented.

In this paper, we introduce a common semantic framework for developing and formally modeling use cases and task models. Use cases are the notation of choice for functional requirements specification and documentation, whereas task models are used as a starting point for user interface design. Based on their intrinsic characteristics we devise an intermediate semantic domain for use cases and for task models, respectively. We describe how the intermediate semantic domain for each model is formally mapped into a common semantic domain which is based on sets of partial order sets. We argue that a two-step mapping results in a semantic framework that can be more easily validated, reused and extended. As a partial validation of our framework we provide a semantics for ConcurTaskTrees (CTT) one of the most popular task model notations as well as our own DSRG use case formalism. Furthermore we use the common semantic model to formally define a satisfiability relation between task model and use case specifications.

We present an approach to modelling Abadi-Cardelli-style object calculi as Unifying Theories of Programming (UTP) designs. Here we provide a core object calculus with an operational

small-step evaluation rule

semantics, and a corresponding UTP model with a denotational

relational predicate

semantics. For clarity, the UTP model is defined in terms of an operand stack, which is used to store the results of subprograms. Models of a less operational nature are briefly discussed. The consistency of the UTP model is demonstrated by a structural induction proof over the operations of the core object calculus. Overall, our UTP model is intended to provide facilities for encoding both object-based and class-based languages.

An increasing interest in “Systems of Systems”, that is, Systems comprising a varying number of interconnected sub-systems, raises the need for automated verification techniques for dynamic process creation and a changing communication topology. In previous work, we developed a verification approach that is based on finitary abstraction via Data-Type Reduction. To be effective in practice, the abstraction has to be complemented by non-trivial assumptions about valid communication behaviour, so-called non-interference lemmata.

In this paper, we mechanise the generation and validation of these kind of non-interference properties by integrating ideas from communication observation and counter abstraction. We thereby provide a fully automatic procedure to substantially increase the precision of the abstraction.

We explain our approach in terms of a modelling language for dynamic communication systems, and use a running example of a car platooning system to demonstrate the effectiveness of our extensions.

Development of computerized embedded control systems is difficult because it brings together systems theory, electrical engineering and computer science. The engineering and analysis approaches advocated by these disciplines are fundamentally different which complicates reasoning about e.g. performance at the system level. We propose a light-weight approach that alleviates this problem to some extent. An existing formal semantic framework for discrete event models is extended to allow for consistent co-simulation of continuous time models from within this framework. It enables integrated models that can be checked by simulation in addition to the verification and validation techniques already offered by each discipline individually. The level of confidence in the design can now be raised in the very early stages of the system design life-cycle instead of postponing system-level design issues until the integration and test phase is reached. We demonstrate the extended semantic framework by co-simulation of VDM++ and bond-graph models on a case study, the level control of a water tank.