Sciweavers

ZUM
2000
Springer
14 years 4 months ago
Type-Constrained Generics for Z
We propose an extension to Z whereby generic parameters may have their types partially constrained. Using this mechanism it becomes possible to dene in Z much of its own schema cal...
Samuel H. Valentine, Ian Toyn, Susan Stepney, Stev...
ZUM
2000
Springer
107views Formal Methods» more  ZUM 2000»
14 years 4 months ago
How to Drive a B Machine
The B-Method is a state-based formal method that describes behaviour in terms of MACHINES whose states change under OPERATIONS. The process algebra CSP is an event-based formalism ...
Helen Treharne, Steve Schneider
ZUM
2000
Springer
14 years 4 months ago
Typechecking Z
Abstract. This paper presents some of our requirements for a Z typechecker: that the typechecker accept all well-typeable formulations, however contrived; that it gather informatio...
Ian Toyn, Samuel H. Valentine, Susan Stepney, Stev...
ZUM
2000
Springer
14 years 4 months ago
Formal Methods for Industrial Products
We have recently completed the specication and security proof of a large, industrial scale application. The application is security critical, and the modelling and proof were done ...
Susan Stepney, David Cooper
ZUM
2000
Springer
14 years 4 months ago
Recursive Schema Definitions in Object-Z
Unlike Z, Object-Z allows schemas to be defined recursively. This enables mutual and self recursive structures, commonly occurring in object-oriented programs, to be readily specif...
Graeme Smith
ZUM
2000
Springer
14 years 4 months ago
Playing with Abstraction and Refinement for Managing Features Interactions
with abstraction and refinement for managing features interactions A methodological approach to feature interaction problem Dominique Cansell and Dominique M
Dominique Cansell, Dominique Méry
ZUM
2000
Springer
14 years 4 months ago
A Computation Model for Z Based on Concurrent Constraint Resolution
We present a computation model for Z, which is based on a reduction to a small calculus, called Z, and on concurrent constraint resolution techniques applied for computing in thi...
Wolfgang Grieskamp
ZUM
2000
Springer
14 years 4 months ago
Retrenchment, Refinement, and Simulation
: Retrenchment is introduced as a liberalisation of refinement intended to address some of the shortcomings of refinement as sole means of progressing from simple abstract models t...
Richard Banach, Michael Poppleton
ZUM
2000
Springer
101views Formal Methods» more  ZUM 2000»
14 years 4 months ago
Analysis of Compiled Code: A Prototype Formal Model
Abstract. This paper reports on an experimental application of formal specification to inform analysis of compiled code. The analyses with are concerned attempt to recover abstract...
R. D. Arthan
ZUM
2000
Springer
14 years 4 months ago
Segregation with Communication
We have developed a general denition of segregation in the context of Z system specications. This denition is general enough to allow multi-way communications between otherwise seg...
David Cooper, Susan Stepney