ZUM
2005
Springer
14 years 5 months ago
2005
Springer
Abstract. 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 ļ¬...
ZUM
2005
Springer
14 years 5 months ago
2005
Springer
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 investiga...
ZUM
2005
Springer
14 years 5 months ago
2005
Springer
Abstract. 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 o...
ZUM
2005
Springer
14 years 5 months ago
2005
Springer
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, typechecki...
ZUM
2005
Springer
14 years 5 months ago
2005
Springer
Abstract. We describe a method for combining formal program development with a disciplined and documented way of introducing realistic compromises, for example necessitated by reso...
ZUM
2005
Springer
14 years 5 months ago
2005
Springer
ZUM
2005
Springer
14 years 5 months ago
2005
Springer
There is signiļ¬cant interest in the use of Z in conjunction with object-orientation. Here we present a new approach to structuring Z speciļ¬cations in an object-oriented (OO) st...
SIGADA
2005
Springer
14 years 5 months ago
2005
Springer
The purpose of this research paper is to examine (1) why formal methods are required for software systems today; (2) the Praxis High Integrity Systemsā Correctness-by-Constructi...
SAS
2005
Springer
14 years 5 months ago
2005
Springer
The termination insensitive secure information ļ¬ow problem can be reduced to solving a safety problem via a simple program transformation. Barthe, DāArgenio, and Rezk coined th...
SAS
2005
Springer
14 years 5 months ago
2005
Springer
We show that the idea of predicates on heap objects can be cast in the framework of predicate abstraction. This leads to an alternative view on the underlying concepts of three-val...