This book constitutes the refereed proceedings of the Second International Conference on Integrated Formal Methods, IFM 2000, held in Dagstuhl, Germany in November 2000.
The 22 revised full papers presented together with the abstracts of two invited talks were carefully reviewed and selected from 58 submissions. The papers are grouped together in topical sections on linking and extending notations, methodology, foundation of one formalism by another, semantics, and verification and validation.
Author(s): Tony Hoare (auth.), Wolfgang Grieskamp, Thomas Santen, Bill Stoddart (eds.)
Series: Lecture Notes in Computer Science 1945
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2000
Language: English
Pages: 446
Tags: Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Software Engineering; Programming Techniques
Assertions....Pages 1-2
State-Based Extension of CASL....Pages 3-24
Linking DC Together with TRSL....Pages 25-44
Formalizing Timing Diagrams as Causal Dependencies for Verification Purposes....Pages 45-60
A Process Compensation Language....Pages 61-76
Activity Graphs and Processes....Pages 77-96
Structuring Real-Time Object-Z Specifications....Pages 97-115
ISpec: Towards Practical and Sound Interface Specifications....Pages 116-135
Cooperation of Formal Methods in an Engineering Based Software Development Process....Pages 136-155
Developing Control Systems Components....Pages 156-175
Specification and Analysis of Automata-Based Designs....Pages 176-193
Structural Refinement in Object-Z / CSP....Pages 194-213
Towards a Unified Development Methodology for Shared-Variable Parallel and Distributed Programs....Pages 214-234
Construction of Finite Labelled Transition Systems from B Abstract Systems....Pages 235-254
μ-Charts and Z: Hows, Whys, and Wherefores....Pages 255-276
Combining Operational Semantics, Logic Programming and Literate Programming in the Specification and Animation of the Verilog Hardware Description Language....Pages 277-296
Why Doesn’t Anyone Use Formal Methods?....Pages 297-298
How to Write a Healthiness Condition....Pages 299-317
A Concurrent and Compositional Petri Net Semantics of Preemption....Pages 318-337
An Approach to Symbolic Test Generation....Pages 338-357
Behavioral Conformance Verification in an Integrated Approach Using UML and B....Pages 358-379
Predicate Diagrams for the Verification of Reactive Systems....Pages 380-397
Modular Verification for a Class of PLTL Properties....Pages 398-419
Towards Model Checking Stochastic Process Algebra....Pages 420-439
