FME 2001: Formal Methods for Increasing Software Productivity

1. Front Matter

   Pages I-XIII

   PDF

2. Lightweight Formal Methods

   • Daniel Jackson

   Pages 1-1

3. Reformulation: a Way to Combine Dynamic Properties and B Refinement

   • F. Bellegarde, C. Darlot, J. Julliand, O. Kouchnarenko

   Pages 2-19

4. Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries

   • Steffen Helke, Thomas Santen

   Pages 20-42

5. Proofs of Correctness of Cache-Coherence Protocols

   • Joseph Stoy, Xiaowei Shen, Arvind

   Pages 43-71

6. Model-Checking Over Multi-Valued Logics

   • Marsha Chechik, Steve Easterbrook, Victor Petrovykh

   Pages 72-98

7. How to Make FDR Spin LTL Model Checking of CSP by Refinement

   • Michael Leuschel, Andrew Currie, Thierry Massart

   Pages 99-118

8. Avoiding State Explosion for Distributed Systems with Timestamps

   • Fabrice Derepas, Paul Gastin, David Plainfossé

   Pages 119-134

9. Secrecy-Preserving Refinement

   • Jan Jürjens

   Pages 135-152

10. Information Flow Control and Applications — Bridging a Gap —

    • Heiko Mantel

    Pages 153-172

11. A Rigorous Approach to Modeling and Analyzing E-Commerce Architectures

    • Vasu S. Alagar, Zheng Xi

    Pages 173-196

12. A Formal Model for Reasoning About Adaptive QoS-Enabled Middleware

    • Nalini Venkatasubramanian, Carolyn Talcott, Gul Agha

    Pages 197-221

13. A Programming Model for Wide-Area Computing

    • Jayadev Misra

    Pages 222-222

14. A Formal Model of Object-Oriented Design and GoF Design Patterns

    • Andres Flores, Luis Reynoso, Richard Moore

    Pages 223-241

15. Validation of UML Models Thanks to Z and Lustre

    • Sophie Dupuy-Chessa, Lydie du Bousquet

    Pages 242-258

16. Components, Contracts, and Connectors for the Unified Modelling Language UML

    • Claus Pahl

    Pages 259-277

17. An Integrated Approach to Specification and Validation of Real-Time Systems

    • Adnan Sherif, Augusto Sampaio, Sérgio Cavalcante

    Pages 278-299

18. Real-Time Logic Revisited

    • Stephen E. Paynter

    Pages 300-317

19. Improvements in BDD-Based Reachability Analysis of Timed Automata

    • Dirk Beyer

    Pages 318-343

20. Serialising Parallel Processes in a Hardware/Software Partitioning Context

    • Leila Silva, Augusto Sampaio, Geraint Jones

    Pages 344-363

FME 2001 is the tenth in a series of meetings organized every eighteen months by Formal Methods Europe (FME), an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. It follows four VDM Europe Symposia, four other Formal Methods Europe S- posia, and the 1999 World Congress on Formal Methods in the Development of Computing Systems. These meetings have been notably successful in bringing - gether a community of users, researchers, and developers of precise mathematical methods for software development. FME 2001 took place in Berlin, Germany and was organized by the C- puter Science Department of the Humboldt-Universit¨at zu Berlin. The theme of the symposium was Formal Methods for Increasing Software Productivity. This theme recognizes that formal methods have the potential to do more for industrial software development than enhance software quality { they can also increase productivity at many di erent points in the software life-cycle. The importance of the theme is borne out by the many contributed papers showing how formal methods can make software development more e cient. There is an emphasis on tools that nd errors automatically, or with relatively little human e ort. There is also an emphasis on the use of formal methods to assist with critical, labor-intensive tasks such as program design and test-case generation.

• Formal Methods
• Formal Specification
• Model Checking
• Program Analysis
• Refinement
• SPIN
• Safety-Critical Systems
• Software Patterns
• Software Testing
• Unified Modeling Language (UML)
• automata
• design
• formal verification
• logic
• productivity

• Computer Science Department, University of Minho, Braga, Portugal

  José Nuno Oliveira

• AT&T Laboratories — Research, Florham Park, USA

  Pamela Zave

Policies and ethics