An Approach to Designing Safety Critical Systems using the Unified Modelling Language (2008)
Richard Hawkins, Ian Toyn, Iain Bate
Abstract. In this paper an approach to using the UML for developing safety critical systems is presented. We describe how safety analysis may be performed on a UML system model and how this analysis...
Refactoring in Maintenance and Development of Z Specifications and Proofs Abstract (2008)
Susan Stepney, Fiona Polack, Ian Toyn
Once you have proved your refinement correct, that is not the end. Real products, and their accompanying specifications, develop over time, with new improved versions having added functionality....
On the Formal Development of Safety-Critical Software (2008)
Andy Galloway, Frantz Iwu, John Mcdermid, Ian Toyn
Abstract. We reflect on the formal development models applicable to embedded control systems in light of our experience with safety-critical applications from the aerospace domain. This leads us to...
Type-constrained Generics for Z (2007)
Samuel Valentine, Ian Toyn, Susan Stepney, Steve King
. We propose an extension to Z whereby generic parameters may have their types partially constrained. Using this mechanism it becomes possible to define in Z much of its own schema calculus and...
Syntax 19 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 6.2 Metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . ....
Syntax 20 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 6.2 Metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . ....
Syntax 21 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 6.2 Metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . ....
Syntax 20 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 6.2 Metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . ....
Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, David Currie
Abstract. This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new...
D230: Z Notation-- Draft 0.6 (2007)
This draft incorporates the effects of decisions taken at meeting 41 of the Z panel and also technical progress made since then. Some highlights of recent progress are: 1. the lexis clause...
A Z Patterns Catalogue : I (2007)
Specification And Refactorings, Susan Stepney, Fiona Polack, Ian Toyn
World' specification from the LFM electronic purse development[Stepney et al. 2000]. This is a case where a specification originally written in a flat Delta/Xi style is then identified later as...
Susan Stepney, Fiona Polack, Ian Toyn
We present a pattern-based approach to depicting the structure of formal specifications. We propose a diagram meta-pattern, and instantiate it to produce a number of diagrammatic patterns for formal...
Proving properties of Stateflow models using ISO Standard Z and CADiZ (2005)
Abstract. This paper focuses on the use of ISO Standard Z and CADiZ in the formal validation of Stateflow models against requirements-oriented assumptions. It documents some of what the...
A Z Patterns Catalogue II - definitions and laws, v0.1 (2004)
Samuel H. Valentine, Susan Stepney, Ian Toyn, I Background
Contents Preface xiii I Background 1 1 Introduction 3 2 ISO Standard Z 5 2.1 History and current status 5 2.1.1 Z: the early years 5 2.1.2 The need for a change 6 2.1.3 Standardisation 7 2.1.4 Aims...
An outline pattern language for Z: five illustrations and two tables (2003)
Susan Stepney, Fiona Polack, Ian Toyn
Abstract. We introduce a pattern language for using formal methods in computer system engineering. We focus on the Z notation, but many of the patterns are adaptable to other formal notations, or can...
Patterns to guide practical refactoring: examples targetting promotion in Z (2003)
Susan Stepney, Fiona Polack, Ian Toyn
Abstract. Formal methods such as Z are generally criticised for their lack of practical applicability. As in other areas of software engineering, patterns help to construct, analyse and describe...
D.: ZML: XML Support for Standard Z (2003)
Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, Nicholas Daley, ...
Abstract. This paper proposes an XML format for standard Z.We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new...
An Outline Pattern Language for Z: five illustrations and two tables (2003)
Susan Stepney, Fiona Polack, Ian Toyn
We introduce a pattern language for using formal methods in computer system engineering. We focus on the Z notation, but many of the patterns are adaptable to other formal notations, or can be used...
D.: ZML: XML Support for Standard Z (2003)
Nicholas Daley, Nicholas Daley, Mark Utting, Mark Utting, Mark Utting, Ian Toyn, ...
Abstract. This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new...
ZML:XML support for standard Z. (2002)
Utting, Mark, Toyn, Ian, Sun, Jing, Martin, Andrew, Dong, Jin Song, Daley, Nicholas, ...
This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new proposal is...
ZML:XML support for standard Z. (2002)
Utting, Mark, Toyn, Ian, Sun, Jing, Martin, Andrew, Dong, Jin Song, Daley, Nicholas, ...
This paper proposes an XML format for standard Z. We describe several earlier XML proposals for Z, the problems and issues that arose, and the rationales behind our new proposal. The new proposal is...
1 Format of meeting Report on CZT discussions at ZB2002 (2002)
Mark Utting introduced CZT at the end of the first day, where several delegates expressed their opinions. Discussion continued over dinner that evening, where Mark was joined by Neil Robinson and Ian...
Reasoning Inductively about Z Specifications via Unification (2000)
. Selecting appropriate induction cases is one of the major problems in proof by induction. Heuristic strategies often use the recursive pattern of definitions and lemmas in making these selections....
Typechecking Z, Ian Toyn, Samuel H. Valentine, Susan Stepney, Steve King
. This paper presents some of our requirements for a Z typechecker: that the typechecker accept all well-typeable formulations, however contrived; that it gather information about uses of...
Towards Industrially Applicable Formal Methods: Three Small Steps, and One Giant Leap (1998)
John McDermid, Andy Galloway, Simon Burton, John Clark, Ian Toyn, Nigel Tracey, ...
In this paper we discuss issues in the development of formal methods for use in aerospace applications, reflecting our experience in working with both Rolls-Royce and British Aerospace. We discuss...
Innovations in the Notation of Standard Z (1998)
The second Committee Draft of the ISO standard "Z Notation" is expected to be published soon after the ZUM'98 proceedings. This paper provides an overview of Standard Z from the...
Towards industrially applicable formal methods: Three small steps, one giant leap (1998)
John Mcdermid, Andy Galloway, Simon Burton, John Clark, Ian Toyn, Nigel Tracey, ...
In this paper we discuss issues in the development of formal methods for use in aerospace applications, reflecting our experience in working with both Rolls-Royce and British Aerospace. We discuss...
Syntax 24 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6.2 Metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . ....
Syntax 20 6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 6.2 Metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . ....
David A. Duffy, Alan M. Frisch, Ian Toyn
.35> [2]. However, their work is limited essentially to confluent rewriting systems, and they are concerned principally with the issue of simultaneous proofs. Our application area will be more...
David A. Duffy, Alan M. Frisch, Ian Toyn
Z is a formal specification language that is extensively used in both academia and industry. Several tools have been developed for reasoning about Z specifications, but they all lack substantial...
Model Conjectures For Z Specifications (1995)
Jon G. Hall, John A. Mcdermid, Ian Toyn
The primary purpose of a specification is to make explicit the intentions of designers. For these intentions to be expressed precisely, a formal (mathematical) language should be used. The use of a...
CADiZ: An Architecture for Z Tools and its Implementation (1995)
This paper gives an overview of
Efficient binary transfer of pointer structures (1994)
Ian Toyn, Alan J. Dix, Call Cadiz
This paper presents a pair of algorithms for output and input of pointer structures in binary format. Both algorithms operate in linear space and time. They have been inspired by copying garbage...
Efficient Binary Transfer of Pointer Structures (1994)
This paper presents a pair of algorithms for output and input of pointer structures in binary format. Both algorithms operate in linear space and time. They have been inspired by copying compacting...
Efficient Binary Transfer of Pointer Structures (1994)
This paper presents a pair of algorithms for output and input of pointer structures in binary format. Both algorithms operate in linear space and time. They have been inspired by copying garbage...
CADiZ: An Architecture for Z Tools and its Implementation (1993)
CADiZ began as a type-checker for Z specifications embedded within troff documents. Addition of other functionality, such as expansion of schema calculus expressions, and alternative functionality,...
Retrieving Re-Usable Software Components By Polymorphic Type (1991)
Polymorphic types are labels classifying both (a) defined components in a library and (b) contexts of free variables in partially written programs. We propose to help programmers make better use of...
Patterns to Guide Practical Refactoring: Examples Targetting Promotion in Z
Susan Stepney, Fiona Polack, Ian Toyn
Formal methods such as Z are generally criticised for their lack of practical applicability. As in other areas of software engineering, patterns help to construct, analyse and describe formal texts....