Integrated Formal Methods

1. Front Matter

   PDF

2. Invited Talks

   1. SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft

      • Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani

      Pages 1-20

   2. Design Verification for Control Engineering

      • Richard J. Boulton, Hanne Gottliebsen, Ruth Hardy, Tom Kelsey, Ursula Martin

      Pages 21-35

   3. Integrating Model Checking and Theorem Proving in a Reflective Functional Language

      • Tom Melham

      Pages 36-39

3. Tutorial

   1. A Tutorial Introduction to Designs in Unifying Theories of Programming

      • Jim Woodcock, Ana Cavalcanti

      Pages 40-66

4. Contributed Papers

   1. An Integration of Program Analysis and Automated Theorem Proving

      • Bill J. Ellis, Andrew Ireland

      Pages 67-86

   2. Verifying Controlled Components

      • Steve Schneider, Helen Treharne

      Pages 87-107

   3. Efficient CSP _Z Data Abstraction

      • Adalberto Farias, Alexandre Mota, Augusto Sampaio

      Pages 108-127

   4. State/Event-Based Software Model Checking

      • Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha

      Pages 128-147

   5. Formalising Behaviour Trees with CSP

      • Kirsten Winter

      Pages 148-167

   6. Generating MSCs from an Integrated Formal Specification Language

      • Jin Song Dong, Shengchao Qin, Jun Sun

      Pages 168-186

   7. UML to B: Formal Verification of Object-Oriented Models

      • K. Lano, D. Clark, K. Androutsopoulos

      Pages 187-206

   8. Software Verification with Integrated Data Type Refinement for Integer Arithmetic

      • Bernhard Beckert, Steffen Schlager

      Pages 207-226

   9. Constituent Elements of a Correctness-Preserving UML Design Approach

      • Tiberiu Seceleanu, Juha Plosila

      Pages 227-246

   10. Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption

       • Xu Wang, A. W. Roscoe, R. S. Lazić

       Pages 247-266

   11. Linking CSP-OZ with UML and Java: A Case Study

       • Michael Möller, Ernst-Rüdiger Olderog, Holger Rasch, Heike Wehrheim

       Pages 267-286

   12. Object-Oriented Modelling with High-Level Modular Petri Nets

       • Cécile Bui Thanh, Hanna Klaudel

       Pages 287-306

   13. Specification and Verification of Synchronizing Concurrent Objects

       • Gabriel Ciobanu, Dorel Lucanu

       Pages 307-327

   14. Understanding Object-Z Operations as Generalised Substitutions

       • Steve Dunne

       Pages 328-342

   15. Embeddings of Hybrid Automata in Process Algebra

       • Tim A. C. Willemse

       Pages 343-362

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.

• Unified Modeling Language (UML)
• automata
• calculus
• component systems
• formal method
• formal methods
• logic
• model checking
• modeling
• object-oriented modeling
• process algebra
• program analysis
• programming
• refinement
• verification

• Computing Laboratory, University of Kent, Canterbury, Kent, UK

  Eerke A. Boiten

• Department of Computing, University of Sheffield, Sheffield, UK

  John Derrick

• School of Information Technology and Electrical Engineering, The University of Queensland, Australia

  Graeme Smith

Policies and ethics