1 In a number of recent presentations – most notably at FME’96 –oneofthe foremost scientists in the ?eld of formal methods, C.A.R. Hoare,has highlighted the fact that formal methods are not the only technique for producing reliable software. This seems to have caused some controversy,not least amongst formal methods practitioners. How can one of the founding fathers of formal methods seemingly denounce the ?eld of research after over a quarter of a century of support? This is a question that has been posed recently by some formal methods skeptics. However, Prof. Hoare has not abandoned formal methods. He is reiterating, 2 albeitmoreradically,his1987view thatmorethanonetoolandnotationwillbe requiredinthepractical,industrialdevelopmentoflarge-scalecomplexcomputer systems; and not all of these tools and notations will be, or even need be, formal in nature. Formalmethods arenotasolution,butratheroneofaselectionoftechniques that have proven to be useful in the development of reliable complex systems, and to result in hardware and software systems that can be produced on-time and within a budget, while satisfying the stated requirements. After almostthree decades,the time has come to view formalmethods in the context of overall industrial-scale system development, and their relationship to othertechniquesandmethods.Weshouldnolongerconsidertheissueofwhether we are “pro-formal” or “anti-formal”, but rather the degree of formality (if any) that we need to support in system development. This is a goal of ZUM’98, the 11th International Conference of Z Users, held for the ?rst time within continental Europe in the city of Berlin, Germany.
Author(s): Klaus Grimm (auth.), Jonathan P. Bowen, Andreas Fett, Michael G. Hinchey (eds.)
Series: Lecture Notes in Computer Science 1493
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1998
Language: English
Pages: 424
Tags: Software Engineering; Logics and Meanings of Programs; Programming Techniques; Mathematical Logic and Formal Languages
Front Matter....Pages -
Industrial Requirements for the Efficient Development of Reliable Embedded Systems....Pages 1-4
How to Combine Z with a Process Algebra....Pages 5-23
The Specification and Refinement of an Environmental Model....Pages 24-41
Formal Derivation of Finite State Machines for Class Testing....Pages 42-59
Using B to Specify, Verify and Design Hardware Circuits....Pages 60-65
Z on the Web Using Java....Pages 66-80
Visualizing Z Notation in HTML Documents....Pages 81-95
On the Semantic Relation of Z and HOL....Pages 96-115
HOL-Z in the UniForM-Workbench – A Case Study in Tool Integration for Z....Pages 116-134
Designing a Requirements Specification Language for Reactive Systems....Pages 135-135
Analyzing a Real-Time Program with Z....Pages 136-153
Recursive Definitions in Z....Pages 154-171
A Logic for the Schema Calculus....Pages 172-191
Combining Specification Techniques for Processes, Data and Time....Pages 192-192
Innovations in the Notation of Standard Z....Pages 193-213
Comparing Extended Z with a Heterogeneous Notation for Reasoning about Time and Space....Pages 214-232
Inconsistency and Undefinedness in Z – A Practical Guide....Pages 233-249
Compositional Specification of Controllers for Batch Process Operations....Pages 250-264
Testing Refinements by Refining Tests....Pages 265-283
More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement....Pages 284-307
Network Topology and a Case Study in TCOZ....Pages 308-327
Object-Oriented Specification of Hybrid Systems Using UML h and ZimOO....Pages 328-346
Translating the OMT Dynamic Model into Object-Z....Pages 347-366
Select Z Bibliography....Pages 367-406
Comp.specification.z and Z FORUM Frequently Asked Questions....Pages 407-416
Back Matter....Pages -
