Catálogo de publicaciones - libros
ZB 2005: Formal Specification and Development in Z and B: 4th International Conference of B and Z Users, Guildford, UK, April 13-15, 2005, Proceedings
Helen Treharne ; Steve King ; Martin Henson ; Steve Schneider (eds.)
En conferencia: 4º International Conference of B and Z Users (ZB) . Guildford, UK . April 13, 2005 - April 15, 2005
Resumen/Descripción – provisto por la editorial
No disponible.
Palabras clave – provistas por la editorial
Theory of Computation; Software Engineering; Logics and Meanings of Programs; Mathematical Logic and Formal Languages
Disponibilidad
Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
---|---|---|---|---|
No detectada | 2005 | SpringerLink |
Información
Tipo de recurso:
libros
ISBN impreso
978-3-540-25559-8
ISBN electrónico
978-3-540-32007-4
Editor responsable
Springer Nature
País de edición
Reino Unido
Fecha de publicación
2005
Información sobre derechos de publicación
© Springer-Verlag Berlin Heidelberg 2005
Cobertura temática
Tabla de contenidos
doi: 10.1007/11415787_1
Specification Before Satisfaction: The Case for Research into Obtaining the Right Specification
Cliff B. Jones
Model-oriented specification techniques like VDM [Jon80,Jon90], Z [Hay93] and B [Abr96] have an enormous amount in common (cf. [Hay92,HJN94]). Among other things that this formal methods community shares is the view that one can start with a formal specification and show that a design/implementation satisfies that specification. It is however obvious that, if a specification does not actually reflect the real need, proving a program correct with respect to it is somewhat pointless.
Pp. 1-5
doi: 10.1007/11415787_2
Visualising Larger State Spaces in P
Michael Leuschel; Edd Turner
is an animator and model checker for the B method. It also allows to visualise the state space of a B machine in graphical way. This is often very useful and allows users to quickly spot whether the machine behaves as expected. However, for larger state spaces the visualisation quickly becomes difficult to grasp by users (and the computation of the graph layout takes considerable time). In this paper we present two relatively simple algorithms to often considerably reduce the complexity of the graphs, while still keeping relevant information. This makes it possible to visualise much larger state spaces and gives the user immediate feedback about the overall behaviour of a machine. The algorithms have been implemented within the toolset and we highlight their potential on several examples. We also conduct a thorough experimentation of the algorithm on 47 B machines and analyse the results.
Pp. 6-23
doi: 10.1007/11415787_3
Non-atomic Refinement in Z and CSP
John Derrick; Heike Wehrheim
In this paper we discuss the relationship between notions of non-atomic (or action) refinement in a state-based setting with that in a behavioural setting. In particular, we show that the definition of non-atomic coupled downward simulation as defined for Z and Object-Z is sound with respect to an action refinement definition of CSP failures refinement.
Pp. 24-44
doi: 10.1007/11415787_4
Process Refinement in B
Steve Dunne; Stacey Conroy
We describe various necessary and sufficient conditions with which to augment B’s existing refinement proof obligations for forward and backward refinement in order to capture within the B Method a variety of CSP process refinement relations, including most significantly that of failures-divergences which provides the standard denotational semantics of CSP processes.
Pp. 45-64
doi: 10.1007/11415787_5
CZT: A Framework for Z Tools
Petra Malik; Mark Utting
The Community Z Tools (CZT) project is an open-source Java framework for building formal methods tools for Z and Z dialects. It also includes a set of tools for parsing, typechecking, transforming and printing standard Z specifications in LATEX, Unicode or XML formats. This paper gives an overview of the CZT framework, including an introduction to its visitor design pattern that makes it possible to write new Z transformation tools in just a few lines of Java code. The paper also discusses several problems and challenges that arose when attempting to build tools based on the SO Standard for Z.
Pp. 65-84
doi: 10.1007/11415787_6
Model Checking Z Specifications Using SAL
Graeme Smith; Luke Wildman
The Symbolic Analysis Laboratory (SAL) is a suite of tools for analysis of state transition systems. Tools supported include a simulator and four temporal logic model checkers. The common input language to these tools was originally developed with translation from other languages, both programming and specification languages, in mind. It is, therefore, a rich language supporting a range of type definitions and expressions. In this paper, we investigate the translation of Z specifications into the SAL language as a means of providing model checking support for Z. This is facilitated by a library of SAL definitions encoding the Z mathematical toolkit.
Pp. 85-103
doi: 10.1007/11415787_7
Proving Properties of Stateflow Models Using ISO Standard Z and CADiZ
Ian Toyn; Andy Galloway
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 Simulink/Stateflow Analyser tool does in support of the Practical Formal Specification method. The tool aims to automate the formal validations of the method, so that users of Simulink/Stateflow can benefit from them. The Z exploits some notations that are particular to ISO Standard Z. The automation is aided by quite terse tactics interpreted by CADiZ.
Pp. 104-123
doi: 10.1007/11415787_8
A Stepwise Development of the Peterson’s Mutual Exclusion Algorithm Using B Abstract Systems
J. Christian Attiogbé
We present a stepwise formal development of the Peterson’s mutual exclusion algorithm using Event B. We use a bottom-up approach where we introduce the parallel composition of subsystems which are separately specified. First, we specify subsystems as B abstract systems; then we compose the subsystems to get a first abstract solution for the mutual exclusion. This solution is improved to obtain the Peterson’s algorithm. This is achieved by refinement and composition of the former abstract subsystems. Therefore the result is formally proved on the basis of correctness (safety) properties added to the invariant. Atelier B (a B prover) is used to check completely the development.
Pp. 124-141
doi: 10.1007/11415787_9
An Extension of Event B for Developing Grid Systems
Pontus Boström; Marina Waldén
Computational grids have become widespread in organizations for handling their need for computational resources and the vast amount of available information. Grid systems, and other distributed systems, are often complex and formal reasoning about them is needed, in order to ensure their correctness and to structure their development. Event B is a formal method with tool support that is meant for stepwise development of distributed systems. To facilitate the implementation of grid systems we here propose extensions to Event B that take grid specific features into account. We add new constructs to model the client-server architecture of grid systems, as well as important features like communication and synchronisation. We introduce the extensions in such a manner that the necessary proof obligations are automatically generated and the system can be implemented in a straightforward manner.
Pp. 142-161
doi: 10.1007/11415787_10
The Challenge of Probabilistic
Carroll Morgan; Thai Son Hoang; Jean-Raymond Abrial
Among the many opportunities offered by computational semantics for probability, the challenge of probabilistic Event B () is one of the most attractive.
The method itself is now almost 20 years old, and has been much improved and adapted over that time by the many projects to which it has been applied, and by its philosophy —right from the start— that it must be practical, effective and amenable to tool support.; more recently, has extended it and altered its style of use. The probabilistic-program semantics we appeal to is even older (in Kozen’s original form), but has only recently been “revived” in the context of -style abstraction and refinement.
The especial attraction of putting the two together is the likely interplay between the probabilistic theory, on the one hand, and the decades of practical experience that have by now been built-in to the approach, on the other.
In particular, there are areas where a full theoretical treatment of probability, concurrency, abstraction and refinement —all at once— seems prohibitively complex; and yet in practice either the complexities seldom occur, or the exigencies of ’s having been so-often applied to real, non-toy problems has forced it to evolve styles for avoiding such complexities. In short, we want to use (event) to guide us towards the issues that truly are important.
Rabin’s is used as a motivating case study.
Pp. 162-171