Formal methods for software correctness are critical to the future of software engineering—and so must be an essential part of software engineering education. Unfortunately, formal methods are often resisted by students due to perceived difficulty, mathematicity, and practical irrelevance. We redeveloped our software correctness course by taking a programming intensive approach, using the solver-aided language Dafny to provide instant formative feedback via automated assessment. Our redeveloped course increased student retention and resulted in the best evaluation for the course for at least ten years.

Currently the SDN research community considers in-line dynamic network functions too complex for SDN, leading to calls to purge them from the forwarding plane. This paper introduces a comprehensive framework that tames this complexity and allows network administrators to deploy complex network functions into the SDN forwarding plane to provide enhanced and provable network properties. We first illustrate mapping complex network functions to a network to determine location and their sphere of influence. Through analysis we identify properties common to all network functions and we provide formalisms to specify the behaviour of a generic network function using typed functions, the basis of many modern programming languages. We extend this generic network function to demonstrate two types of firewall providing security properties and also demonstrate chaining which is the basis of Unified Threat Management firewalls and Deep Packet Inspection. This paper is a foundation for ongoing research into proving properties of black box implementations of network functions.

It appears to be SDN dogma that middleboxes are bad. However middleboxes form near half the elements that comprise today's networks and at least three active research fields are exploring how to improve their functionality. Fifteen recent SDN survey papers were examined for evidence to support the SDN dogma and its assertion that all network functionality belongs in the control plane, without success. In fact many chose to ignore the subject. Consequently this paper critically examines what is almost an SDN article of faith and finds this dogma creates a number of interesting and avoidable problems. Three common middlebox types are examined: firewall, NAT and load balancer to highlight the preferred SDN architecture and generate critical thinking. Finally the concept of global and local knowledge is used in a framework to determine whether an application should reside in the control plane or data plane.

Usually, test automation scripts for a web application directly mirror the actions that the tester carries out in the browser, but they tend to be verbose and repetitive, making them expensive to maintain and ineffective in an agile setting. Our research has focussed on providing tool-support for business-level, example-based specifications that are mapped to the browser level for automatic verification. We provide refactoring support for the evolution of existing browser-level tests into business-level specifications. As resulting business rule tables may be incomplete, redundant or contradictory, our tool provides feedback on coverage.

In this paper we have been influenced by those who take an "engineering view" of the problem of designing systems, i.e. a view that is motivated by what someone designing a real system will be concerned with, and what questions will arise as they work on their design. Specifically, we have borrowed from the testing work of Hennessy, de Nicola and van Glabbeek, e.g. Hennessy, 1988 [13], de Nicola [5], de Nicola, 1992 [21] and van Glabbeek, 2001, 1990 [40,39].Here we concentrate on one fundamental part of the engineering view and where consideration of it leads. The aspects we are concerned with are computational entities in contexts, observed by users. This leads to formalising design steps that are often left informal, and that in turn gives insights into non-determinism and ultimately leads to being able to use refinement in situations where existing techniques fail. (C) 2010 Elsevier B.V. All rights reserved.

Before we combine actions and probabilities two very obvious questions should be asked. Firstly, what does "the probability of an action" mean? Secondly, how does probability interact with nondeterminism? Neither question has a single universally agreed upon answer but by considering these questions at the outset we build a novel and hopefully intuitive probabilistic event-based formalism.In previous work we have characterised refinement via the notion of testing. Basically, if one system passes all the tests that another system passes (and maybe more) we say the first system is a refinement of the second. This is, in our view, an important way of characterising refinement, via the question "what sort of refinement should I be using?"We use testing in this paper as the basis for our refinement. We develop tests for probabilistic systems by analogy with the tests developed for non-probabilistic systems. We make sure that our probabilistic tests, when performed on non-probabilistic automata, give us refinement relations which agree with for those non-probabilistic automata. We formalise this property as a vertical refinement.

Mobile services depend on user context and preferences, and a mobile user's context is constantly changing. Many services are only available locally. The most appropriate service for a user's context is not known in advance and a user may enter or leave a service's range at any time. For a seamless user experience, services need to collaborate. These complex collaborations should be instantaneous yet anonymous - without disclosing user information. The paper proposes a new service collaboration model using event-based interaction. A prototypical implementation is used to demonstrate functionality, inter-operability, and generality of our solution. The solution guarantees ad-hoc service collaboration while protecting user information.

In this paper we explore how formal models are interpreted and to what degree meaning is captured in the formal semantics and to what degree it remains in the informal interpretation of the semantics. By applying a robust approach to the definition of refinement and semantics, favoured by the event-based community, to state-based theory we are able to move some aspects from the informal interpretation into the formal semantics.

Simulation rules have long been used as an effective computational means to decide refinement relations in state-based formalisms. Here we investigate how they might be amended so as to decide the event-based notion of singleton failures refinement of abstract data types, or processes, that have operations with a ''guarded'' interpretation.

In this paper, we give simple example abstract data types, with atomic operations, that are related by data refinement under a definition used widely in the literature, but these same abstract data types are not related by singleton failure refinement. This contradicts results found in the literature.

In the previous, companion, paper [Reeves, S. and D. Streader, General refinement, part one: interfaces, determinism and special refinement, Proceedings of Refine 2008, Electronic Notes in Theoretical Computer Science (2008).] to this paper we introduced our general model of refinement, discussed ideas around determinism and interfaces that the general definition raised, and gave several examples showing how the general definition could be specialised to the sorts of refinement we see in the literature. In this paper we continue the story and we define vertical refinement on our general model. Vertical refinement can be seen as a generalisation of what, in the literature, has been called action refinement or non-atomic refinement. Alternatively, by viewing a special model (from the previous paper) as a logical theory, vertical refinement can be seen as a theory morphism, formalised as a Galois connection. We give an example of the utility of this definition by constructing a vertical refinement between broadcast processes and interactive branching programs, and we see how interactive branching programs can be implemented on a platform which provides broadcast communication. We also show how developments that fall outside the usual, special theories of refinement can be brought into the refinement world by giving examples of development which were thought not to be possible using refinement. Throughout, the central, simple idea of refinement as a development process that moves from abstract to concrete while preserving certain valuable guarantees will guide us.

Tools have become essential in the formal model-driven development of software but are very time consuming to build and often restricted to a particular semantic interpretation of a particular syntax. This is regrettable since there is large amount in common between tools, even if they do ''implement'' different syntaxes and different semantics. We propose splitting tools into front- and back-ends where an operational semantics acts as the link between the two. We will not have much to say about the front-end and the link in this paper since it is theoretically straightforward. Instead, we concentrate on the second part and provide a well-motivated, general, mathematical framework to form the underlying theory that gives great flexibility to the back-end of a tool which is concerned with developing software via stepwise refinement. From a general model of refinement between two entities, where the refinement is parameterised on contexts and observations, we build logical theories which have refinement as implication. Further, we consider what can be expected of a guarantee concerning the behaviour of an implementation relative to a specification. Then by fixing the contexts and observations in suitable ways, and so getting particular, special models of refinement, we give a formal interpretation of a guarantee. To this we add theory morphisms between special models, where a theory morphism can change the contexts and observations we can make in controlled and useful ways, mainly by preserving a refinement relation between entities even as we change them. We show how the generality brought about by the parameterisation allows an example from the literature, which seems formally not to be a refinement, to be captured as a refinement, in accordance with our intuitions about the example. In this way we show the flexibility of our theory for a refinement tool back-end. From this it follows that the effort put into building a tool based on our theory will be well-spent-a single tool should be parameterised (just as our theory is) to deal with the many different notions of refinement found in the literature. Thus we make a contribution to the problem of ensuring correctness and dependability of software using formal methods and tools of modelling, design, verification and validation.

We introduce a general model of refinement. This is defined in terms of what contexts an entity can appear in, and what observations can be made of it in those contexts. We show explicitly how five refinement relations, taken from the refinement literature, are instances of our general model. Henceforth, since they are specialisations of a general model, we call these instances special models. We show these theories of refinement are special models simply by fixing the sets of contexts and observations involved in appropriate ways.

web applications have a tendency to get bigger. Yet despite the current popularity of web applications, little has been done to help programmers to leverage the performance and scalability benefits that can result from the introduc- tion of parallelism into a program. Accordingly, we present a technique for the automatic parallelisation of whole web applications, including persistent data storage mechanisms. We detail our prototype implementation of this technique, Ceth and finally, we establish the soundness of the process by which we extract coarse-grained parallelism from programs.

This paper presents supervisory control theory in a process-algebraic setting, and proposes a way of synthesising modular supervisors that guarantee nonblocking. The framework used includes the possibility of hiding actions which results in nondeterminism. As modularity crucially depends on the process equivalence used, the paper studies possible equivalences and points out that, in order to be consistent with respect to the nonblocking property and to supervisor synthesis, a conflict-preserving equivalence must be used. It applies the results to synthesise nonblocking modular supervisors for a manufacturing system.

Development by formal stepwise refinement offers a guarantee that an implementation satisfies a specification. But refinement is frequently defined in such a restrictive way as to disallow some useful development steps. Here we define feature refinement to overcome some limitations of refinement and show its usefulness by applying it to examples taken from the literature. Using partial relations as a canonical state-based semantics and labelled transition systems as a canonical event-based semantics, we define functions formally linking the state- and event-based operational semantics. We can then use this link to move notions of refinement between the event- and state-based worlds. An advantage of this abstract approach is that it is not restricted to a specific syntax or even a specific interpretation of the operational semantics.

We define two lifted, total relation semantics for Event B machines: Safe B for safety-only properties and Live B for liveness properties. The usual Event B proof obligations, Safe, are sufficient to establish Safe B refinement. Satisfying Safe plus a simple additional proof obligation ACT REF is sufficient to establish Live B refinement. The use of lifted, total relations both prevents the ambiguity of the unlifted relational semantics and prevents operations being clairvoyant.

In this paper we give simple example abstract data types, with atomic opera- tions, that are related by data renement under a denition used widely in the liter- ature, but these abstract data types are not related by singleton failure renement. This contradicts results found in the literature. Further we show that a common way to change a model of atomic operations to one of value passing operations actually changes the underlying atomic operational semantics.