Integrated Formal Methods: Third International Conference, IFM 2002, Turku, Finland, May 15-18, 2002. Proceedings.

Front Cover
Michael Butler, Luigia Petre, Kaisa Sere
Springer Science & Business Media, May 2, 2002 - Computers - 401 pages
The third in a series of international conferences on Integrated Formal Methods, IFM 2002, was held in Turku, Finland, May 15–17, 2002. Turku, situated in the south western corner of the country, is the former capital of Finland. The ? conference was organized jointly by Abo Akademi University and Turku Centre for Computer Science. The theme of IFM 1999 was the integration of state and behavioral based formalisms. For IFM 2000 this was widened to include all aspects pertaining to the integration of formal methods and formal notations. One of the goals of IFM 2002 was to further investigate these themes. Moreover, IFM 2002 explored the relations between formal methods and graphical notations, especially the industrialstandardlanguageforsoftwaredesign,theUni?edModelingLanguage (UML). The themes of IFM 2002 re?ect what we believe is a growing trend in the Formal Methods and Software Engineering research communities. Over the last threedecades,computerscientistshavedevelopedarangeofformalismsfocusing on particular aspects of behavior or analysis, such as sequential program str- tures,concurrentprogramstructures,dataandinformationstructures,temporal reasoning, deductive proof, and model checking. Much e?ort is now being - voted to integrating these methods in order to combine their advantages and ensure they scale up to industrial needs. Graphical notations are now widely used in software engineering and there is growing recognition of the importance ofprovidingthesewiththeformalunderpinningsandformalanalysiscapabilities found in formal methods.
 

Contents

A Complete LifeCycle ModelBased Development System
1
An Integrated Semantics for UML Class Object and State Diagrams Based on Graph Transformation
11
Stochastic Process Algebras Meet Eden
29
From Implicit Specifications to Explicit Designs in Reactive System Development
49
Integrated Approach for Design Specification and Verification of Distributed Systems
69
AssumeGuarantee Algorithms for Automatic Detection of Software Failures
89
Contributions for Modelling UML StateCharts in B
109
Translating Statecharts to B
128
Refinement in ObjectZ and CSP
225
Combining Specification Techniques for Processes Data and Time
245
An Integration of RealTime ObjectZ and CSP for Specifying Concurrent RealTime Systems
267
Model Driven Engineering
286
The Design of a ToolSupported Graphical Notation for Timed CSP
299
Combining Graphical and Formal Development of Open Distributed Systems
319
Translations between Textual Transition Systems and Petri Nets
339
Specification and Proof of Liveness Properties under Fairness Assumptions in B Event Systems
360

A Framework for Translating Models and Specifications
145
Model Checking ObjectZ Using ASM
165
Formalization of Cadence SPW FixedPoint Arithmetic in HOL
185
Formally Linking MDG and HOL Based on a Verified MDG System
205
Minimally and Maximally Abstract Retrenchments
380
Author Index
400
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information