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

Front Cover
Springer Science & Business Media, Mar 24, 2004 - Computers - 540 pages
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.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Selected pages

Contents

Technology Transfer of Formal Methods inside Microsoft
1
Design Verification for Control Engineering
21
Integrating Model Checking and Theorem Proving in a Reflective Functional Language
36
A Tutorial Introduction to Designs in Unifying Theories of Programming
40
An Integration of Program Analysis and Automated Theorem Proving
67
Verifying Controlled Components
87
Efficient CSPz Data Abstraction
108
StateEventBased Software Model Checking
128
ObjectOriented Modelling with HighLevel Modular Petri Nets
287
Specification and Verification of Synchronizing Concurrent Objects
307
Understanding ObjectZ Operations as Generalised Substitutions
328
Embeddings of Hybrid Automata in Process Algebra
343
An Optimal Approach to HardwareSoftware Partitioning for Synchronous Model
363
A ManyValued Logic with Imperative Semantics for Incremental Specification of Timed Models
382
Integrating Temporal Logics
402
Integration of Specification Languages Using Viewpoints
421

Formalising Behaviour Trees with CSP
148
Generating MSCs from an Integrated Formal Specification Language
168
Formal Verification of ObjectOriented Models
187
Software Verification with Integrated Data Type Refinement for Integer Arithmetic
207
Constituent Elements of a CorrectnessPreserving UML Design Approach
227
Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption
247
A Case Study
267
Integrating Formal Methods by Unifying Abstractions
441
A Case Study on Postcompletion Errors
461
Using UML Sequence Diagrams as the Basis for a Formal Test Description Language
481
ViewpointBased Testing of Concurrent Components
501
A Method for Compiling and Executing Expressive Assertions
521
Author Index
541
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information