Integrated Formal Methods: Third International Conference, IFM 2002, Turku, Finland, May 15-18, 2002. Proceedings.Michael Butler, Luigia Petre, Kaisa Sere 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 |
400 | |
Other editions - View all
Integrated Formal Methods: Third International Conference, IFM 2002, Turku ... Michael Butler,Luigia Petre,Kaisa Sere No preview available - 2002 |
Integrated Formal Methods: Third International Conference, IFM 2002, Turku ... Michael Butler,Luigia Petre,Kaisa Sere No preview available - 2002 |
Common terms and phrases
A/G lists abstract machine actions algorithms approach assigned basic behavior boolean C.A.R. Hoare channel class diagram client communication components composition Computer Science concurrent construct corresponding data servers deferred events defined denotes DriveThrough example execution expressed external failures finite fixed-point arithmetic fixed-point numbers floating-point Formal Methods function graph transformation graphical notation holds identified IEEE implementation init initial input integration interface invariant Isvalid liveness properties LNCS mapping MDG-HDL model checking Modeling Language module object object diagram Object-Z Object-Z classes operations output OZ-ASM parameters Petri net PHIL PN-class PN-transition portmapper predicate process algebra program counter proof obligations prove real-time refinement relation result retrenchment Section semantics sequence simulation rules Software SoftwareBus specification language Springer-Verlag statecharts structure synchronization syntax target TCSP textual tion transition system translation TTS-transition Unified Modeling Language Univ user applications variables verification