Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2014 | Buch

An Introduction to Z Kapitel lesen Erstes Kapitel lesen

Refinement in Z and Object-Z

Foundations and Advanced Applications

verfasst von: John Derrick, Eerke A. Boiten

Verlag: Springer London

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

Refinement is one of the cornerstones of the formal approach to software engineering, and its use in various domains has led to research on new applications and generalisation. This book brings together this important research in one volume, with the addition of examples drawn from different application areas. It covers four main themes:

Data refinement and its application to ZGeneralisations of refinement that change the interface and atomicity of operationsRefinement in Object-ZModelling state and behaviour by combining Object-Z with CSP

Refinement in Z and Object-Z: Foundations and Advanced Applications provides an invaluable overview of recent research for academic and industrial researchers, lecturers teaching formal specification and development, industrial practitioners using formal methods in their work, and postgraduate and advanced undergraduate students.

This second edition is a comprehensive update to the first and includes the following new material:

Early chapters have been extended to also include trace refinement, based directly on partial relations rather than through totalisationProvides an updated discussion on divergence, non-atomic refinements and approximate refinementIncludes a discussion of the differing semantics of operations and outputs and how they affect the abstraction of models written using Object-Z and CSPPresents a fuller account of the relationship between relational refinement and various models of refinement in CSPBibliographic notes at the end of each chapter have been extended with the most up to date citations and research

Inhaltsverzeichnis

Frontmatter

Refining Z Specifications

Frontmatter
Chapter 1. An Introduction to Z
Abstract
This chapter introduces the Z specification notation. Z is a formal specification language. It is a language in that it provides a notation for describing the behaviour of a system, and it is formal in that it uses mathematics to do so. The mathematics is simple, consisting of first order predicate logic and set theory. However, based upon this, it offers a very elegant way of structuring the mathematics to provide a specification of the system under consideration. In this chapter we present the notations for logic, sets and relations, the schema notation and the schema calculus, leading to the definition of an abstract data type in the “states-and-operations” style, and the first example refinement.
John Derrick, Eerke A. Boiten
Chapter 2. Simple Refinement
Abstract
This chapter introduces the notion of refinement informally, and discusses the refinement of operations on a given data type. We first present a semi-formal motivation of the simplest refinement relation of all, namely operation refinement. Operation refinement can be applied to individual operations without reference to the other operations present in the abstract data type (ADT). The other simple refinement rules presented in this chapter, establishing and imposing invariants, only apply in the context of a full ADT, and require abstraction, in the sense of the state not being observable.
John Derrick, Eerke A. Boiten
Chapter 3. Data Refinement and Simulations
Abstract
This chapter presents the formal definitions of data refinement and upward and downward simulation, initially for total relations. Various ways of applying these definitions to abstract data types with partial relations are then considered. The central part of this chapter is the standard definition of data refinement for relational data types, the definitions of upward and downward simulations, and the statement of their soundness and joint completeness. This theory was initially formulated for ADTs whose operations are total relations. In order to apply this theory to a specification language we look at how operations in a specification are modelled as partial relations. The application of the simulation rules to specifications with partial operations leads to the simulation rules as they are normally presented.
John Derrick, Eerke A. Boiten
Chapter 4. Refinement in Z
Abstract
Chapter 4 translates the relational refinement rules for upward and downward simulation into rules for specifications consisting of Z schemas. Particular attention is given to the role of inputs and outputs in Z.
In this chapter, we formulate the theory of data refinement for Z. This is done systematically: a relational interpretation will be given for the standard Z ADT as defined in Chap. 1. We apply the simulation based refinement rules from Chap. 3 to these interpretations, and then reformulate them directly for Z schemas (i.e., without using the relational meta-language). In order to separate the issues involved with this derivation, we first derive rules for Z ADTs without inputs and outputs, and then show the more complicated derivation in the presence of inputs and outputs. Finally, this chapter presents a collection of examples of data refinement in Z.
John Derrick, Eerke A. Boiten
Chapter 5. Calculating Refinements
Abstract
In this chapter we discuss an alternative approach to refinement where we move the emphasis from verification to calculation. That is, instead of writing down the concrete operations and verifying that they are refinements, we will calculate the operations and initialisation. To do this, all that is needed is the abstract specification, a description of the concrete state space and a retrieve relation which links the abstract to concrete. The result of this calculation will be the most general data refinement of the abstract specification with respect to the concrete state space and retrieve relation used.
John Derrick, Eerke A. Boiten
Chapter 6. Promotion
Abstract
In this chapter we discuss a technique for structuring Z specifications known as promotion. The purpose of promotion is to provide an elegant way of composing specifications in order to build multiple indexed instances of a single component. To do so the component is described as a local state together with operations acting on that state, a global state is then defined which consists of multiple instances of this local state together with global operations defined in terms of the local operations and a special promotion schema. In this chapter we describe the circumstances when an elegant relationship between promotion and refinement holds: specifically when is the promotion of a refinement a refinement of a promotion. We also look at some commonly arising cases.
John Derrick, Eerke A. Boiten
Chapter 7. Testing and Refinement
Abstract
This chapter explores the relationship between testing and refinement. In particular, it looks at how tests for a refinement can be derived from tests for the abstract system. We discuss both how to derive tests from a formal specification, and also how tests can be refined for use with an implementation. We also consider how concrete tests can be calculated from abstract ones for refinements which are downward or upward simulations.
John Derrick, Eerke A. Boiten
Chapter 8. A Single Simulation Rule
Abstract
Previous chapters have considered refinement in terms of upward and downward simulations, which are sound and jointly complete—i.e., all refinements can be proved using a combination of upward and downward simulation steps. This chapter presents an alternative in the form of powersimulations which provide for a single complete refinement rule for Z. This requires a change in the underlying framework, moving from relations to possibility mappings.
John Derrick, Eerke A. Boiten

Interfaces and Operations: ADTs Viewed in an Environment

Frontmatter
Chapter 9. Refinement, Observation and Modification
Abstract
This is the first of a series of chapters presenting more liberal notions of refinement in Z, based on relaxations of the underlying assumptions—in this particular case, “representation hiding”, i.e. that the state variables are hidden from the environment. We consider some different specification styles, expressed as variants on the standard abstract data type from earlier chapters. State variables may be visible to the environment, even modifiable, or there may be operations that observe part of the state while not changing it (“displays”), to model for example the situation where certain information is constantly available on a screen. For each of these modifications, we derive refinement rules by interpreting the variant ADTs in terms of standard ADTs. Thus, the semantic basis from Chap. 3 is retained unchanged.
John Derrick, Eerke A. Boiten
Chapter 10. IO Refinement
Abstract
As formal development steps are concerned with changes of abstraction level, it is natural to also apply such changes to the inputs and outputs of a system. Indeed, many previous textbooks on Z and refinement had included subtle manipulations of inputs and outputs in refinement steps in their examples, without considering formal justifications. This chapter describes the new notion of “IO refinement”, which provides the foundations for changing, adding, or deleting inputs and outputs in refinement steps, by retaining the relational theory of Chap. 3 but generalising the Z refinement rules as derived in Chap. 4.
John Derrick, Eerke A. Boiten
Chapter 11. Weak Refinement
Abstract
The notion of operation in earlier chapters is that they are available for the environment to execute. In modelling distributed and reactive systems, it is common to also use “internal” operations which are under the control of the system rather than of the observer. From a generalisation of the definition of data refinement in Chap. 3, we obtain versions of the simulation conditions which allow the refinement, introduction and removal of such internal operations. In this, we also consider the possibility of “livelock”, where internal operations are continuously enabled, its impact on refinement conditions, and the related notion of divergence.
John Derrick, Eerke A. Boiten
Chapter 12. Non-atomic Refinement
Abstract
Another way in which the level of abstraction can change in development is through the granularity of operations, in particular changing one abstract operation into several concrete ones. This chapter considers the consequences of allowing operations to be decomposed in refinement, which involves further generalisation of the theory from Chap. 3. This is often known as non-atomic or action refinement in the literature. The final sections discuss applications to verifying concurrent data structures.
John Derrick, Eerke A. Boiten
Chapter 13. Case Study: A Digital and Analogue Watch
Abstract
This chapter exemplifies the techniques from Chaps. 9–12 in an extended case study. It describes a variety of specifications and implementations of a digital watch, and how their validity is founded on the new notions of refinement defined earlier.
John Derrick, Eerke A. Boiten
Chapter 14. Further Generalisations
Abstract
This chapter concludes the discussion on more liberal forms of Z refinement, by discussing a few more options, and how they all fit together. It looks at whether new operations can be added without relating to any previous operations, or as multiple copies of previous ones: alphabet extension, and alphabet translation. It also describes a generalisation which looks at approximate refinement between abstract and concrete systems.
John Derrick, Eerke A. Boiten

Object-Oriented Refinement

Frontmatter
Chapter 15. An Introduction to Object-Z
Abstract
This chapter starts the discussion of refinement in an object oriented setting. To do so it introduces the Object-Z specification language as a canonical example, focusing on the additional features in Object-Z and the differences between Z and Object-Z that impact on the theory of refinement in subsequent chapters.
John Derrick, Eerke A. Boiten
Chapter 16. Refinement in Object-Z
Abstract
In this chapter we adapt the refinement rules derived for Z to Object-Z specifications consisting of just a single class, taking into account the consequences of the different interpretation of preconditions. We also consider how weak refinement and non-atomic refinement may be applied to Object-Z. Finally, we discuss the relation between refinement, and two other important concepts in object orientation: subtyping and inheritance.
John Derrick, Eerke A. Boiten
Chapter 17. Class Refinement
Abstract
The final chapter of this part considers more complex Object-Z specifications, in particular ones that involve objects and promotions of their operations. Specifications consisting of multiple classes enable a wide range of more complex refinements, by allowing (for example) classes to be split or merged. This chapter investigates how such refinements can be verified, and concludes with an investigation of compositionality of refinement in Object-Z.
John Derrick, Eerke A. Boiten

Modelling State and Behaviour

Frontmatter
Chapter 18. Combining CSP and Object-Z
Abstract
This chapter starts the discussion of formal notations that combine state-based modelling as in (Object-)Z, with the modelling of behaviour. Our particular choice for a behavioural notation is CSP, thus this chapter includes a short introduction to CSP first. Then we show how component specifications can be given in Object-Z, and then combined using CSP to specify their interactions. This integration is possible due to the existence of a common semantic model.
John Derrick, Eerke A. Boiten
Chapter 19. Refining CSP and Object-Z Specifications
Abstract
For systems described using a combination of Object-Z and CSP, several possibilities for refinement exist. This chapter discusses some of these. In particular, it turns out that such systems can be refined component by component, due to a correlation between refinement in Object-Z and refinement in CSP.
John Derrick, Eerke A. Boiten
Chapter 20. Conclusions
Abstract
This concluding chapter briefly discusses how refinement in a number of similar formalisms compares to refinement in Z and Object-Z. In particular, it considers VDM, B, Event-B, Abstract State Machines, and the Refinement Calculus.
John Derrick, Eerke A. Boiten
Backmatter
Metadaten
Titel
Refinement in Z and Object-Z
verfasst von
John Derrick
Eerke A. Boiten
Copyright-Jahr
2014
Verlag
Springer London
Electronic ISBN
978-1-4471-5355-9
Print ISBN
978-1-4471-5354-2
DOI
https://doi.org/10.1007/978-1-4471-5355-9