Integrated Formal Methods: 4th International Conference, IFM 2004, Cnaterbury, UK, April 4-7, 2004. Proceedings

Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani (auth.), Eerke A. Boiten, John Derrick, Graeme Smith (eds.)3540213775, 9783540213772, 9783540247562

The fourth conference in the series of international meetings on Integrated F- mal Methods, IFM, was held in Canterbury, UK, 4–7 April 2004. The conference was organized by the Computing Laboratory at the University of Kent, whose main campus is just outside the ancient town of Canterbury, part of the county of Kent. Kent is situated in the southeast of England, and the university sits on a hill overlooking the city of Canterbury and its world-renowned cathedral. The UniversityofKentwasgranteditsRoyalCharterin1965.Todaytherearealmost 10,000 full-time and part-time students, with over 110 nationalities represented. The IFM meetings have proven to be particularly successful. The ?rst m- ting was held in York in 1999, and subsequently we held events in Germany in 2000, and then Finland in 2002. The conferences are held every 18 months or so, and attract a wide range of participants from Europe, the Americas, Asia and Australia. The conference is now ?rmly part of the formal methods conference calendar. The conference has also evolved in terms of themes and subjects – presented, and this year, in line with the subject as a whole, we saw more work on veri?cation as some of the challenges in this subject are being met. The work reported at IFM conferences can be seen as part of the attempt to manage complexity by combining paradigms of speci?cation and design, so that the most appropriate design tools are used at di?erent points in the life-cycle.

---

Table of contents :
Front Matter….Pages –
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft….Pages 1-20
Design Verification for Control Engineering….Pages 21-35
Integrating Model Checking and Theorem Proving in a Reflective Functional Language….Pages 36-39
A Tutorial Introduction to Designs in Unifying Theories of Programming….Pages 40-66
An Integration of Program Analysis and Automated Theorem Proving….Pages 67-86
Verifying Controlled Components….Pages 87-107
Efficient CSP Z Data Abstraction….Pages 108-127
State/Event-Based Software Model Checking….Pages 128-147
Formalising Behaviour Trees with CSP….Pages 148-167
Generating MSCs from an Integrated Formal Specification Language….Pages 168-186
UML to B: Formal Verification of Object-Oriented Models….Pages 187-206
Software Verification with Integrated Data Type Refinement for Integer Arithmetic….Pages 207-226
Constituent Elements of a Correctness-Preserving UML Design Approach….Pages 227-246
Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption….Pages 247-266
Linking CSP-OZ with UML and Java: A Case Study….Pages 267-286
Object-Oriented Modelling with High-Level Modular Petri Nets….Pages 287-306
Specification and Verification of Synchronizing Concurrent Objects….Pages 307-327
Understanding Object-Z Operations as Generalised Substitutions….Pages 328-342
Embeddings of Hybrid Automata in Process Algebra….Pages 343-362
An Optimal Approach to Hardware/Software Partitioning for Synchronous Model….Pages 363-381
A Many-Valued Logic with Imperative Semantics for Incremental Specification of Timed Models….Pages 382-401
Integrating Temporal Logics….Pages 402-420
Integration of Specification Languages Using Viewpoints….Pages 421-440
Integrating Formal Methods by Unifying Abstractions….Pages 441-460
Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors….Pages 461-480
Using UML Sequence Diagrams as the Basis for a Formal Test Description Language….Pages 481-500
Viewpoint-Based Testing of Concurrent Components….Pages 501-520
A Method for Compiling and Executing Expressive Assertions….Pages 521-540
Back Matter….Pages –