The creation of a consistent system description is a challenging problem of requirements engineering. Formal and informal reasoning can greatly contribute to meet this challenge. However, this demands that formal and informal reasoning and the system description are connected in such way that the reasoning permits drawing conclusions about the system description.

We describe an incremental approach to requirements modelling and validation that incorporates formal and informal reasoning. Our main contribution is an approach to requirements tracing that delivers the necessary connection that links the reasoning to the system description. Formal refinement is used in order to deal with large and complex system descriptions.

We discuss tool support for our approach of requirements tracing that combines informal requirements modelling with formal modelling and verification while tracing requirements among each other and into the formal model.

Establishing the absence of deadlocks is important in many applications of formal methods. The use of model checking for finding deadlocks in formal models is limited because in many industrial applications the state space is either infinite or much too large to be explored exhaustively.

In this paper we propose a constraint-based approach to finding deadlocks employing the ProB constraint solver to find values for the constants and variables of formal models that describe a deadlocking state. We present the general technique, as well as various improvements that had to be performed on ProB's Prolog kernel, such as reification of membership and arithmetic constraints.

ProB typically finds counter examples to deadlock-freedom constraints, a formula of about 900 partly nested conjunctions and disjunction among them 80 arithmetic and 150 set-theoretic predicates (in total a formula of 30 pages), in under two seconds.

We also present other successful applications of this new technique, in particular to BPEL processes. Experiments using SAT and SMT solvers on these constraints were thus far unsuccessful.

We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose. We present an algorithm for simultaneous multi-level animation of refinement, and show how it can be used to detect a variety of errors that occur frequently when using refinement. The algorithm has been implemented in ProB and we applied it to several case studies, showing that multi-level animation is tractable also on larger models. We present empirical results and discuss how the algorithm can be combined with symmetry reduction.

Establishing the absence of deadlocks is important in many applications of formal methods. The use of model checking for finding deadlocks in formal models is limited because in many industrial applications the state space is either infinite or much too large to be explored exhaustively. In this paper we propose a constraint-based approach to finding deadlocks employing the ProB constraint solver to find values for the constants and variables of formal models that describe a deadlocking state. We discuss the principles of the technique implemented in ProB's Prolog kernel and present some results of a larger case study to which we have applied the approach.

Tracing between informal requirements and formal models is challenging. A method for such tracing should permit to deal efficiently with changes to both the requirements and the model. A particular challenge is posed by the persisting interplay of formal and informal elements.

In this paper, we describe an incremental approach to requirements validation and systems modelling. Formal modelling facilitates a high degree of automation: it serves for validation and traceability.

The foundation for our approach are requirements that are structured according to the WRSPM reference model. We provide a system for traceability with a state-based formal method that supports refinement. We do not require all specification elements to be modelled formally and support incremental incorporation of new specification elements into the formal model. Refinement is used to deal with larger amounts of requirements in a structured way.

We provide a small example using Problem Frames and Event-B to demonstrate our approach.

The development of the Event-B formal method and the supporting tools Rodin and ProB was guided by practical experiences with the B-Method, the Z specification notation, VDM and similar practical formal methods. The case study discussed in this article - a cruise control system - is a serious test of industrial use. We report on where Event-B and its tools have succeeded, where they have not. We also report on advances that were inspired by the case study. Interestingly, the case study was not a pure formal methods problem. In addition to Event-B, it used Problem Frames for capturing requirements. The interaction between the two proved to be crucial for the success of the case study. The heart of the problem was tracing informal requirements from Problem Frames descriptions to formal Event-B models. To a large degree, this issue dictated the approach that had to be used for formal modelling. A dedicated record theory and dedicated tool support were required. The size of the formal models rather than complex individual formulas was the main challenge for tool support.

Event-B does not provide specific support for the modelling of problems that require some structuring, such as, local variables or sequential ordering of events. All variables need to be declared globally and sequential ordering of events can only be achieved by abstract program counters. This has two unfortunate consequences: such models become less comprehensible - we have to infer sequential ordering from the use of program counters; proof obligation generation does not consider ordering - generating too many proof obligations (although these are usually trivially discharged). In this article we propose a method for specifying structured models avoiding, in particular, the use of abstract program counters. It uses a notation that mainly serves to drive proof obligation generation. However, the notation also describes the structure of a model explicitly. A corresponding graphical notation is introduced that visualises the structure of a model.

We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose. We present an algorithm for simultaneous multi-level animation of refinement, and show how it can be used to detect a variety of errors that occur frequently when using refinement. The algorithm has been implemented in ProB and we applied it to several case studies, showing that multi-level animation is tractable also on larger models.

Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing systems can be addressed by formal refinement introducing all the necessary details piecemeal. We report on preliminary results that we have obtained for tracing informal natural-language requirements into formal models across refinement levels. The approach uses the WRSPM reference model for requirements modeling, and Event-B for formal modeling and formal refinement. The combined use of WRSPM and Event-B is facilitated by the rudimentary refinement notion of WRSPM, which provides the foundation for tracing requirements to formal refinements.

We assume that requirements are evolving, meaning that we have to cope with frequent changes of the requirements model and the formal model. Our approach is capable of dealing with frequent changes, making use of corresponding techniques already built into the Event-B method.

Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges on the fact that any particular model has an appropriate semantics. In Event-B this semantics is provided implicitly by proof obligations associated with a model. There is no fixed semantics though. In this article we argue that this approach is beneficial to modelling because we can use similar proof obligations across a variety of modelling domains. By way of two examples we show how similar proof obligations are linked to different semantics. A small set of proof obligations is thus suitable for a whole range of modelling problems in diverse modelling domains.

Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. In this article we present the Rodin modelling tool that seamlessly integrates modelling and proving. We outline how the Event-B language was designed to facilitate proof and how the tool has been designed to support changes to models while minimising the impact of changes on existing proofs. We outline the important features of the prover architecture and explain how well-definedness is treated. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods.

Event-B and the Rodin tool use a number of simple techniques that make the modelling method around them effective in practical applications. We present two of these techniques, anticipation and witnesses. It is interesting how a couple of very simple techniques are so important for the method to work. Finally we propose a small enhancement of Event-B that would extend the use of witnesses.

The Event-B method can be used to model all sorts of discrete event systems, among them sequential programs. We have made the experience that the minimalist nature of Event-B is of advantage when it comes to tool support and to using proof as a means to analyse a model. The downside of the minimalism is that when models get more complex the lack of structure in the models can make them cluttered with auxiliary variables. System decomposition will not solve this problem. This can not be reasonably applied to a sequential program. In this article we describe our experiences with using Event-B by way of an example. We show how we verified iterative Quicksort in Event-B and intersperse our observations and criticisms. We use them to formulate some suggestions of how we believe Event-B should evolve in future. Some of the minimalism may have to be abandoned in favour of more clarity of the produced formal models.

Usually we teach formal methods relying for a large part on one kind of reasoning technique about a formal model. For instance, we either use formal proof or we use model-checking. It would appear that it is already hard enough to learn one technique and having to cope with two puts just another burden on the students. This is not our experience. Especially model-checking is easily used to complement formal proof. It only relies on an intuitive operational understanding of a formal model. In this article we show how using model-checking, animation, and formal proof together can be used to improve understanding of formal models. We demonstrate how animation can help finding an explanation for a failing proof. We also demonstrate where animation or model-checking may not help and where proving may not help. For most part use of another tool pays off. Proof obligations present intentionally a static view of a system so that we focus on abstract properties of a model and not on its behaviour. By contrast model-checking provides a more dynamic view based on an operational interpretation. Both views are valuable aids to reasoning about a model.

When teaching Event-B to beginners, we usually start with models that are already good enough, demonstrating occasionally some standard techniques like ``invariant strengthening''. We show that we got it essentially right but need to make improvements here and there. However, this is not how we really create formal models. To a beginner, getting shown only nearly perfect models is overwhelming. So we should start earlier and show how we usually get models wrong initially. This provides ample opportunity to demonstrate the strengths of formal reasoning (and the weaknesses). The principal strength of formal reasoning lies in its capacity to locate mistakes in a model and to suggest corrections. A beginner should learn how to profit from his mistakes by improving his understanding of the model. A weakness of formal reasoning is that we only find mistakes that we expect, for example, invariant violation or non-termination. Mistakes that do not fall into one of these categories may slip through. In this article we present how a formal model is created by refinement and alteration. The approach employs mathematical methodology for problem solving and a software tool. Both aspects are important. Mathematical methodology provides ways to turn mistakes into improvements. The software tool is necessary to ease the impact of changes on a model and to obtain rapid feed back. We begin with a set of assumptions and requirements, the problem, and set out to solve it, giving a more vivid picture of how formal methods work.

Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. The continued development of the Rodin toolset is funded by the EU research project ICT 214158 DEPLOY (Industrial deployment of system engineering methods providing high dependability and productivity) www.deploy-project.eu. The toolset was originally developed as part of the project IST 511599 RODIN (Rigorous Open Development Environment for Complex Systems).

Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges on the fact that any particular model has an appropriate semantics. In Event-B this semantics is provided implicitly by proof obligations associated with a model. There is no fixed semantics though. In this article we argue that this approach is beneficial to modelling because we can use similar proof obligations across a variety of modelling domains. By way of two examples we show how similar proof obligations are linked to different semantics. A small set of proof obligations is thus suitable for a whole range of modelling problems in diverse modelling domains.

A reasonable approach to formal modelling is to start with a specification that captures the requirements of a system and then use formal refinement to implement it. The problem with this approach is that for complex systems the specification itself is complex. It becomes a challenge to say whether the specification is the right one for the given requirements. Sometimes requirements also concern features of a system closely related to its implementation. This would make an abstract specification necessarily incomplete. We believe that it is better not to follow the rigid approach to modelling described above. Instead, we argue that the specification itself should be elaborated by refinement. Ultimately, the distinction between specification and implementation is no longer made in the strict sense above. There is only one model of the system that is connected by successive refinements. Using Event-B, we demonstrate how this can be applied to cope with the complexity of specifications. On the one hand we benefit from the reduced number of detail to consider at different times. On the other hand we are encouraged to reason about the formal model since the beginning and to rethink it occasionally to capture better its intended behaviour and match the requirements.

We argue that formal modeling should be the starting point for any serious development of computer systems. This claim poses a challenge for modeling: at first it must cope with the constraints and scale of serious developments. Only then it is a suitable starting point. We present three techniques, refinement, decomposition, and instantiation, that we consider indispensable for modeling large and complex systems. The vehicle of our presentation is Event-B, but the techniques themselves do not depend on it.

Event-B is a notation and method for discrete systems modelling by refinement. The notation has been carefully designed to be simple and easily teachable. The simplicity of the notation takes also into account the support by a modelling tool. This is important because Event-B is intended to be used to create complex models. Without appropriate tool support this would not be possible. This article presents justifications and explanations for the choices that have been made when designing the Event-B notation.

We present a software tool, the Rodin tool, for formal modelling in Event-B. Event-B is a notation and method developed from the B-Method and is intended to be used with an incremental style of modelling. The idea of incremental modelling has been taken from programming: modern programming languages come with integrated development environments that make it easy to modify and improve programs. The Rodin tool provides such an environment for Event-B. The two main characteristics of the Rodin tool are its ease of use and its extensibility. The tool focuses on modelling. It is easy to modify models and try out variations of a model. The tool can also be extended easily. This will make it possible to adapt the tool specific needs. So the tool can be adapted to fit into existing development processes instead demanding the opposite. We believe that these two characteristics are major points for industrial uptake.

Event-B is a notation and method for discrete systems modelling by refinement. We introduce a small but very useful construction: qualitative probabilistic choice. It extends the expressiveness of Event-B allowing us to prove properties of systems that could not be formalised in Event-B before. We demonstrate this by means of a small example, part of a larger Event-B development that could not be fully proved before. An important feature of the introduced construction is that it does not complicate the existing Event-B notation or method, and can be explained without referring to the underlying more complicated probabilistic theory. The necessary theory itself is briefly outlined in this article to justify the soundness of the proof obligations given. We also give a short account of alternative constructions that we explored, and rejected.

We consider modelling indispensable for the development of complex systems. Modelling must be carried out in a formal notation to reason and make meaningful conjectures about a model. But formal modelling of complex systems is a difficult task. Even when theorem provers improve further and get more powerful, modelling will remain difficult. The reason for this that modelling is an exploratory activity that requires ingenuity in order to arrive at a meaningful model. We are aware that automated theorem provers can discharge most of the onerous trivial proof obligations that appear when modelling systems. In this article we present a modelling tool that seamlessly integrates modelling and proving similar to what is offered today in modern integrated development environments for programming. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods.

All modelling items used in a formal B development are kept in the database kernel-component. This database is analysed by the static checker with respect to various properties the collection of modelling items must satisfy. When the static checker has accepted the database as being consistent, its items can be submitted to proof obligation generation and subsequent proof. In addition to marking modelling items as consistent the static checker computes auxiliary data structures to improve performance of all tasks that involve using items stored in the database.

This text describes a proof obligation generator for EventB. Most of the document describes the actual generated proof obligations and justification of their correctness. The algorithm for their generation is very simple. We distinguish generated proof obligations from theoretical ones. Theoretical proof obligations are well-suited for hand-written mathematical proofs but less suited for machine-assisted proof. In particular, generated proof obligations have be obtained by decomposing theoretical proof obligations as far as possible so that they are as simple as possible; and hopefully provable by an automatic prover. Substitutions produced by the proof obligation generator are left unevaluated. These are applied in a preprocessing step of the proof manager. The reason for this is to keep the design of the proof obligation generator distinct from the actual provers. By using witnesses in models a part of the proof has been moved into modelling itself. The price to pay is that one has to think about proving while modelling. The advantage is that proofs are decomposed and almost all existential quantifiers are removed from the consequents of proof obligations. There are three main sections on contexts, initial models, and refined models. Each of these contains three subsections: the description subsection introduces the notation used in the section; the theory subsection presents the theoretical proof obligations and derives the generated proof obligations by proof; the generated proof obligations subsection contains the list of proof obligations to be generated by the proof obligation generator. This last section also contains proof obligations for well-definedness. On first reading well-definedness proof obligations should be ignored. These are necessary but are actually not derived from the theoretical proof obligations.

Le développement de systèmes à l'aide du raffinement est une méthode formelle qui permet de gérer la complexité d'un système et de sa preuve de correction en permettant l'introduction des détails du système pas à pas. A partir d'un système abstrait, chaque pas de raffinement est prouvé correct jusqu'au niveau d'implantation. La méthode B est basée sur le raffinement, mais elle aide aussi à gérer les obligations de preuve qui se présentent à chaque pas. La méthode B est l'une des méthodes qui possdent le plus d'outils support pour être utilisée en pratique. Les systèmes électroniques deviennent de plus en plus complexes, l'approche traditionnelle qui consiste à garantir la correction par la simulation ne suffit plus. Par ailleurs, les systèmes électroniques sont de plus en plus présents dans les systmes de toute nature et l'exigence en qualité est de plus en plus forte. Les méthodes formelles sont les seules à pouvoir faire face à cette complexité croissante. Nous présentons dans cet article comment la méthode B peut être utilisée pour la conception des systèmes électroniques.

The approach proposed in this paper introduces a hardware/software co-design framework for developing complex embedded systems. The method relies on formal proof of system properties at every phase of the co-design cycle. The key concept is the combined use of UML and the B language for system modeling and design, and the seamless transition from UML specifications to system descriptions in B. The final system prototype emerges from correct-by-construction subsystems described in the B language; the hardware components are translated in VHDL/SystemC, while for the software components C/C++ is used. The outcome is a formally proven correct system implementation. The efficiency of the proposed method is exhibited through the design of a case study from the telecommunication domain.

Formal notations like B or action systems support a notion of refinement. Refinement relates an abstract specification AA to a more deterministic concrete specification CC. Knowing AA and CC one proves CC refines, or implements, specification AA. In this study we consider specification AA as given and concern ourselves with a way to find a good candidate for implementation CC. To this end we classify all implementations of an abstract specification according to their performance. We distinguish performance from correctness. Concrete systems that do not meet the abstract specification correctly are excluded. Only the remaining correct implementations CC are considered with respect to their performance. A good implementation of a specification is identified by having some optimal behaviour in common with it. In other words, a good refinement corresponds to a reduction of non-optimal behaviour. This also means that the abstract specification sets a boundary for the performance of any implementation. We introduce the probabilistic action system formalism which combines refinement with performance. In our current study we measure performance in terms of long-run expected average-cost. Performance is expressed by means of probability and expected costs. Probability is needed to express uncertainty present in physical environments. Expected costs express physical or abstract quantities that describe a system. They encode the performance objective. The behaviour of probabilistic action systems is described by traces of expected costs. A corresponding notion of refinement and simulation-based proof rules are introduced. Probabilistic action systems are based on discrete-time Markov decision processes. Numerical methods solving the optimisation problems posed by Markov decision processes are well-known, and used in a software tool that we have developed. The tool computes an optimal behaviour of a specification AA thus assisting in the search for a good implementation CC.

In this chapter we discuss modeling of hardware and translation to VHDL. Translation to SystemC or Verilog is similar. However VHDL is easier to read and we use VHDL synthesis tools. Translation is important to provide a complete path from formal models to a circuit. Equally important we need a refinement method to arrive at a formal circuit description that can be translated. This method has some significant differences to the refinement method for software. As one would expect, they are virtually not present at system level but become more and more visible as an actual implementation is approached. This means that the initial refinement steps used in hardware are, in principle, also applicable to software, and vice versa. The subset of the B-language that serves to describe hardware is called BHDL. The definition of the BHDL subset is oriented at the register transfer level for hardware description.

The approach presented in this book relies on the unification of system specification environments for developing electronic systems that are formally proven to be correct (correct-by-construction systems). The key concept conveyed is the formal proof of system properties, which is carried out at every phase of the co-design cycle. The main idea is to build fully functional system models that are formally proven to be correct, and based on them to produce automatically the hardware and the software parts of the system. The approach presented relies on the combined use of UML and B language.

This chapter presents a study of the SAE J1708 Serial Communication link. The study is carried out in Event-B, an extension of the B method. The system is implemented and decomposed using step-wise refinement. We present how to derive with this method a cycle-accurate hardware model. The model of the communication link system is composed of an arbitrary finite number of identical components that run concurrently. The model contains synchronisation of these components required to control access to the communication link. At the end of the refinement we obtain an implementable model of the components which is translated into VHDL. The generated VHDL design is synthesizable, meaning that the implementable B model is synthesizable as well.

Formal refinement as offered by the B method has been shown to be applicable in practice and to scale up. However, it has been recognised that it is difficult communicate a formal B model with customers. Recently, the UML has been investigated as an interface to rigorous formal B models to facilitate this communication. The UML is generally accepted as being a good vehicle for communicating models of systems. Availability of this interface to the B method addresses a major problem faced by most formal methods: How to validate a formal model with a customer who is not formal methods expert? In this chapter we present an approach to the development of a formally verified circuit implementing a Hamming encoder/decoder. The UML-B is used as a formal specification language and the B method is used to prove refinements until the implementation level at which we can translate into VHDL.

We present the design of a parallel synchronous hardware component from a purely functional description of its behaviour. Starting from an abstract specification of a linear time-invariant (LTI) system in Event-B a pipelined implementation is developed. The presented approach is applicable to LTI systems that can be represented as linear constant-coefficient difference equations. Scheduling and allocation can be conveniently expressed in the Event-B formalism.

We use the B formalism to derive functionally correct synchronous circuits. To represent the circuit we employ the hardware description language VHDL. This article outlines the development of a circuit design starting from an initial abstract functional specification of a system component. We discuss some topics involved in the translation to synthesisable VHDL and demonstrate the approach by way of an example.

We present the design of a parallel synchronous hardware component from a purely functional description of its behaviour. Starting from an abstract specification of a linear time-invariant (LTI) system in Event-B a pipelined implementation is developed. The presented approach is applicable to LTI systems that can be represented as linear constant-coefficient difference equations.

Stepwise refinement transforms an abstract specification into a more deterministic concrete specification. Ultimately one arrives at a specification that is implementable. At the various stages in the refinement process decisions are made that determine how the final implementation operates. Different implementations can be compared with respect to their expected performance within their environment. In this sense refinement poses an optimisation problem. We present a B-based language and a tool that can assist in solving this optimisation problem.

We introduce the probabilistic action system formalism which combines refinement with performance. Performance is expressed by means of probability and expected costs. Probability is needed to express uncertainty present in physical environments. Expected costs express physical or abstract quantities that describe a system. They encode the performance objective. The behaviour of probabilistic action systems is described by traces of expected costs. Corresponding notions of refinement and simulation-based proof rules are introduced. Formal notations like B or action systems support a notion of refinement. Refinement relates an abstract specification AA to a more deterministic concrete specification CC. Knowing AA and CC one proves CC refines, or implements, specification AA. In this study we consider specification AA as given and concern ourselves with a way to find a good candidate for implementation CC. To this end we classify all implementations of an abstract specification according to their performance. The performance of a specification AA is a value val.AA associated with some optimal behaviour it may exhibit. We distinguish performance from correctness. Concrete systems that do not meet the abstract specification are excluded. Only the remaining correct implementations CC are considered with respect to their performance. A good implementation of a specification is identified by having some optimal behaviour in common with it. In other words, a good refinement corresponds to a reduction of non-optimal behaviour. This also means that the abstract specification sets a boundary val.AA for the performance of any implementation. An implementation may perform worse than its specification but never better. Probabilistic action systems are based on discrete-time Markov decision processes. Numerical methods solving the optimisation problems posed by Markov decision processes are well-known, and used in a software tool that we have developed. The tool computes an optimal behaviour of a specification AA, and the associated value val.AA, thus assisting in the search for a good implementation CC. We present examples and case studies to demonstrate the use of probabilistic action systems.

Existing refinement frameworks such as B allow a developer to specify a system on an abstract level. Subsequently, this abstract specification is refined into an implementation that performs the specified task. In this paper a conventional refinement approach is extended with a means for performance analysis. This new approach guides a developer towards well-performing implementations throughout the refinement process. The main achievement of this work is an elaboration of a connection between performance and trace refinement.

CSP-Z ist eine Sprache zur Spezifikation zustandsbasierter kommunizierender Systeme, welche die Prozeßalgebra CSP und die Z-Notation zusammenführt. Die Semantik von CSP-Z-Spezifikationen wird durch das Failures/Divergences-Modell von CSP beschrieben, das von Roscoe angepaßt wurde, um unbeschränkten Nichtdetermismus besser behandeln zu können. Für CSP gibt es eine Verfeinerungstheorie, die auf dem Failures/Divergences-Modell basiert. Diese Theorie lässt sich in einfacher Weise auf CSP-Z übertragen. Ziel dieser Arbeit ist es die existierende Verfeinerungstheorie von Z für CSP-Z nutzbar zu machen. Mit Z können Datentypen prädikativ beschrieben werden, die nicht oder nur mit großem Aufwand zu implementieren sind. Doch bieten diese Datentypen den Vorteil, daß sie zu leichter verständlichen Spezifikationen führen, da bei starker Abstraktion viele für die Funktionalität des zu entwickelnden Programms unwesentliche Details wegfallen. Zu einem späteren Zeitpunkt werden jedoch besser implementierbare Datentypen benötigt. Es ist in Z möglich, einen (abstrakten) Datentypen durch einen anderen (konkreten) Datentypen zu ersetzen, so daß Programme, die bei Verwendung des abstrakten Datentypen korrekt waren, es auch bei Verwendung des konkreten Datentypen bleiben. Dieses Verfahren heißt Datenverfeinerung. Als Beweismethode zum Nachweis einer Datenverfeinerung dient die Simulation. Bis zu einem gewissen Grade lässt sich die Datenverfeinerungstheorie auch im Zusammenhang mit unsichtbaren Operationen verwenden, die durch Hiding entstehen. Es werden einige Regeln entwickelt, die auf den Regeln zur Datenverfeinerung in Z basieren und benutzt werden können, um Simulationsbeziehungen zwischen CSP-Z-Spezifikationen zu beweisen. Die Anwendung der entwickelten Regeln wird anhand kleinerer Fallstudien veranschaulicht.