The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
The Event Calculus is a model of communicating state machines which is defined in Z. The machines have a number of behavioural states, which can be represented in diagrammatic form, and have data states which can be described with Z data base schemas. Machines change state on the occurrence of an “event”. A diagrammatic notation is used in which each transition may be labelled with an event together...
Large Z specifications require testing if they are to be at all credible and translation to Prolog provides one means of doing this. Experience with PiZA (Prolog Z Animator), a system designed to carry out this translation automatically, is described. The paper gives a brief description of the principles of the translation with some practical details of using PiZA. Experience in animating large specifications...
We use a structure preserving encoding of Z in the higher-order logic instance of the generic theorem prover Isabelle to derive test cases from Z specifications. This work shows how advanced theorem provers can be used with little effort to provide tool support for Z beyond mere type-checking. Experience with a non-trivial example shows that modular reasoning according to the structure of a specification...
We describe the Z/EVES system, which allows Z specifications to be analysed in a number of different ways. Among the significant features of Z/EVES are domain checking, which ensures that a specification is meaningful, and a theorem prover that includes a decision procedure for simple arithmetic and a heuristic rewriting mechanism that recognizes “obvious” facts.
We present a new formal OO method, called $$\mathcal{F}\mathcal{O}\mathcal{X}$$ , which is a synergetic combination of the semi-formal Fusion method and the formal specification language Object-Z. To manage complexity and to foster separation of concerns, $$\mathcal{F}\mathcal{O}\mathcal{X}$$ distinguishes between analysis and design. In each phase structure and behaviour specifications...
An early version of the Z Standard included the deductive system W for reasoning about Z specifications. Later versions contain a different deductive system. In this paper we sketch a proof that W is relatively sound with respect to this new deductive system. We do this by demonstrating a semantic basis for a correspondence between the two systems, then showing that each of the inference rules of...
We demonstrate how the rippling heuristic [Bundy et al 93], originally developed for inductive proofs, can be used to automate set membership proofs. Set membership proofs occur frequently as subgoals in Z proofs, and automating these goals would lift a significant burden of the proof off of users of proof tools. The approach is promising and is being integrated into the proof tool Z-in-Isabelle [Kraan...
We describe a method for rigorously specifying and verifying the control of pipelined microprocessors which can be used by the hardware designer for a precise documentation and justification of the correctness of his design techniques. We proceed by successively refining a one-instruction-at-a-time-view of a RISC processor to a description of its pipelined implementation; the structure of the refinement...
This paper presents work performed in the EPSRC “Object-oriented Specification of Reactive and Real-time Systems” project. It aims to provide formal design methods for real-time systems, using a combination of the VDM++ formal method and the HRT-HOOD method. We identify refinement steps for hard real-time systems in VDM++, together with a case study of a mine-pump control system, involving...
In this paper, we describe an approach to the design of distributed systems with B AMN. The approach is based on the action-system formalism which provides a framework for developing state-based parallel reactive systems. More specifically, we use the so-called CSP approach to action systems in which interaction between subsystems is by synchronised message passing and there is no sharing of state...
This paper describes techniques for specifying and designing reactive systems in the B Abstract Machine (AMN) language, using concepts from procedural process control. In addition, we consider what forms of concurrent extensions to B AMN would make it more effective in representing such systems.
This paper provides a formal specification in Z of a new intelligent hypertext model called the soft-link hypertext model (SLHM). This model has been implemented and extensively tested, and provides a new methodology for constructing the future generation of information retrieval systems. Its core is the adoption of a data structure called the conceptual index, which allows hypertext structure to...
We are developing a control program for a unique radiation therapy machine. The program is safety-critical, executes several concurrent tasks, and must meet real-time deadlines. Development employs both formal and traditional methods: we produce an informal specification in prose (supplemented by tables, diagrams and a few formulas) and a formal description in Z. The Z description includes an abstract...
In this paper we report on a research project in which the user interface for a research nuclear reactor was specified using a combination of formal notations. The goal of the project was to evaluate the use of a combination of techniques and to assess their utility in specifying a user interface for a non-trivial safety-critical application. We conclude that the techniques worked well and scale up...
Architectural styles have been introduced in [1] in order to classify and analyze software architectures. In that paper, Z was used as a notation to specify and study architectural styles, however some problems remained open concerning specification and analysis of their behavioral properties. We use a new operational semantics to describe and analyze an architectural style of distributed systems...
An important aspect in the specification of distributed systems is the role of the internal (or unobservable) operation. Such operations are not part of the user interface (i.e. the user cannot invoke them), however, they are essential to our understanding and correct modelling of the system. Various conventions have been employed to model internal operations when specifying distributed systems in...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.