Catálogo de publicaciones - libros

In this paper we use Z to capture the requirements for an ‘intuitive’ menu navigation system as a series of conjectures that should hold. We use those requirements to investigate potential algorithms. The Z formalisation enables the somewhat fuzzy requirement of ‘being intuitive’ to be captured precisely, analysed, and critiqued, leading to possibly new requirements, and more intuitive algorithms.

We present a prospective-value (pv) semantics for the Generalised Substitution Language. Whereas wp semantics captures the meaning of a computation in terms of the weakest precondition that must be fulfilled for a generalised substitution to establish any given postcondition , pv semantics expresses the meaning of a computation in terms of the value any expression would take were the computation to be carried out. To integrate non-termination we formulate improper bunch theory, an extended version of Hehner’s bunch theory where each type is augmented with an improper bunch. Algebraic simplification laws for the pv expression transformer are presented, and proved to be sound. Iteration is treated as a fixed-point in , and a corresponding theorem is presented allowing us to infer the pv effect of the while-loop construct.

An experiment to incorporate retrenchment into the B-Toolkit is described. The syntax of a retrenchment construct is given, as is the proof obligation which gives retrenchment its semantics. The practical aspects of incorporating these into the existing B-Toolkit are then investigated. It transpires that the B-Toolkit’s internal architecture is heavily committed to monolithic refinement, because of B-Method philosophy, and this restricts what can be done without a complete rebuild of the toolkit. Experience with case studies is outlined.

Since the early 90’s (after the seminal article of R. Back [4]), the refinement of stuttering steps [5] are performed by means of new actions (called here events) refining skip. It is shown in this article that such a refinement method is not always possible in the development of large systems. We shall instead use events refining some kind of non-deterministic actions maintaining the invariant (sometimes called keep). We show that such new refinements are completely safe. In a second part, we explain how such a mechanism can be used to express some reachability conditions that were otherwise expressed using some special temporal logic statements à la TLA [5] in a previous article [2]. Examples will be used to illustrate our proposals.

This paper presents a way to describe design patterns rigorously based on role concepts. Rigorous pattern descriptions are a key aspect for patterns to be used as rules for model evolution in the MDA context, for example. We formalize the role concepts commonly used in defining design patterns as a role metamodel using Object-Z. Given this role metamodel, individual design patterns are specified generically as a formal pattern role model using Object-Z. We also formalize the properties that must be captured in a class model when a design pattern is deployed. These properties are defined generically in terms of role bindings from a pattern role model to a class model. Our work provides a precise but abstract approach for pattern definition and also provides a precise basis for checking the validity of pattern usage in designs.

There is significant interest in the use of Z in conjunction with object-orientation. Here we present a new approach to structuring Z specifications in an object-oriented (OO) style. Our structuring is based on views, it uses the schema calculus, and it does not extend Z. The resulting OO Z specifications are comprehensible, modular, and conceptually clear. The modularity of the new approach supports a template-instantiation approach to expressing OO models in Z; practical formal verification and validation of the model can be undertaken using meta-proof, meta-lemmas, and formal snapshots.

We present a new methodology that permits to reuse an existing hardware component that has not been developed within the B framework while maintaining a correct design flow. It consists of writing a specification of the component in B and proving that the VHDL description of the component implements the specification using the ACL2 system. This paper focuses on the translation of the B specification into ACL2.

In this paper, we present a method and a tool to build symbolic labelled transition systems from specifications. The tool, called GeneSyst, can take into account refinement levels and can visualize the decomposition of abstract states in concrete hierarchical states. The resulting symbolic transition system represents all the behaviors of the initial event system. So, it can be used to reason about them. We illustrate the use of GeneSyst to check security properties on a model of electronic purse.

We have identified a type flaw attack on the Amended Needham Schroeder Protocol with Conventional Keys due to a potential oversight at the presentation layer of the network architecture. Using Object-Z, a formal specification of the protocol is presented allowing us to state the assumed properties of the presentation layer explicitly. Object-Z’s schema calculus is used to verify the attack we have found and the weaknesses upon which the attack depends, thus enabling us to minimise the effort required to prevent the attack and to specify this as part of the model accordingly.

In this article we would like to go back on B used to design software, by presenting the industrial process established through years by Siemens Transportation Systems on a real project: the VAL shuttle for Roissy Charles de Gaulle airport. In this project, the logical core of an equipment located along the tracks and driving the shuttles is designed with B.

By confronting this B software development, with the historical context, we show that B can be used as a high-level programming language offering the feature of proving properties. We show how this process is used to build, by construction, a large size software with very few design errors ever since its first release, and for a predefined cost.