Formal Specification and Documentation using Z: A Case Study Approach

Formal Specification and Documentation using Z: A Case Study Approach

Presents a pragmatic view of the use of formal methods, that it can still be beneficial (and is much more cost effective in general) than attempting proofs in many cases.

Publication date: 01 Feb 1996

ISBN-10: 1850322309

ISBN-13: 9781850322306

Paperback: 315 pages

Views: 27,214

Type: N/A

Publisher: Thomson Publishing

License: n/a

Post time: 11 Jun 2005 08:27:28

Formal Specification and Documentation using Z: A Case Study Approach

Formal Specification and Documentation using Z: A Case Study Approach Presents a pragmatic view of the use of formal methods, that it can still be beneficial (and is much more cost effective in general) than attempting proofs in many cases.
Tag(s): Formal Methods
Publication date: 01 Feb 1996
ISBN-10: 1850322309
ISBN-13: 9781850322306
Paperback: 315 pages
Views: 27,214
Document Type: N/A
Publisher: Thomson Publishing
License: n/a
Post time: 11 Jun 2005 08:27:28
:santagrin: This book was suggested by jpbowen

Book excerpts:

Formal methods are becoming more accepted in both academia and industry as one possible way in which to help improve the quality of both software and hardware systems. It should be remembered however that they are not a panacea, but rather one more weapon in the armoury against making design mistakes. Thus one should not expect too much from formal methods, but rather use them to advantage where appropriate.

This book presents an even more pragmatic view of the use of formal methods than that held by some academics: that is that formal specification alone can still be beneficial (and is much more cost effective in general) than attempting proofs in many cases. While the cost of proving a system correct may be justified in safety-critical systems where lives are at risk, many systems are less critical, but could still benefit from formalization earlier on in the design process than is normally the case in much industrial practice.

This book presents the use of one notation in the accumulation of available mathematical techniques to help ensure the correctness of computer-based systems, namely the Z notation (pronounced 'zed'), intended for the specification of such systems. The formal notation Z is based on set theory and predicate calculus, and has been developed at the Oxford University Computing Laboratory since the late 1970?s.

The use of a formal notation early on in the design process helps to remove many errors that would not otherwise be discovered until a later stage. The book includes specification of a number of digital systems in a variety of areas to help demonstrate the scope of the notation. Most of the specifications are of real systems that have been built, either commercially or experimentally. It is hoped that the variety of examples in this book will encourage more developers to attempt to specify their systems in a more formal manner before they attempt the development or programming stage.

It is hoped that the specifications presented here will help students and industrial practitioners alike to produce better specifications of their designs, be they large or small. Even if no proofs or refinement of a system are attempted, mere formalization early on in the design process will help to clarify a designer?s thoughts (especially when undertaken as part of a team) and remove many errors before they become implemented, and therefore much more difficult and expensive to rectify.
 




About The Author(s)


Jonathan Bowen, FBCS FRSA, is Chairman of Museophile Limited (founded in 2002) and an Emeritus Professor at London South Bank University, where he established and headed the Centre for Applied Formal Methods in 2000.

He has been involved with the field of computing in both industry (including Marconi Instruments, Logica, Silicon Graphics Inc., and Praxis) and academia since 1977. His interests have ranged from formal methods, safety-critical systems, the Z notation, provably correct systems, rapid prototyping using logic programming, decompilation, hardware compilation, software/hardware co-design, linking semantics, and software testing, to the history of computing, on-line museums, and virtual communities.

Jonathan Bowen

Jonathan Bowen, FBCS FRSA, is Chairman of Museophile Limited (founded in 2002) and an Emeritus Professor at London South Bank University, where he established and headed the Centre for Applied Formal Methods in 2000.

He has been involved with the field of computing in both industry (including Marconi Instruments, Logica, Silicon Graphics Inc., and Praxis) and academia since 1977. His interests have ranged from formal methods, safety-critical systems, the Z notation, provably correct systems, rapid prototyping using logic programming, decompilation, hardware compilation, software/hardware co-design, linking semantics, and software testing, to the history of computing, on-line museums, and virtual communities.


Book Categories
Sponsors