Formal Methods and Software Engineering

A theory of programming is intended to support the practice of programming by relating each program to the specification of what it is intended to achieve. Our intention is to develop a signal calculus for event-based synchronous languages used for specification and programming of embedded systems. In this paper, we mainly tackle conceptually instantaneous reactions, i.e., zero-time reactions. The delay-time reactions will be investigated in the follow-up work. To explore the semantic definition of instantaneous reactions (I-calculus), a set of algebraic laws is provided, which can be used to reduce all instantaneous reactions to a normal form algebraically. The normal form, surprisingly, exposes the internal implicit dependence explicitly. Consequently, that two differently written reactions happen to mean the same thing can be proved from the equations of an algebraic presentation.

Reasoning about programs has traditionally been done using deductive reasoning, where mathematical logic is used to make proofs that connect programs with specifications. In this talk I describe an approach where an automated reasoning tool approaches program code as a scientist would in the natural world. Instead of just deductive logic, versions of abductive reasoning (generation of new hypotheses) and inductive generalization are used in an iterative fashion to discover specifications that partly describe what programs do, starting from bare code. The resulting specifications are partial or conservative, but the inference/discovery aspect makes it much easier to approach large code bases, quickly, than with the traditional deductive-only approach.

The underlying program logic in this work is separation logic, a logic for reasoning about the way that programs use computer memory, and the inference method attempts to discover a logical assertion describing the program’s footprint: the collection of cells that it touches. Aiming for the footprint provides a strategy to select compact specifications, amongst the enormity of all potential specifications (which would be too many to consider). After describing the inference techniques, I report on experience using a software tool that automates the method, which has been applied to large code bases.

This talk is based on joint work with Cristiano Calcagno, Dino Distefano and Hongseok Yang.

Concurrent programming is difficult. The challenges are foundational: unlike sequential control flow, asynchronous control flow is difficult to understand and reason about. Not surprisingly, even expert programmers find it difficult to write concurrent software. We desperately need software engineering techniques and tools to move concurrent programming from black art to a rigorous engineering discipline. I believe that automated tools that reduce the cognitive burden of reasoning about concurrency can help tremendously in improving the productivity of concurrent programmers. In collaboration with my colleagues at Microsoft Research, I have developed Poirot (http://research.microsoft.com/ en-us/projects/poirot/), a tool for answering semantic queries about a concurrent program by statically searching over its executions. Poirot exploits sequential encodings of concurrent semantics, structural under- and over-approximations for sequential control flow, and advances in automated theorem proving to search concurrent program executions efficiently. Poirot is being used in many different applications—bug detection, program understanding, and symbolic debugging. This lecture will present both a demonstration and an explanation of the techniques underlying the search engine inside Poirot.

Poirot is joint work with Akash Lal and Shuvendu Lahiri.

An important challenge to realize dynamic adaptation is finding suitable components for substitution or interaction according to the current context. A possible solution is checking behavioral equivalence of components in different contexts. Two components are equivalent with respect to a context, if they behave equivalently in that context. In this work, we deal with context-specific behavioral equivalence of PobSAM components. PobSAM is a flexible formal model for developing and modeling evolving self-adaptive systems. A PobSAM model is a collection of actors, views, and autonomous managers. Autonomous managers govern the behavior of actors by enforcing suitable context-based policies. Views provide contextual information for managers to control and adapt the actors behavior. Managers are the core components used to realize adaptation by changing their policies. They are modeled as meta-actors whose configurations are described using a multi-sorted algebra called CA. The behavior of mangers depends on the context in which they are executing. In this paper, we present an equational theory to reason about context-specific behavioral equivalence of managers independently from actors. To this end, we introduce and axiomatize a new operator to consider the interaction of managers and the context. This equational theory is based on the notion of statebased bisimilarity and allows us to reason about the behavioral equivalence of managers as well as the behavioral equivalence of the constitutes of managers (i.e., policies and configurations). We illustrate our approach through an example.

This work provides an underpinning for a systems modelling approach based on UML and fUML together. It uses UML state diagrams as a starting point for modelling system object behaviour abstractly, then refining each state diagram by adding the implementation decisions in a form of a fUML activity diagram. Maintaining behavioural consistency between each UML state diagram and its corresponding fUML activity diagram is an important but difficult task. In this paper we introduce a framework that automates checking such consistency in a practical way.

The framework is based on formalizing these diagrams into the process algebra CSP to do trace refinement checking using FDR2. One of the main contributions in this work is that we transform FDR2 output (counter-example in case of inconsistency) back to the UML/fUML model in a way that allows the modeller to debug the consistency problem. To be able to provide this kind of interactive feedback, the generated CSP model is augmented with traceability information. A case tool plugin based on the Epsilon model management framework has been developed to support our approach.

Safety-Critical Java (SCJ) is a restriction of the Real-Time Specification for Java to support the development and certification of safety-critical applications. It is the result of an international effort from industry and academia. Here we present the first formalisation of the SCJ execution model, covering missions and event handlers. Our formal language is part of the

Circus

family; at the core, we have Z, CSP, and Morgan’s calculus, but we also use object-oriented and timed constructs from the

OhCircus

and

CircusTime

variants. Our work is a first step in the development of refinement-based reasoning techniques for SCJ.

Formal specifications are not an exception for aging. Furthermore, they stay valid resources only in the case when they have been kept up to date during all evolutionary changes taking place. As specifications are then not just written once, an interesting aspect is whether they do also deteriorate or not. In order to answer this question, this paper addresses the issues on various kinds of changes in the development of formal specifications and how they could be measured. For this, a set of semantic-based measures is introduced and then used in a longitudinal study, assessing the specification of the Web-Service Definition Language. By analyzing all 139 different revisions of it, it is shown that specifications can deteriorate and that it takes effort to keep them constantly at high quality. The results yield in a refined model of software evolution exemplifying these recurring changes.

Projection Temporal Logic (PTL) is a sound formalism for specifying and verifying properties of concurrent systems. The modeling, simulation and verification language MSVL for concurrent systems is an executable subset of PTL. However, asynchronous communication, a key component of modeling distributed system, has not been implemented in MSVL. This paper presents asynchronous communication techniques for MSVL to improve its capability for modeling and verifying distributed systems. First, a process structure is defined; then a channel structure and two pairs of communication commands are formalized; finally, an example of asynchronous communication for the contract signing protocol is demonstrated.

Orc

is a computation orchestration language which is designed to specify computational services, such as distributed communication and data manipulation, in a concise and elegant way. Four concurrency primitives allow programmers to orchestrate site calls to achieve a goal, while managing timeouts, priorities, and failures. To guarantee the correctness of

Orc

model, effective verification support is desirable.

Orc

has a highly concurrent semantics which introduces the problem of state-explosion to search-based verification methods like model checking. In this paper, we present a new method, called Compositional Partial Order Reduction (CPOR), which aims to provide greater state-space reduction than classic partial order reduction methods in the context of hierarchical concurrent processes. Evaluation shows that CPOR is more effective in reducing the state space than classic partial order reduction methods.

Programmable Logic Controllers are widely used in industry. Reliable PLCs are vital to many critical applications. This paper presents a novel symbolic approach for analysis of PLC systems. The main components of the approach consists of: (1) calculating the uncertainty characterization of the PLC systems, (2) abstracting the PLC system as a Hidden Markov Model, (3) solving the Hidden Markov Model using domain knowledge, (4) integrating the solved Hidden Markov Model and the uncertainty characterization to form an integrated (regular) Markov Model, and (5) harnessing probabilistic model checking to analyze properties on the resultant Markov Model. The framework provides expected performance measures of the PLC systems by automated analytical means without expensive simulations. Case studies on an industrial automated system are performed to demonstrate the effectiveness of our approach.

The power industry is currently moving towards a more dynamical, intelligent power grid. This

Smart Grid

is still in its infancy and a formal evaluation of the expensive technologies and ideas on the table is necessary before committing to a full investment. In this paper, we argue that a good model for the Smart Grid must match its basic properties: it must be hybrid (both evolve over time, and perform control/computation), distributed (multiple concurrently executing entities), and allow for asynchronous communication and stochastic behaviour (to accurately model real-world power consumption). We propose Distributed Probabilistic-Control Hybrid Automata (Dpcha) as a model for this purpose, and extend Bounded LTL to Quantified Bounded LTL in order to adapt and apply existing statistical model-checking techniques. We provide an implementation of a framework for developing and verifying DPCHAs. Finally, we conduct a case study for Smart Grid communications analysis.

Model Checking real-life systems is always difficult since such systems usually have quantitative timing factors and work in unreliable environment. The combination of real-time and probability in hierarchical systems presents a unique challenge to system modeling and analysis. In this work, we develop an automated approach for verifying probabilistic, real-time, hierarchical systems. Firstly, a modeling language called PRTS is defined, which combines data structures, real-time and probability. Next, a zone-based method is used to build a finite-state abstraction of PRTS models so that probabilistic model checking could be used to calculate the probability of a system satisfying certain property. We implemented our approach in the PAT model checker and conducted experiments with real-life case studies.

Writing formal specifications in a practical software project is likely to increase the time for requirements analysis and/or abstract design and to postpone the implementation, which is often hard to be accepted by the user and/or the manager of the project. Prototyping provides an agile approach for communication between the user and the developer but is unable to deal with all aspects of the system precisely and completely. In this paper, we put forward a new development approach resulting from integrating prototyping techniques into the SOFL three-step modeling approach. The new approach is aimed at achieving a quality development process through promoting the facilities for user-friendly communication between the user and the developer and for exploring all possible aspects of the system precisely. We have applied the approach to develop an IC card software for the Japan railway service system and present the recorded data as the result of the study. Compared to our previous experiences using both formal and informal methods, our study suggests that the new approach can be more practical than existing formal specification methods and more effective in achieving the completeness and accuracy of the user’s requirements than informal specification methods.

The real time dialect of VDM, called VDM-RT, contains constructs for describing concurrent threads, synchronisation of such threads and the distribution of object instances and their threads over multiple CPUs with busses connecting them. Tools that simulate an executable subset of VDM-RT models benefit from being deterministic so that problems are reproducible and can be more easily investigated. We describe the deterministic scheduling features of our VDM-RT interpreter, and show how multi-threaded models can also be debugged deterministically.

The development of the Event-B formal method and the supporting tools Rodin and

ProB

was guided by practical experiences with the B-Method, the Z specification notation, VDM and similar practical formal methods. The case study discussed in this article — a cruise control system — is a serious test of industrial use. We report on where Event-B and its tools have succeeded, where they have not. We also report on advances that were inspired by the case study. Interestingly, the case study was not a pure formal methods problem. In addition to Event-B, it used Problem Frames for capturing requirements. The interaction between the two proved to be crucial for the success of the case study. The heart of the problem was tracing informal requirements from Problem Frames descriptions to formal Event-B models. To a large degree, this issue dictated the approach that had to be used for formal modelling. A dedicated record theory and dedicated tool support were required. The size of the formal models rather than complex individual formulas was the main challenge for tool support.

We apply the Abstract State Machine (ASM) method and the CoreASM tool to design and analysis of Situation Analysis Decision Support (SADS) systems. Realistic situation analysis scenarios routinely deal with situations involving multiple mobile agents reacting to discrete events distributed in space and time. SADS system engineering practices call for systematic formal modeling approaches to manage complexity through modularization, refinement and validation of abstract models. We explore here SADS system design based on ASM modeling techniques paired with CoreASM tool support to facilitate analysis of the problem space and reasoning about design decisions and conformance criteria so as to ensure they are properly established and well understood prior to building the system. We provide an extension to CoreASM for the Marine Safety & Security domain, specifically for capturing rendezvous scenarios. The extension yields the necessary background concepts, such as mobile sensors and shipping lanes, and offers runtime visualization of simulation runs together with an analyzer to measure success of various rendezvous detection strategies used in the model. We illustrate the application of the proposed approach using a sample rendezvous scenario.

The capture, deployment and enforcement of appropriate access control policies are crucial aspects of many modern software-based systems. Previously, there has been a significant amount of research undertaken with respect to the formal modelling and analysis of access control policies; however, only a limited proportion of this work has been concerned with

dynamic

policies. In this paper we explore techniques for the modelling, analysis and subsequent deployment of such policies—which may rely on external data. We use the Alloy modelling language to describe constraints on policies and external data; utilising these constraints, we test static instances constructed from the current state of the external data. We present Gauge, a constraint checker for static instances that has been developed to be complementary to Alloy, and show how it is possible to test systems of much greater complexity via Gauge than can typically be handled by a model finder.

We present a new approach for automated knowledge-based verification of access control policies. The verification method not only discovers if a vulnerability exists, but also produces the strategies that can be used by the attacker to exploit the vulnerability. It investigates the information needed by the attacker to achieve the goal and whether he acquires that information when he proceeds through the strategy or not. We provide a policy language for specifying access control rules and the corresponding query language that is suited for expressing the properties we aim to verify. The policy language is expressive enough to handle integrity constraints and policy invariants. Finally, we compare the results and enhancements of the current method - implemented as a policy verification tool called

PoliVer

- over similar works in the context of dynamic access control policy verification.

This paper is aimed at formally specifying and validating security-design models of an information system. It combines graphical languages and formal methods, integrating specification languages such as UML and an extension, SecureUML, with the Z language. The modeled system addresses both functional and security requirements of a given application. The formal functional specification is built automatically from the UML diagram, using our RoZ tool. The secure part of the model instanciates a generic security-kernel written in Z, free from applications specificity, which models the concepts of RBAC (Role-Based Access Control). The final modeling step creates a link between the functional model and the instanciated security kernel. Validation is performed by animating the model, using the Jaza tool. Our approach is demonstrated on a case-study from the health care sector where confidentiality and integrity appear as core challenges to protect medical records.

Separation logic was developed as an extension to Hoare logic with the aim of simplifying pointer program proofs. A key feature of the logic is that it focuses the reasoning effort on only those parts of the heap that are relevant to a program - so called local reasoning. Underpinning this local reasoning are the

separating conjunction

and

separating implication

operators. Here we present an automated reasoning technique called

mutation

that provides guidance for separation logic proofs. Specifically, given two heap structures specified within separation logic, mutation attempts to construct an equivalence proof using a difference reduction strategy. Pivotal to this strategy is a generalised decomposition operator which is essential when matching heap structures. We show how mutation provides an effective strategy for proving the functional correctness of iterative and recursive programs within the context of weakest precondition analysis. Currently, mutation is implemented as a proof plan within our CORE program verification system. CORE combines results from shape analysis with our work on invariant generation and proof planning. We present our results for mutation within the context of the CORE system.

This paper presents an approach to compositional contract-based verification of Simulink models. The verification approach uses Synchronous Data Flow (SDF) graphs as a formalism to obtain sequential program statements that can then be analysed using traditional refinement-based verification techniques. Automatic generation of the proof obligations needed for verification of correctness with respect to contracts, as well as automatic proofs are also discussed.

We compare two approaches for efficient formal verification of the integration of pipelined processor cores with arrays of reconfigurable functional units. The processors are modeled at a high level of abstraction, using a subset of Verilog, in a way that allows us to exploit the property of Positive Equality that results in significant simplifications of the solution space, and orders of magnitude speedup relative to previous methods. The presented techniques allow us to formally verify the integration of pipelined processors, including complex Digital Signal Processors (DSPs), with arrays of reconfigurable functional units of any size, where the reconfigurable functional units have any design, and for any topology of the connections between them. Such architectures are becoming increasingly used because of their much higher performance and reduced power consumption relative to conventional processors. One of the compared two approaches, which abstracts the entire array of reconfigurable functional units, results in at least 3 orders of magnitude speedup relative to the other approach that models the exact number of reconfigurable functional units and abstracts the design of each and the network that connects them, such that the speedup is increasing with the size of the array. To the best of our knowledge, this is the first work on automatic formal verification of pipelined processors with arrays of reconfigurable functional units.

Although validation of complex dynamic systems can be realised using checklists and simulations provided by tools such as Simulink, these techniques usually do not cover all system behaviours. Moreover, the control laws are rarely modelled together with the system architecture. This integration can reveal defects which are only detected in final stages of the development. This work presents two major contributions: a strategy to validate the integration of a proposed architecture with control laws, based on the

CSP

process algebra; and the validation of a Fly-by-wire Elevator Control System designed by Embraer. The results show that the strategy helps finding defects in early stages of the development, saving time and costs.

Symbolic execution is a technique for systematic exploration of program behaviors using symbolic inputs, which characterize classes of concrete inputs. Symbolic execution is traditionally performed on imperative programs, such as those in C/C++ or Java. This paper presents a novel approach to symbolic execution for declarative programs, specifically those written in Alloy – a first-order, declarative language based on relations. Unlike imperative programs that describe

how

to perform computation to conform to desired behavioral properties, declarative programs describe

what

the desired properties are, without enforcing a specific method for computation. Thus, symbolic execution does not directly apply to declarative programs the way it applies to imperative programs. Our insight is that we can leverage the fully automatic, SAT-based analysis of the Alloy Analyzer to enable symbolic execution of Alloy models – the analyzer generates instances, i.e., valuations for the relations in the model, that satisfy the given properties and thus provides an execution engine for declarative programs. We define symbolic types and operations, which allow the existing Alloy tool-set to perform symbolic execution for the supported types and operations. We demonstrate the efficacy of our approach using a suite of models that represent structurally complex properties. Our approach opens promising avenues for new forms of more efficient and effective analyses of Alloy models.

Distributed hybrid systems present extraordinarily challenging problems for verification. On top of the notorious difficulties associated with distributed systems, they also exhibit continuous dynamics described by quantified differential equations. All serious proofs rely on decision procedures for real arithmetic, which can be extremely expensive. Quantified Differential Dynamic Logic (Qd

$\mathcal{L}$

) has been identified as a promising approach for getting a handle in this domain. Qd

$\mathcal{L}$

has been proved to be complete relative to quantified differential equations. But important questions remain as to how best to translate this theoretical result into practice: how do we succinctly specify a proof search strategy, and how do we control the computational cost? We address the problem of automated theorem proving for distributed hybrid systems. We identify a simple mode of use of Qd

$\mathcal{L}$

that cuts down on the enormous number of choices that it otherwise allows during proof search. We have designed a powerful strategy and tactics language for directing proof search. With these techniques, we have implemented a new automated theorem prover called KeYmaeraD. To overcome the high computational complexity of distributed hybrid systems verification, KeYmaeraD uses a distributed proving backend. We have experimentally observed that calls to the real arithmetic decision procedure can effectively be made in parallel. In this paper, we demonstrate these findings through an extended case study where we prove absence of collisions in a distributed car control system with a varying number of arbitrarily many cars.

Wireless sensor networks (WSNs) are expected to run unattendedly for critical tasks. To guarantee the correctness of WSNs is important, but highly nontrivial due to the distributed nature. In this work, we present an automatic approach to directly verify WSNs built with TinyOS applications implemented in the NesC language. To achieve this target, we firstly define a set of formal operational semantics for most of the NesC language structures for the first time. This allows us to capture the behaviors of sensors by labelled transition systems (LTSs), which are the underlying semantic models of NesC programs. Secondly, WSNs are modeled as the composition of sensors with a network topology. Verifications of individual sensors and the whole WSN become possible by exploring the corresponding LTSs using model checking. With substantial engineering efforts, we implemented this approach in the tool NesC@PAT to support verifications of deadlock-freeness, state reachability and temporal properties for WSNs. NesC@PAT has been applied to analyze and verify WSNs, with

unknown

bugs being detected. To the best of our knowledge, NesC@PAT is the first model checker which takes NesC language as the modeling language and completely preserves the interrupt-driven feature of the TinyOS execution model.

In wireless sensor networks (WSNs), scheduling of the sensors is considered to be the most effective energy conservation mechanism. The random and unpredictable deployment of sensors in many WSNs in the open fields makes the sensor scheduling problem very challenging and thus randomized scheduling algorithms are used. The performance of these algorithms is usually analyzed using simulation techniques, which do not offer 100% accurate results. Moreover, probabilistic model checking, when used, does not include a strong support to reason accurately about statistical quantities like expectation and variance. In this paper, we overcome these limitations by using higher-order-logic theorem proving to formally analyze the coverage-based random scheduling algorithm for WSNs. Using the probabilistic framework developed in the HOL theorem prover, we formally reason about the expected values of coverage intensity, the upper bound on the total number of disjoint subsets, for a given expected coverage intensity, the lower bound on the total number of nodes and the average detection delay inside the network.

We present an approach to prove safety (collision freedom) of multi-lane motorway traffic with lane-change manoeuvres. This is ultimately a hybrid verification problem due to the continuous dynamics of the cars. We abstract from the dynamics by introducing a new spatial interval logic based on the view of each car. To guarantee safety, we present two variants of a lane-change controller, one with perfect knowledge of the safety envelopes of neighbouring cars and one which takes only the size of the neighbouring cars into account. Based on these controllers we provide a local safety proof for unboundedly many cars by showing that at any moment the reserved space of each car is disjoint from the reserved space of any other car.

Achieving high dependability of distributed systems remains a major challenge due to complexity arising from concurrency and communication. There are a number of formal approaches to verification of properties of distributed algorithms. However, there is still a lack of methods that enable a transition from a verified formal model of communication to a program that faithfully implements it. In this paper we aim at bridging this gap by proposing a state-based formal approach to correct-by-construction development of distributed programs. In our approach we take a systems view, i.e., formally model not only application but also its environment – the middleware that supports it. We decompose such an integrated specification to obtain the distributed program that should be deployed on the targeted network infrastructure. To illustrate our approach, we present a development of a distributed leader election protocol.

The main destination of this paper is the industrial milieu. We are concerned with the difficulties encountered by industrial developers who are willing to apply ”new” approaches to software engineering (since they always face the same problem for years: how to develop safe software) but are in fact disappointed by what is proposed to them. We try to characterize what the relevant constraints of industrial software projects are and then propose a

simple methodology

able to face the real problem. It is based on the usage of Event-B [1] and is illustrated by means of an

industrial project

.

Event-B is a formal method which is widely used in modelling safety critical systems. So far, the main properties of interest in Event-B are safety related. Even though some liveness properties, e,g, termination, are already within the scope of Event-B, more general liveness properties, e.g. progress or persistence, are currently unsupported. We present in this paper proof rules to reason about important classes of liveness properties. We illustrate our proof rules by applying them to prove liveness properties of realistic examples. Our proof rules are based on several proof obligations that can be implemented in a tool support such as the Rodin platform.

Specification mining techniques are used to automatically infer interaction specifications among objects in the format of call sequences, but many of these specifications can be meaningless or insignificant. As a consequence, when used in program testing or formal verification, the presence of these leads to false positive defects, which in turn demand much effort for manual investigation. We propose a novel process for determining and extracting significant specifications from a set of mined specifications using

mutation testing

. The resulting specifications can then be used with program verification to detect defects with high accuracy. To our knowledge, this is the first fully automatic approach for extracting significant specifications from mining using program testing. We evaluate our approach through mining significant specifications for the Java API and use them to find real defects in many systems.

This paper examines the problem of structuring proofs in functional software verification from a novel perspective. By aligning the proofs with the operational behaviour of the program, we allow the formalization of the underlying concepts and their properties to reflect informal correctness arguments. By splitting the proof along the different aspects of the code, we achieve re-use of both theories and proof strategies across algorithms, thus enabling reasoning by analogy as employed in software construction. We demonstrate the viability and usefulness of the approach using a low-level C implementation of Cheney’s algorithm.

In this paper we propose a unifying approach for the static analysis of string values based on abstract interpretation, and we present several abstract domains that track different types of information. In this way, the analysis can be tuned at different levels of precision and efficiency, and it can address specific properties.

LePUS3 is a formal design description language for specifying decidable (i.e. automatically verifiable) properties of object-oriented design. LePUS3 has been successfully applied to both design verification and reverse engineering applications. However, LePUS3 is becoming over zealously pragmatic. Its current definition is inflexible, limiting is expressivity, extensibility and reasoning capabilities. We present a new theory of classes derived from the theoretical foundations of LePUS3, and defined in the Typed Predicate Logic. The expressive power of our theory is demonstrated by specifying and reasoning over design patterns.

Concurrent programs often use Labeled Transition Systems (LTSs) as their operational semantic models, which provide the basis for automatic system analysis and verification. System behaviors (generated from the operational semantics) evolve as programs evolve for fixing bugs or implementing new user requirements. Even when a program remains unchanged, its LTS models explored by a model checker or analyzer may be different due to the application of different exploration methods. In this paper, we introduce a novel approach (named SpecDiff) to computing the differences between two LTSs, representing the evolving behaviors of a concurrent program. SpecDiff considers LTSs as Typed Attributed Graphs (TAGs), in which states and transitions are encoded in finite dimensional vector spaces. It then computes a maximum common subgraph of two TAGs, which represents an optimal matching of states and transitions between two evolving LTSs of the concurrent program. SpecDiff has been implemented in our home grown model checker framework PAT. Our evaluation demonstrates that SpecDiff can assist in debugging system faults, understanding the impacts of state reduction techniques, and revealing system change patterns.

Consensus problems arise in any area of computing where distributed processes must come to a joint decision. Although solutions to consensus problems have similar aims, they vary according to the processor faults and network properties that must be taken into account, and modifying these assumptions will lead to different algorithms. Reasoning about consensus protocols is subtle, and correctness proofs are often informal. This paper gives a fully formal development and proof of a known consensus algorithm using the stepwise refinement method Event-B. This allows us to manage the complexity of the proof process by factoring the proof of correctness into a number of refinement steps, and to carry out the proof task concurrently with the development. During the development the processor faults and network properties on which the development steps rely are identified. The research outlined here is motivated by the observation that making different choices at these points may lead to alternative algorithms and proofs, leading to a refinement tree of algorithms with partially shared proofs.

State machines are hierarchical automata that are widely used to structure complex behavioural specifications. We develop two notions of refinement of state machines, node refinement and edge refinement. We compare the two notions by means of examples and argue that, by adopting simple conventions, they can be combined into one method of refinement. In the combined method, node refinement can be used to develop architectural aspects of a model and edge refinement to develop algorithmic aspects. The two notions of refinement are grounded in previous work. Event-B is used as the foundation for our refinement theory and UML-B state machine refinement influences the style of node refinement. Hence we propose a method with direct proof of state machine refinement avoiding the detour via Event-B that is needed by UML-B.

Verifying the functional correctness of a processor requires a sound and complete specification of its Instruction Set Architecture (ISA). Current industrial practice is to describe a processor’s ISA informally using natural language often with added semi-formal notation to capture the functional intent of the instructions. This leaves scope for errors and inconsistencies. In this paper we present a method to specify, design and construct sound and complete ISAs by stepwise refinement and formal proof using the formal method Event-B. We discuss how the automatically generated Proof Obligations help to ensure self-consistency of the formal ISA model, and how desirable properties of ISAs can be enforced within this modeling framework. We have developed a generic ISA modeling template in Event-B to facilitate reuse. The key value of reusing such a template is increased model integrity. Our method is now being used to formalize the ISA of the XMOS XCore processor with the aim to guarantee that the documentation of the XCore matches the silicon and the silicon matches the architectural intent.

Model-based testing (MBT) generates test cases by analysing a formal model of the system under test (SUT). In many MBT methods, these test cases are too abstract to be executed. Therefore, an executable representation of them is necessary to test the SUT. So far, the MBT community has focused on methods that automate the generation of test cases, but less has been done in making them executable. In this paper we propose a language to specify rules that can be automatically applied to produce an executable representation of test cases generated by the Test Template Framework (TTF), a MBT method for the Z notation.

We implement a large Isabelle/HOL repository of algebras for application in modelling computing systems. They subsume computational logics such as dynamic and Hoare logics and form a basis for various software development methods. Isabelle has recently been extended by automated theorem provers and SMT solvers. We use these integrated tools for automatically proving several rather intricate refinement and termination theorems. We also automate a modal correspondence result and soundness and relative completeness proofs of propositional Hoare logic. These results show, for the first time, that Isabelle’s tool integration makes automated algebraic reasoning particularly simple. This is a step towards increasing the automation of formal methods.

We devise a theoretical foundation of

directed rewriting

, a term rewriting strategy for logics of partial functions, inspired by term rewriting in the Rodin platform. We prove that directed rewriting is sound and show how to supply new rewrite rules in a soundness preserving fashion. In the context of Rodin, we show that directed rewriting makes a significant number of conditional rewrite rules unconditional. Our work not only allows us to point out a number of concrete ways of improving directed rewriting in Rodin, but also has applications in other logics of partial functions. Additionally, we give a semantics for the logic of Event-B.

Distributed Real-Time Systems (DRTS), such as avionics systems and distributed control systems in motor vehicles, are very hard to design because of asynchronous communication, network delays, and clock skews. Furthermore, their model checking problem typically becomes unfeasible due to the large state spaces caused by the interleavings. For many DRTSs, we can use the PALS methodology to reduce the problem of designing and verifying asynchronous DRTSs to the much simpler task of designing and verifying their synchronous versions. AADL is an industrial modeling standard for avionics and automotive systems. We define in this paper the

Synchronous AADL

language for modeling synchronous real-time systems in AADL, and provide a formal semantics for Synchronous AADL in Real-Time Maude. We have integrated into the OSATE modeling environment for AADL a plug-in which allows us to model check Synchronous AADL models in Real-Time Maude within OSATE. We exemplify such verification on an avionics system, whose Synchronous AADL design can be model checked in less than 10 seconds, but whose asynchronous design cannot be feasibly model checked.