Browsing by Author "Reeves, Steve"
Now showing items 173 of 73

Combining models for interactive system modelling
Bowen, Judy; Reeves, Steve (Springer International Publishing, 2017)Our approach for modelling interactive systems has been to develop models for the interface and interaction which are lightweight but with an underlying formal semantics. Combined with traditional formal methods to describe ... 
Using state machines for the visualisation of specifications via refinement
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 ... 
Design patterns for models of interactive systems
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 ... 
Composing patterns to construct secure systems
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 ... 
Eliciting usage contexts of safetycritical medical devices
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 ... 
A tale of two studies
Bowen, Judy; Reeves, Steve; Schweer, Andrea (ACS, 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 ... 
Modelling safety properties of interactive medical systems
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 ... 
Formal methods for interactive system: (FMIS 2013)
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 ... 
UIdriven testfirst development of interactive systems
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 ... 
From a community of practice to a body of knowledge: a case study of the formal methods community
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 ... 
Refinement for probabilistic systems with nondeterminism
Reeves, Steve; Streader, David (EPTCS, 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 ... 
Developing usability studies via formal models of UIs
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 ... 
Contexts, refinement and determinism
Reeves, Steve; Streader, David (Elsevier, 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 ... 
Guarded operations, refinement and simulation
Reeves, Steve; Streader, David (University of Waikato, Department of Computer Science, 20090610)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 ... 
A robust semantics hides fewer errors
Reeves, Steve; Streader, David (University of Waikato, Department of Computer Science, 20090610)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 ... 
UIDesign driven modelbased testing
Bowen, Judy; Reeves, Steve (EASST, 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 ... 
Refinement for user interface designs
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 ... 
Supporting multipath UI development with vertical reﬁnement
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 ... 
Guarded operations, refinement and simulation
Reeves, Steve; Streader, David (Elsevier, 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 ... 
A robust semantics hides fewer errors
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 ... 
Considering reachability when comparing data refinements
Reeves, Steve (University of Waikato, Department of Computer Science, 20081103)Adding considerations about reachability to the Logics of Specification Languages [1] chapter [2]. 
Generic tools via general refinement
Reeves, Steve; Streader, David (Elsevier B.V., 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 ... 
Formal models for user interface design artefacts
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 ... 
Data refinement and singleton failures refinement are not equivalent
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 ... 
Modular synthesis of discrete controllers
Malik, Petra; Malik, Robi; Streader, David; Reeves, Steve (IEEE Computer Society, 200707)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 ... 
Flexible refinement
Reeves, Steve; Streader, David (University of Waikato, 20070507)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 ... 
Using formal models to design user interfaces a case study
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, ... 
Feature refinement
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. ... 
State and eventbased refinement
Reeves, Steve; Streader, David (Department of Computer Science, University of Waikato, 20060901)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 ... 
LSB  Live and Safe B: Alternative semantics for Event B
Reeves, Steve; Streader, David (Department of Computer Science, University of Waikato, 20060701)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 ... 
Liberalising Event B without changing it
Reeves, Steve; Streader, David (Department of Computer Science, University of Waikato, 20060701)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 ... 
Constructing programs or processes
Reeves, Steve; Streader, David (Institute for Information Processing and Computer Supported New Media, 20051228)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 ... 
Constructing programs or processes
Reeves, Steve; Streader, David (Department of Computer Science, University of Waikato, 200512)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 ... 
Stepwise refinement of processes
Reeves, Steve; Streader, David (20050101)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 ... 
Including design guidelines in the formal specification of interfaces in Z
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 ... 
Atomic components
Reeves, Steve; Streader, David (University of Waikato, Department of Computer Science, 200402)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 ... 
Unifying state and process determinism
Reeves, Steve; Streader, David (University of Waikato, Department of Computer Science, 200402)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 ... 
The syntax and semantics of μCharts
Reeve, Greg; Reeves, Steve (University of Waikato, Department of Computer Science, 200402)μ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 ... 
Fair testing revisited: A processalgebraic characterisation of conflicts
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 ... 
A logic for schemabased program development
Henson, Martin C.; Reeves, Steve (SpringerVerlag London Ltd, 20030701)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 ... 
Z logic and its consequences
Henson, Martin C.; Reeves, Steve; Bowen, Jonathan P. (Institute of Informatics, 200306)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 ... 
Comparison of data and process refinement
Reeves, Steve; Streader, David (University of Waikato, Department of Computer Science, 200305)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 ... 
Statebased and processbased value passing
Reeves, Steve; Streader, David (Formal Methods Europe, 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 ... 
Investigating Z
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 ... 
An analysis of total correctness refinement models for partial relation semantics I
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. ... 
Operation Refinement and Monotonicity in the Schema Calculus
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 ... 
Results on formal stepwise design in Z
Deutsch, Moshe; Henson, Martin C.; Reeves, Steve (IEEE Computer Society, 20021201)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 ... 
μChartbased specification and refinement
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 ... 
Idioms for µcharts
Anderson, Grant; Reeve, Greg; Reeves, Steve (IEEE COMPUTER SOC, 20010801)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 ... 
Experiences using Z animation tools.
Reeve, Greg; Reeves, Steve (University of Waikato, Department of Computer Science, 20010501)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 ... 
Teaching formal methods lite via testing
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 ... 
µCharts and Z: Examples and extensions
Reeve, Greg; Reeves, Steve (IEEE COMPUTER SOC, 20001201)μ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 ... 
µCharts and Z: Extending the translation
Reeve, Greg; Reeves, Steve (University of Waikato, Department of Computer Science, 200008)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. ... 
A survey of software development practices in the New Zealand software industry
Groves, Lindsay; Nickson, Ray; Reeve, Greg; Reeves, Steve; Utting, Mark (IEEE Computer Society, 200004)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 ... 
µCharts and Z: hows, whys and wherefores
Reeve, Greg; Reeves, Steve (University of Waikato, Department of Computer Science, 200003)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. 
Program Development and Specification Refinement in the Schema Calculus
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 ... 
Revising Z: part II  logical development
Henson, Martin C.; Reeves, Steve (19991201)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 ... 
Revising Z: part I  logic and semantics
Henson, Martin C.; Reeves, Steve (19991201)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 ... 
A survey of software requirements specification practices in the New Zealand software industry
Groves, Lindsay; Nickson, Ray; Reeve, Greg; Reeves, Steve; Utting, Mark (Computer Science, University of Waikato, 199906)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 ... 
Constructive Mathematics in Theory and Programming Practice
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 ... 
New foundations for Z
Henson, Martin C.; Reeves, Steve (University of Waikato, Department of Computer Science, 199803)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. ... 
A logic for the schema calculus
Henson, Martin C.; Reeves, Steve (University of Waikato, Department of Computer Science, 199803)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 ... 
Revising Z: semantics and logic
Henson, Martin C.; Reeves, Steve (University of Waikato, Department of Computer Science, 199803)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 ... 
Specifying collaborative software: a proposal
Reeves, Steve (IEEE Computer Society Press, 19980101)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 ... 
CSCW in New Zealand: a snapshot
Blackett, Colin; Reeves, Steve (199607)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 ... 
Notes: an experiment in CSCW
Apperley, Mark; Gianoutsos, Simon; Grundy, John C.; Paynter, Gordon W.; Reeves, Steve; Venable, John R. (199604)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 ... 
A teaching and support tool for building formal models of graphical userinterfaces
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 ... 
A teaching and support tool for building formal models of graphical userinterfaces
Reeves, Steve (University of Waikato, Department of Computer Science, 199508)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 ... 
Towards an integrated refinement environment for formal program development
Reeves, Steve; Grundy, John C. (University of Waikato, Department of Computer Science, 199508)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 ... 
A logic for specifying and reasoning about cooperative environments
Reeves, Steve (University of Waikato, Department of Computer Science, 199508)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 ... 
Proceedings of the First New Zealand Formal Program Development Colloquium
Reeves, Steve (199411)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 ... 
A calculator for supporting derivation in constructive typetheory: PICTCalc
Reeves, Steve (199406)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 ... 
MiraCalc: the Miranda Calculator, the Unix version
Goldson, Doug; Hopkins, Mike; Reeves, Steve (199404)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
Steve Reeves has 30 coauthors in Research Commons.
 Grant Anderson
 Mark Apperley
 Len Bass
 Colin Blackett
 Jonathan P. Bowen
 Judy Bowen
 Douglas Bridges
 Sally Jo Cunningham
 Moshe Deutsch
 Simon Gianoutsos
 Doug Goldson
 Lindsay Groves
 John C. Grundy
 Martin C. Henson
 Annika Hinze
 Mike Hopkins
 Doris Jung
 Ihor Kuz
 Petra Malik
 Robi Malik
 Ray Nickson
 Gordon W. Paynter
 Colin Pilbrow
 Greg Reeve
 Paul Rimba
 Andrea Schweer
 David Streader
 Mark Utting
 John R. Venable
 Liming Zhu
Supervised by Steve Reeves
Showing up to 5 theses  most recently added to Research Commons first.

On Conflicts in Concurrent Systems
Ware, Simon Ian (University of Waikato, 2014)This dissertation studies conflicts. A conflict is a bug in concurrent systems where one or more components of the system may potentially be blocked from completing their task. This dissertation investigates how nonconflicting ... 
Analysing Reverse Engineering Techniques for Interactive Systems
Lin, Feifei (Amy) (University of Waikato, 2012)Reverse engineering is the process of discovering a model of a software system by analyzing its structure and functions. Reverse engineering techniques applied to interactive software applications (e.g. applications with ... 
Formal Models and Refinement for Graphical User Interface Design
Bowen, Judy (The University of Waikato, 2008)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 ...