𝔖 Scriptorium
✦   LIBER   ✦

πŸ“

Formal Methods and Software Engineering: 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003. Proceedings

✍ Scribed by Ian J. Hayes (auth.), Jin Song Dong, Jim Woodcock (eds.)


Publisher
Springer-Verlag Berlin Heidelberg
Year
2003
Tongue
English
Leaves
693
Series
Lecture Notes in Computer Science 2885
Edition
1
Category
Library

⬇  Acquire This Volume

No coin nor oath required. For personal study only.

✦ Synopsis


This volume contains the proceedings of the 2003 International Conference on Formal Engineering Methods (ICFEM 2003). The conference was the ?fth in a series that began in 1997. ICFEM 2003 was held in Singapore during 5–7 November 2003. ICFEM 2003 aimed to bring together researchers and practitioners from - dustry, academia, and government to advance the state of the art in formal engineering methods and to encourage a wider uptake of formal methods in industry. The Program Committee received 91 submissions from more than 20 co- tries in various regions. After each paper was reviewed by at least three referees in each relevant ?eld, 34 high-quality papers were accepted based on originality, technical content, presentation and relevance to formal methods and software engineering. We wish to sincerely thank all authors who submitted their work for consideration. We would also like to thank the Program Committee members and other reviewers for their great e?orts in the reviewing and selecting process. Weareindebtedtothethreekeynotespeakers,Prof.IanHayesoftheUniv- sity of Queensland, Prof. Mathai Joseph of the Tata Research, Development and DesignCentre,andDr.ColinO’HalloranofQinetiQ,foracceptingourinvitation to address the conference.

✦ Table of Contents


Front Matter....Pages -
Programs as Paths: An Approach to Timing Constraint Analysis....Pages 1-15
Model Based Code Verification....Pages 16-25
Adding Formalism to Methods or Where and When Will Industry Use Formal Reasoning? ....Pages 26-33
Using Formal Methods to Serialize Synchronization Events....Pages 34-47
An AMBA-ARM7 Formal Verification Platform....Pages 48-67
Formalization, Testing and Execution of a Use Case Diagram....Pages 68-85
Service-Based Systems Engineering: Consistent Combination of Services....Pages 86-104
Using State Diagrams to Describe Concurrent Behaviour....Pages 105-124
The Equivalence of Statecharts....Pages 125-143
Generic Interacting State Machines and Their Instantiation with Dynamic Features....Pages 144-166
Using PVS to Prove Properties of Systems Modelled in a Synchronous Dataflow Language....Pages 167-186
Formalising an Integrated Language in PVS....Pages 187-205
Modeling SystemC Fixed-Point Arithmetic in HOL....Pages 206-225
Adding Action Refinement to Stochastic True Concurrency Models....Pages 226-245
Incremental Derivation of Abstraction Relations for Data Refinement....Pages 246-265
Comparison of Data and Process Refinement....Pages 266-285
Compilation by Refinement for a Practical Assembly Language....Pages 286-305
Java Card Code Generation from B Specifications....Pages 306-318
Efficient Path Finding with the Sweep-Line Method Using External Storage....Pages 319-337
Formal Development of a Distributed Logging Mechanism Supporting Disconnected Updates....Pages 338-358
Formal Proof of a Polychronous Protocol for Loosely Time-Triggered Architectures....Pages 359-374
A Z Based Approach to Verifying Security Protocols....Pages 375-395
A Refinement Tool for Z....Pages 396-415
The Common Semantic Constructs of XML Family....Pages 416-431
Controller Synthesis for Object Petri Nets....Pages 432-451
Towards a Workflow Model of Real-Time Cooperative Systems....Pages 452-470
New Developments in Closed-Form Computation for GSPN Aggregation....Pages 471-490
On Clock Difference Constraints and Termination in Reachability Analysis of Timed Automata....Pages 491-503
Analyzing the Redesign of a Distributed Lift System in UPPAAL....Pages 504-522
Verification of Timeliness QoS Properties in Multimedia Systems....Pages 523-540
A Calculus for Set-Based Program Development....Pages 541-559
Compositional Verification of a Switch Fabric from Nortel Networks....Pages 560-578
Constraint-Based Model Checking of Data-Independent Systems....Pages 579-598
A Formal Model for the Block Device Subsystem of the Linux Kernel....Pages 599-619
A Mathematical Framework for Safecharts....Pages 620-640
A Relational Model for Formal Object-Oriented Requirement Analysis in UML....Pages 641-664
From Specification to Hardware Device: A Synthesis Algorithm....Pages 665-681
Back Matter....Pages -

✦ Subjects


Software Engineering; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Mathematical Logic and Formal Languages


πŸ“œ SIMILAR VOLUMES


Formal Methods and Software Engineering:
✍ Anthony Hall (auth.), Kung-Kiu Lau, Richard Banach (eds.) πŸ“‚ Library πŸ“… 2005 πŸ› Springer-Verlag Berlin Heidelberg 🌐 English

<P>This book constitutes the refereed proceedings of the 7th International Conference on Formal Engineering Methods, ICFEM 2005, held in Manchester, UK in November 2005.</P><P>The 30 revised full papers presented together with 3 invited contributions were carefully reviewed and selected from 74 subm

Formal Methods and Software Engineering:
✍ Anthony Hall (auth.), Kung-Kiu Lau, Richard Banach (eds.) πŸ“‚ Library πŸ“… 2005 πŸ› Springer-Verlag Berlin Heidelberg 🌐 English

<P>This book constitutes the refereed proceedings of the 7th International Conference on Formal Engineering Methods, ICFEM 2005, held in Manchester, UK in November 2005.</P><P>The 30 revised full papers presented together with 3 invited contributions were carefully reviewed and selected from 74 subm

Formal Methods and Software Engineering:
✍ Zhou Chaochen (auth.), Zhiming Liu, Jifeng He (eds.) πŸ“‚ Library πŸ“… 2006 πŸ› Springer-Verlag Berlin Heidelberg 🌐 English

<P>This book constitutes the refereed proceedings of the 8th International Conference on Formal Engineering Methods, ICFEM 2006, held in Macao, China, in November 2006.</P><P>The 38 revised full papers presented together with three keynote talks were carefully reviewed and selected from 108 submissi

Formal Methods and Software Engineering:
✍ Bernhard SchΓ€tz (auth.), Jim Davies, Wolfram Schulte, Mike Barnett (eds.) πŸ“‚ Library πŸ“… 2004 πŸ› Springer-Verlag Berlin Heidelberg 🌐 English

<p>Formal engineering methods are changing the way that software systems are - veloped.Withlanguageandtoolsupport,theyarebeingusedforautomaticcode generation, and for the automatic abstraction and checking of implementations. In the future, they will be used at every stage of development: requiremen

Formal Methods and Software Engineering:
✍ Bernhard SchΓ€tz (auth.), Jim Davies, Wolfram Schulte, Mike Barnett (eds.) πŸ“‚ Library πŸ“… 2004 πŸ› Springer-Verlag Berlin Heidelberg 🌐 English

<p>Formal engineering methods are changing the way that software systems are - veloped.Withlanguageandtoolsupport,theyarebeingusedforautomaticcode generation, and for the automatic abstraction and checking of implementations. In the future, they will be used at every stage of development: requiremen