Catálogo de publicaciones - libros

In earlier work, we introduced probability to the by providing a probabilistic choice substitution and by extending ’s semantics to incorporate its meaning [8]. This, a first step, allowed probabilistic programs to be written and reasoned about within .

This paper extends the previous work into refinement within . To allow probabilistic and within , we must add a probabilistic substitution; and we must determine the rules and techniques for its rigorous refinement into probabilistic code.

Implementation in frequently contains loops. We generalise the standard proof obligation rules for loops giving a set of rules for reasoning about the correctness of probabilistic loops. We present a small case-study that uses those rules, the randomised Min-Cut algorithm.

We describe a method for combining formal program development with a disciplined and documented way of introducing realistic compromises, for example necessitated by resource bounds. Idealistic specifications are identified with the limits of sequences of more “realistic” specifications, and such sequences can then be refined in their entirety. Compromises amount to focusing the attention on a particular element of the sequence instead of the sequence as a whole.

This method addresses the problem that initial formal specifications can be abstract or complete but rarely both. Various potential application areas are sketched, some illustrated with examples. Key research issues are found in identifying metric spaces and properties that make them usable for refinement using approximations.

It is well known that the principal operators in the Z schema calculus are not monotonic with respect to either operation or data refinement. This is generally regarded as limiting their usefulness in software development, and has lead to proposals to redefine the schema calculus and/or the notion of refinement so that monotonicity is established. We examine this issue more closely, to demonstrate just how non-monotonicity arises, and identify various conditions under which components of schema expressions can be safely replaced by their refinements. This shows that in a wide range of practical situations, refinement of such components can be justified by checking fairly simple conditions.

Slicing is the activity of reducing a program or a specification with respect to a given condition (the slicing criterion) such that the condition holds on the full program if and only if it holds on the reduced program. Originating from program analysis the entity to be sliced is usually a program and the slicing criterion a value of a variable at a certain program point. In this paper we present an approach to slicing Object-Z specifications with temporal logic formulae as slicing criteria and show the correctness of our approach. The underlying motivation is the goal to substantially reduce the size of the specification and subsequently facilitate verification of temporal logic properties.

This paper presents a solution to the lack of tool-support for the JML models verification. We propose an approach for expressing JML specifications within the B abstract machines notation. The B machines generated from the JML can then be checked to ensure their correctness. Thus, we deduce the correctness of the original JML specification, ensured by rewriting rules which give the semantical equivalence of the two models. More generally, this translation can be applied to object-oriented specification languages using before-after predicates.

For any sort of computer system, the problems of being sure you have asked for the right thing and then being sure you are implementing the right thing are important and hard problems. For systems with a graphical user interface there are the analogous additional problems of making sure that the interface allows any interaction that is required, and works in a usable way. Design guidelines are used in both the design and evaluation of user interfaces to try and ensure that the systems we build are both usable and conform to specific requirements. This paper discusses practical ways in which we can use formal methods to model guidelines for interface design and then use these as a basis for the formal proof that a specified system has the desired properties described in the guidelines.

Web-based applications are the most common form of distributed systems that have gained a lot of attention in the past ten years. Today many of us are relying on scores of mission-critical Web-based systems in different areas such as banking, finance, e-commerce and government. The development process of these systems needs a sound methodology, which ensures quality, consistency and integrity. Formal Methods provide systematic and quantifiable approaches to create coherent systems. Despite this there has been limited work on the formal modelling of Web-based applications. In this paper our aim is to provide researchers with some guidelines based on results from ongoing work to model a Web-based system using the B-Method. Session and state management, developing formal models for complex data types, abstraction of distributed database systems and formal representation of communication links between different components of a web-based system are the main issues that we have examined.