Steve Reeves
@waikato.ac.nz
Professor, Software Engineering, School of Computing and mathematical Sciences
University of Waikato
RESEARCH INTERESTS
Formal methods
Software Engineering
Programming Languages
Blockchain
Scopus Publications
Scopus Publications
Daniel Britten and Steve Reeves
ACM
To create trustworthy programs, the 'gold standard' is specifications at a high-enough level to clearly correspond to the informal specifications, and also a refinement proof linking these high-level specifications down to, in our case, executable bytecode. The DeepSEA system demonstrates how this can be done, in the context of smart contracts on the Ethereum blockchain. A key component of this is the model of the blockchain on which the smart contracts reside. When doing proofs in DeepSEA, it is critical to have such a model, which allows for the writing of specifications at a high-level clearly corresponding to informal specifications. A candidate model for doing so and its usefulness for carrying out proofs is discussed in this paper.
Jessica Turner, Judy Bowen, and Steve Reeves
ACM
In this paper we describe SeqCheck, a model checking tool which allows us to investigate if certain properties hold for an interactive system. These properties allow us to determine if the interaction sequence model of an interactive system's overlap component behaves as expected. We describe the properties we have defined for this overlap component and then demonstrate the use of SeqCheck to identify when these do not hold.
Jessica Turner, Judy Bowen, and Steve Reeves
Association for Computing Machinery (ACM)
Testing is an important part of the software engineering process to help ensure that systems will behave as expected. In this paper we investigate interactive system testing, taking into consideration the different components of the system. Interactive systems have three different components, the interactive, functional and overlap. The interactive component is the interface of the interactive system, the functional the underlying instructions of the interactive system, and the overlap component the point at which the interactive and functional components intersect. The interactive and functional components are often tested separately, however, problems can occur where these components overlap. Therefore, in this paper we present a model-based testing approach specifically designed to inspect the overlap component behaviour and to ensure that it behaves as expected.
Sapna Jaidka, Steve Reeves, and Judy Bowen
Springer International Publishing
Formal modelling is now widely applied for creating models of safety-critical interactive systems. Most approaches built so far either focus on the user interface or on the functional part of a safety-critical interactive system. This paper aims to apply formal methods for modelling and specifying the user interface, interaction and functional aspects of a safety-critical system in a single model using Coloured Petri Nets (CPN). We have used CPNs because of its expressive graphic representation and the ability to simulate the system behaviour. The technique is illustrated through a case study of the Niki T34 Infusion Pump.
Sapna Jaidka, Steve Reeves, and Judy Bowen
IEEE
To gain confidence in safety-critical interactive systems, formal modelling and analysis plays a vital role. The aim of this paper is to use Coloured Petri Nets to model and analyze safety-critical interactive systems. We present a technique to construct a single Coloured Petri Net model of the user interface, interaction and functionality of safety-critical interactive systems and then analyze the achieved Coloured Petri Net model using a state space analysis method. There are several reasons for using Coloured Petri Nets. Coloured Petri Nets provides a graphical representation and hierarchical structuring mechanism, and a state space verification technique, which allows querying the state space to investigate behaviours of a system. There are several tools that supports Coloured Petri Nets including the CPN Tool which helps in building CPN models and allows simulation and analysis using state spaces. The technique to model and analyze safety-critical interactive systems is illustrated using a simplified infusion pump example.
Felipe Bravo-Marquez, Steve Reeves, and Martin Ugarte
IEEE
This article presents WekaCoin, a peer-to-peer cryptocurrency based on a new distributed consensus protocol called Proof-of-Learning. Proof-of-learning achieves distributed consensus by ranking machine learning systems for a given task. The aim of this protocol is to alleviate the computational waste involved in hashing-based puzzles and to create a public distributed and verifiable database of state-of-the-art machine learning models and experiments.
Judy Bowen and Steve Reeves
IEEE
The use of sound and robust software engineering techniques are essential during the design and development of safety-critical interactive systems. Failure of such systems (such as those found in medical settings or transportation) can lead to serious harm or even fatalities. Model-based development of interactive systems provides a number of benefits which can support correctness of the interface, the interaction and the functional logic of the system. Many different approaches have been proposed which target the models at different aspects of the development process (for example task analysis, interface layouts, functional behaviours etc.) and which can be used in different ways (verification of correctness, usability, testing). Typically these rely on multiple models at differing levels of abstraction. There are challenges in ensuring consistency between the models, and more importantly in ensuring that the final implementation correctly satisfies all of the models. In this paper we propose a method of deriving pre-and post-conditions for both interactive and functional elements of the system from formal models. These are used to generate code contracts within a code framework to support programmers who are implementing the system described in such models. We describe both the process for this and present an initial examination of the applicability of the approach based on a proof-of-concept user study. This small study was intended to examine whether we could correctly derive the code contracts in an automated fashion and whether or not they were usable (and beneficial) for programmers working on a pre-defined task. This initial investigation suggested that such an approach can aid programmers in correctly implementing a specification and that the general approach outlined in the paper is worth developing further.
Nathaniel Watson, Steve Reeves, and Paolo Masci
Open Publishing Association
Creating formal models of interactive systems has wide reaching benefits, not only for verifying low-level correctness, but also as a tool for ensuring user interfaces behave logically and consistently. Despite this, tools for designing user experiences and tools for creating and working with formal models are typically distinctly separate systems. This work aims to bridge this divide by allowing the generation of state machine diagrams and formal models via a simple, interactive prototyping tool that mirrors the basic functionality of many modern digital prototyping applications.
J. Derrick, Brijesh Dongol and S. Reeves
Open Publishing Association
Refinement is one of the cornerstones of a formal approach to software engineering. Refinement is the process of developing a more detailed design or implementation from an abstract specification through a sequence of mathematically-based steps that maintain correctness with respect to the original specification. Work on the foundations of languages such as Z, B, VDM and CSP have led to their widespread use in certain industrial sectors, e.g., those with security or safety critical concerns. In addition to precise specification, formal methods also allow the possibility of precise and verifiable development, as captured by the concept of refinement.
The 18th Refinement Workshop was held as part of FLoC 2018 at Oxford, UK.
Jessica Turner, Judy Bowen, and Steve Reeves
ACM
Modelling interactive systems is an important part of a sound software engineering process. In order to support this and reduce the amount of time it takes to create and update the models we typically need tools to support this process. Interaction sequences are a particular type of model used for interactive systems which allow us to reason about their behaviour when a user interacts with the system. In this paper we describe the 'Sequence Simulator' tool which allows us to build, modify, and manipulate interaction sequence models. The tool also supports model abstraction using the 'self-containment' property and we show how this automatically abstracts and expands the state space of the models as required.
Colin Pilbrow and Steve Reeves
IEEE
For validation or for communication with a client, it is useful to create a visualisation of a specification. It is important that the visualisation does not mislead the user. In this work we look at how to characterise the conditions for a micro-chart visualisation to be sound. This is done by introducing a new operator to the micro-chart semantics, allowing us to use Z data refinement to find a refinement relation between a Z specification and its (claimed sound) micro-chart visualisation. If the relation does not hold, then the visualisation is not sound.
Colin Pilbrow and Steve Reeves
IEEE
For validation or for communication with a client, it is useful to create a visualisation of a specification. It is important that the visualisation does not mislead the user. In this work we look at how to characterise the conditions for a micro-chart visualisation to be sound. This is done by introducing a new operator to the micro-chart semantics, allowing us to use Z data refinement to find a refinement relation between a Z specification and its (claimed sound) micro-chart visualisation. If the relation does not hold, then the visualisation is not sound.
Jessica Turner, Judy Bowen, and Steve Reeves
Springer International Publishing
Interaction sequences can be used as an abstraction of an interactive system. We can use such models to consider or verify properties of a system for testing purposes. However, interaction sequences have the potential to become unfeasibly long, leading to models which are intractable. We propose a method of reducing the state space of such sequences using the self-containment property. This allows us to hide (and subsequently expand) some of the model describing parts of the system not currently under consideration. Interaction sequences and their models can therefore be used to control the state space size of the models we create as an abstraction of an interactive system.
Jessica Turner, Judy Bowen, and Steve Reeves
ACM
In software engineering testing is an important part of the development process. In interactive systems human input introduces the possibility of human error, which increases the testing requirements. In safety-critical systems user or system error can result in injury or death to a user. We propose using interaction sequences as a way of supporting interactive system testing to help address these issues.
Sapna Jaidka, Steve Reeves, and Judy Bowen
ACM
The paper describes a model that presents a technique in which we combine formal languages---Z, presentation models and coloured Petri nets---and methods which use them, to specify the functionality and model the user interface and interaction of a system by clearly describing the state space, operations and behavioural aspects of a system. We show how to combine the Z specification and presentation models with coloured Petri nets for modelling safety critical systems by retaining the strengths of the formalisms and alleviating their drawbacks.
Judy Bowen and Steve Reeves
Association for Computing Machinery (ACM)
Model-based development of interactive systems provides a number of benefits which can support the creation of robust and correct systems, particularly important when the interactive systems are safety-critical. Many different approaches have been proposed which target the models at different aspects of the development process (for example task analysis, interface layouts, functional behaviours etc.) and which can be used in different ways (verification of correctness, plasticity, usability). One of the aims for any modelling method should be simplicity - we are after all trying to hide complexity via abstraction in order to make reasoning about systems more tractable than working at the programming level. One of the challenges that exists however we do our modelling is ensuring the consistency between the model of the interface and interactivity and model of the functional behaviour of the system. This is primarily due to the different types of models that most naturally describe these different elements. In this paper we propose a method of tightening the integration of models of these different components of the system by generating obligations which explicitly describe the coupling of functional behaviour with interactive elements. We then show how these obligations can be used to support the development process during the programming and testing of the system.
J. Derrick, E. Boiten and S. Reeves
Open Publishing Association
We are proud to present the papers from the 17th Refinement Workshop, co-located with FM 2015 held in Oslo, Norway on June 22nd, 2015.
Refinement is one of the cornerstones of a formal approach to software engineering: the process of developing a more detailed design or implementation from an abstract specification through a sequence of mathematically-based steps that maintain correctness with respect to the original specification.
This 17th workshop continued a 20+ year tradition under the auspices of the British Computer Society (BCS) FACS special interest group.
This is the third volume that has appeared as an EPTCS proceedings, and we would like to thank the editorial board (and in particular Rob van Glabbeek) for their help and cooperation in making this happen.
The organisers would like to thank everyone: the authors, BCS-FACS, EPTCS, and the organisers of FM 2015 for their help in organising this workshop, the participants of the workshop, and the reviewers involved in selecting the papers.
Paul Rimba, Liming Zhu, Len Bass, Ihor Kuz, and Steve Reeves
IEEE
Building secure applications requires significant expertise. Secure platforms and security patterns have been proposed to alleviate this problem. However, correctly applying patterns to use platform features is still highly expertise-dependent. Patterns are informal and there is a gap between them and platform features. We propose the concept of reusable verified design fragments, which package security patterns and platform features and are verified to provide assurance about their security properties. Design fragments can be composed through four primitive tactics. The verification of the composed design against desired security properties is presented in an assurance case. We demonstrate our approach by securing a Continuous Deployment pipeline and show that the tactics are sufficient to compose design fragments into a secure system. Finally, we formally define composition tactics, which are intended to support the development of systems that are secure by construction.
Colin Pilbrow and Steve Reeves
ACM
We talk in this paper about using state machines and refinement to characterise the visualisation of a computation. We use Z specifications to give examples of systems in the usual way, and then use Z schemas to also represent states and transitions in state machines, which we consider to be a particular kind of visualisation of a specified system. We have investigated the principle of substitutivity and the idea of downward simulation to check whether or not a refinement relation exists between the specification and the state machine. We are looking at this because we believe that the soundness of the visualisation can be captured by such a refinement relationship.
Judy Bowen and Steve Reeves
IEEE
Building models of safety-critical interactive systems (in healthcare, transport, avionics and finance, to name but a few) as part of the design process is essential. It is also advised for non-safety critical interactive systems if we want to be certain they will behave as intended in all circumstances. However, modelling interactive systems is also challenging. The levels of complexity in modern user interfaces and the wealth of interaction possibilities means that modelling at a suitable level of abstraction is crucial to ensure our models remain reasonably sized, readable, and therefore usable. The decisions we make about how to abstract the system to retain enough detail to be able to reason about it without running into known modelling problems (state-explosion, verbosity, unread ability) are complex, even for experienced modellers. We have identified a number of commonly seen problems in such models based on occurrences of common properties of interactive systems, and in order to help both experienced and novice modellers we propose model-patterns as a solution to this.
Elvinia Riccobene and Steve Reeves
Elsevier BV
Judy Bowen and Steve Reeves
Springer International Publishing
Creating formal models of interactive systems requires that we understand not just the functionality of the system, but also the interface and interaction possibilities. The benefits of fully modelling these systems is that we can ensure behavioural properties of all aspects of the system are correct and prove properties of correctness of the whole system. In the case of safety-critical interactive systems this is important as errors of interactive behaviours can be just as devastating as functional errors. In previous works we have developed models which enable us to perform these tasks - notably presentation models and presentation interaction models PIMs and have shown that by using the μCharts language to describe PIMs we can use its underlying Z semantics to produce specifications of both functionality and interface/interaction. In this paper we revisit the Z semantics of PIMs and propose an alternative and simpler semantics along with explanations of why this is more useful and appropriate for particular modelling situations.