Browsing by Author "Reeves, Steve"

Pilbrow, Colin; Reeves, Steve
(ACM, 2015)
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 ...

Bowen, Judy; Reeves, Steve
(IEEE, 2015)
Building models of safetycritical 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 nonsafety critical interactive ...

Rimba, Paul; Zhu, Liming; Bass, Len; Kuz, Ihor; Reeves, Steve
(IEEE, 2015)
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 ...

Bowen, Judy; Cunningham, Sally Jo; Hinze, Annika; Jung, Doris; Reeves, Steve
(Department of Computer Science, The University of Waikato, 2014)
This position paper outlines our approach to improve the usage choice of suitable devices in different health care environments (contexts). Safetycritical medical devices are presumed to have undergone a thorough ...

Reeves, Steve; Bowen, Judy
(ACM, 2013)
The workshop focuses on use of formal methods in the development and analysis of Interactive Systems. The workshop is particularly concerned with issues relating to Human Computer Interaction and to the analysis of interaction ...

Bowen, Judy; Reeves, Steve; Schweer, Andrea
(2013)
Running user evaluation studies is a useful way of getting feedback on partially or fully implemented software systems. Unlike hypothesisbased testing (where specific design decisions can be tested or comparisons made ...

Reeves, Steve; Bowen, Judy
(ACM, 2013)
Formally modelling the software functionality and interactivity of safetycritical devices allows us to prove properties about their behaviours and be certain that they will respond to user interaction correctly. In domains ...

Reeves, Steve; Streader, David
(2011)
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 ...

Bowen, Judy; Reeves, Steve
(ACM, 2011)
Testdriven development (TDD) is a software development approach, which has grown out of the Extreme Programming and Agile movements, whereby tests are written prior to the implementation code which is then developed and ...

Bowen, Jonathan P.; Reeves, Steve
(Springer, Berlin, 2011)
A Body of Knowledge (BoK) is an ontology for a particular professional domain. A Community of Practice (CoP) is the collection of people developing such knowledge. In the paper we explore these concepts in the context of ...

Bowen, Judy; Reeves, Steve
(ACM, 2010)
Developing usability studies to evaluate software is a task requiring a wide variety of skills. For software developers who are not used to taking a usercentred approach to development it is often easier and more convenient ...

Reeves, Steve; Streader, David
(2010)
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 ...

Reeves, Steve; Streader, David
(University of Waikato, Department of Computer Science, 2009)
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 ...

Reeves, Steve; Streader, David
(University of Waikato, Department of Computer Science, 2009)
Simulation rules have long been used as an effective computational means to decide refinement relations in statebased formalisms. Here we investigate how they might be amended so as to decide the eventbased notion of ...

Bowen, Judy; Reeves, Steve
(2009)
Testing interactive systems is notoriously difficult. Not only do we need to ensure that the functionality of the developed system is correct with respect to the requirements and specifications, we also need to ensure that ...

Bowen, Judy; Reeves, Steve
(Springer, 2009)
Formal approaches to software development require that we correctly describe (or specify) systems in order to prove properties about our proposed solution prior to building it. We must then follow a rigorous process to ...

Bowen, Judy; Reeves, Steve
(IEEE, 2009)
As computers and software applications become ubiquitous the systems we build are increasingly required to run on not just a single piece of hardware, but rather be available for different platforms, different types of ...

Reeves, Steve; Streader, David
(2009)
Simulation rules have long been used as an effective computational means to decide refinement relations in statebased formalisms. Here we investigate how they might be amended so as to decide the eventbased notion of ...

Reeves, Steve; Streader, David
(Springer, 2009)
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 ...

Reeves, Steve
(University of Waikato, Department of Computer Science, 2008)
Adding considerations about reachability to the Logics of Specification Languages [1] chapter [2].

Reeves, Steve; Streader, David
(2008)
Tools have become essential in the formal modeldriven 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 ...

Reeves, Steve; Streader, David
(Springer, 2008)
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 ...

Bowen, Judy; Reeves, Steve
(Springer, 2008)
There are many different ways of building software applications and of tackling the problems of understanding the system to be built, designing that system and finally implementing the design. One approach is to use formal ...

Malik, Petra; Malik, Robi; Streader, David; Reeves, Steve
(2007)
This paper presents supervisory control theory in a processalgebraic setting, and proposes a way of synthesising modular supervisors that guarantee nonblocking. The framework used includes the possibility of hiding actions ...

Reeves, Steve; Streader, David
(2007)
To help make refinement more usable in practice we introduce a general, flexible 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 ...

Bowen, Judy; Reeves, Steve
(British Computer Society, 2007)
The use of formal models for user interface design can provide a number of benefits. It can help to ensure consistency across designs for multiple platforms, prove properties such as reachability and completeness and, ...

Reeves, Steve; Streader, David
(IEEE Computer Society, 2007)
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. ...

Reeves, Steve; Streader, David
(2006)
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 abstract data types are not related by ...

Reeves, Steve; Streader, David
(2006)
We define two lifted, total relation semantics for Event B machines: Safe B for safetyonly properties and Live B for liveness properties. The usual Event B proof obligations, Safe, are sufficient to establish Safe B ...

Reeves, Steve; Streader, David
(2006)
We transfer a process algebraic notion of refinement to the B method by using the wellknown bridge between the relational semantics underlying the B machines and the labelled transition system semantics of processes. Thus ...

Reeves, Steve; Streader, David
(2005)
We define interacting sequential programs, motivated originally by constructivist considerations. We use them to investigate notions of implementation and determinism. Process algebras do not define what can be implemented ...

Reeves, Steve; Streader, David
(2005)
Industry is looking to create a market in reliable "plugandplay" components. To model components in a modular style it would be useful to combine eventbased and statebased
reasoning. One of the first steps in building ...

Bowen, Judy; Reeves, Steve
(Springer, Berlin, 2005)
For any sort of computer system, the problems of being sure you have asked for the right thing and then being sure you are implementing the right thing are important and hard problems. For systems with a graphical user ...

Reeve, Greg; Reeves, Steve
(University of Waikato, Department of Computer Science, 2004)
μCharts is a language for specifying the behaviour of reactive systems. The language is a simplified variant of the wellknown language Statecharts that was introduced by Harel. Development of the μCharts language is ...

Reeves, Steve; Streader, David
(University of Waikato, Department of Computer Science, 2004)
If a coin is given to a deterministic robot that interacts with a deterministic vending machine then is the drink that the robot is delivered determined? Using process definitions of determinism from CSP, CCS or ACP the ...

Reeves, Steve; Streader, David
(University of Waikato, Department of Computer Science, 2004)
There has been much interest in components that combine the best of statebased and eventbased approaches. The interface of a component can be thought of as its specification and substituting components with the same ...

Malik, Robi; Streader, David; Reeves, Steve
(Springer, Berlin, 2004)
This paper studies conflicts from a processalgebraic point of view and shows how they are related to the testing theory of fair testing. Conflicts have been introduced in the context of discrete event systems, where two ...

Henson, Martin C.; Reeves, Steve
(2003)
We show how a theory of specification refinement and program development can be constructed as a conservative extension of our existing logic for Z. The resulting system can be set up as a development method for a Zlike ...

Henson, Martin C.; Reeves, Steve; Bowen, Jonathan P.
(Institute of Informatics, 2003)
This paper provides an introduction to the specification language Z from a logical perspective. The possibility of presenting Z in this way is a consequence of a number of joint publications on Z logic that Henson and ...

Reeves, Steve; Streader, David
(University of Waikato, Department of Computer Science, 2003)
When is it reasonable, or possible, to refine a one place buffer into a two place buffer? In order to answer this question we characterise refinement based on substitution in restricted contexts. We see that data refinement ...

Reeves, Steve; Streader, David
(2003)
Statebased and processbased formalisms each come with their own distinct set of assumptions and properties. To combine them in a useful way it is important to be sure of these assumptions in order that the formalisms are ...

Deutsch, Moshe; Henson, Martin C.; Reeves, Steve
(Springer, Berlin, 2003)
The schema calculus of Z provides a means for expressing structured, modular specifications. Extending this modularity to program development requires the monotonicity of these operators with respect to refinement. This ...

Deutsch, Moshe; Henson, Martin C.; Reeves, Steve
(Oxford University Press, 2003)
This is the first of a series of papers devoted to the thorough investigation of (total correctness) refinement based on an underlying partial relational model. In this paper we restrict attention to operation refinement. ...

Henson, Martin C.; Reeves, Steve
(Oxford University Press, 2003)
In this paper we introduce and investigate an improved kernel logic Zc for the specification language Z. Unlike standard accounts, this logic is consistent and is easily shown to be sound. We show how a complete shema ...

Deutsch, Moshe; Henson, Martin C.; Reeves, Steve
(2002)
Stepwise design involves the process of deriving a concrete model of a software system from a given abstract one. This process is sometimes known as refinement. There are numerous refinement theories proposed in the ...

Goldson, Doug; Reeve, Greg; Reeves, Steve
(Springer, Berlin, 2002)
We introduce two new notions of refinement for μcharts and compare them with the existing notion due to Scholz. The two notions are interesting and important because one gives rise (via a logic) to a calculus for constructing ...

Anderson, Grant; Reeve, Greg; Reeves, Steve
(2001)
This paper presents an idiomatic construct for µcharts which reflects the highlevel specification construct of synchronization between activities. This, amongst others, has emerged as a common and useful idea during our ...

Reeve, Greg; Reeves, Steve
(University of Waikato, Department of Computer Science, 2001)
In this paper we describe our experience of using three different animation systems. We searched for and decided to use these tools in the context of a project which involved developing formal versions (in Z) of informal ...

Utting, Mark; Reeves, Steve
(John Wiley & Sons, Ltd., 2001)
A new style of formal methods course is described, based on a pragmatic approach that emphasizes testing. The course introduces students to formal specification using Z, and shows how formal specification and testing can ...

Reeve, Greg; Reeves, Steve
(2000)
μCharts are a way of specifying reactive systems, i.e. systems which are in some environment to which they have to react, based on the wellestablished formalism Statecharts. This paper gives (very abbreviated) examples ...

Reeve, Greg; Reeves, Steve
(University of Waikato, Department of Computer Science, 2000)
This paper describes extensions and modifications to the µcharts as given in earlier papers of Philipps and Scholz. The charts are extended to include a command language, integervalued signals and local integer variables. ...

Groves, Lindsay; Nickson, Ray; Reeve, Greg; Reeves, Steve; Utting, Mark
(2000)
We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a general questionnaire ...

Reeve, Greg; Reeves, Steve
(University of Waikato, Department of Computer Science, 2000)
In this paper we show, by a series of examples, how the µchart formalism can be translated into Z. We give reasons for why this is an interesting and sensible thing to do and what it might be used for.

Henson, Martin C.; Reeves, Steve
(Springer, Berlin, 2000)
We introduce a framework for program development and specification refinement in the schema calculus of Z. We provide illustrative examples outlining the major design decisions based on an interpretation of operation schemas ...

Henson, Martin C.; Reeves, Steve
(1999)
This is the second of two related papers. In "Revising Z: Part I  logic and semantics" (this journal) we introduced a simple specification logic ZC comprising a logic and a semantics (in ZF set theory). We then provided ...

Henson, Martin C.; Reeves, Steve
(1999)
This is the first of two related papers. We introduce a simple specification logic ZC comprising a logic and a semantics (in ZF set theory) within which the logic is sound. We then provide an interpretation for (a rational ...

Groves, Lindsay; Nickson, Ray; Reeve, Greg; Reeves, Steve; Utting, Mark
(1999)
We report on the software development techniques used in the New Zealand software industry, paying particular attention to requirements gathering. We surveyed a selection of software companies with a general questionnaire ...

Bridges, Douglas; Reeves, Steve
(Oxford University Press, 1999)
The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop’s constructive mathematics(BISH). It gives a sketch of both Myhill’s axiomatic system for BISH and a constructive ...

Henson, Martin C.; Reeves, Steve
(University of Waikato, Department of Computer Science, 1998)
We introduce a simple specification logic Zc comprising a logic and semantics (in ZF set theory). We then provide an interpretation for (a rational reconstruction of) the specification language Z within Zc. As a result we ...

Henson, Martin C.; Reeves, Steve
(University of Waikato, Department of Computer Science, 1998)
In this paper we introduce and investigate a logic for the schema calculus of Z. The schema calculus is arguably the reason for Z’s popularity but so far no true calculus (a sound system of rules for reasoning about schema ...

Henson, Martin C.; Reeves, Steve
(University of Waikato, Department of Computer Science, 1998)
We provide a constructive and intensional interpretation for the specification language Z in a theory of operations and kinds T. The motivation is to facilitate the development of an integrated approach to program construction. ...

Reeves, Steve
(1998)
The aim of this paper is to illustrate how formal specifications for collaborative interactive systems might be written. It presents a new modelling paradigm for certain systems. It also shows how formal software engineering ...

Blackett, Colin; Reeves, Steve
(1996)
This report has been produced as one of the outputs of the FORST funded project "Improved Computer Supported Collaborative Work Systems" which is currently running in the Department of Computer Science at the University ...

Apperley, Mark; Gianoutsos, Simon; Grundy, John C.; Paynter, Gordon W.; Reeves, Steve; Venable, John R.
(1996)
Computer Supported Cooperative Work (CSCW) systems are complex, yet no computerbased tools of any sophistication exist to support their development. Since several people often need to work together on the same project ...

Reeves, Steve
(1996)
In this paper we propose the design of a tool that will allow the construction of a formal, textual description of a software system even if it has a graphical userinterface as a component. An important aspect of this ...

Reeves, Steve
(University of Waikato, Department of Computer Science, 1995)
In this paper we describe the current progress of an attempt to develop a logic which will allow us to specify required properties of systems which typically consist of a single interactive program being used, probably ...

Reeves, Steve; Grundy, John C.
(University of Waikato, Department of Computer Science, 1995)
One of the main hurdles to the general adoption of formal program development techniques is a lack of tools to support their use in combination with more traditional development techniques. This paper describes an integrated ...

Reeves, Steve
(University of Waikato, Department of Computer Science, 1995)
In this paper we propose the design of a tool that will allow the construction of a formal, textual description of a software system even if it has a graphical userinterface as a component. An important aspect of this ...

Reeves, Steve
(1994)
This volume gathers together papers presented at the first in what is planned to be a series of annual meetings which aim to bring together people within New Zealand who have an interest in the use of formal ideas to enhance ...

Reeves, Steve
(1994)
PICTCalc is an interactive program written in LPA Prolog which has encoded within it the rules of MartinLöf's constructive type theory (CTT), a formal system based on the constructive or intuitionistic mathematics of ...

Goldson, Doug; Hopkins, Mike; Reeves, Steve
(1994)
Those of you who already have some experience of programming, or experience of simply using a computer, will know that computers can be very unforgiving. They are fussy, and unless you get things exactly right they will ...
Coauthors for Steve Reeves
Supervised by Steve Reeves