FME 2003: Formal Methods

1. Front Matter

   Pages I-XV

   PDF

2. Invited Speakers

   1. Looking Back to the Future

      • Kouichi Kishida

      Pages 1-6

   2. Past, Present, and Future of SRA Implementation of CafeOBJ

      • Toshimi Sawada, Kouichi Kishida, Kokichi Futatsugi

      Pages 7-17

   3. On Failures and Faults

      • Brian Randell

      Pages 18-39

   4. Trends in Software Verification

      • Gerard J. Holzmann

      Pages 40-50

   5. Event Based Sequential Program Development: Application to Constructing a Pointer Program

      • Jean-Raymond Abrial

      Pages 51-74

3. I-Day

   1. Proving the Shalls

      • Steven P. Miller, Alan C. Tribble, Mats P. E. Heimdahl

      Pages 75-93

   2. Adaptable Translator of B Specifications to Embedded C Programs

      • Didier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, Laurent Voisin

      Pages 94-113

   3. Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle

      • Daniele Compare, Paola Inverardi, Patrizio Pelliccione, Alessandra Sebastiani

      Pages 114-132

   4. Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project

      • Alan Wassyng, Mark Lawford

      Pages 133-153

4. Control Systems and Industrial Applications

   1. Determining the Specification of a Control System from That of Its Environment

      • Ian J. Hayes, Michael A. Jackson, Cliff B. Jones

      Pages 154-169

   2. Managerial Issues for the Consideration and Use of Formal Methods

      • Donna C. Stidolph, James Whitehead

      Pages 170-186

   3. Verifying Emulation of Legacy Mission Computer Systems

      • Colin J. Fidge

      Pages 187-207

   4. Improving Safety Assessment of Complex Systems: An Industrial Case Study

      • Marco Bozzano, Antonella Cavallo, Massimo Cifaldi, Laura Valacca, Adolfo Villafiorita

      Pages 208-222

5. Communications System Verification

   1. Compositional Verification of an ATM Protocol

      • Vlad Rusu

      Pages 223-243

   2. Proving the Correctness of Simpson’s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method

      • Neil Henderson

      Pages 244-263

   3. Synthesis and Verification of Constraints in the PGM Protocol

      • Marc Boyer, Mihaela Sighireanu

      Pages 264-281

6. Co-specification and Compilers

   1. Mapping Statecharts to Verilog for Hardware/Software Co-specification

      • Shengchao Qin, Wei-Ngan Chin

      Pages 282-300

   2. A Strategy for Compiling Classes, Inheritance, and Dynamic Binding

      • Adolfo Duran, Ana Cavalcanti, Augusto Sampaio

      Pages 301-320

7. Composition

   1. A Semantic Foundation for TCOZ in Unifying Theories of Programming

      • Shengchao Qin, Jin Song Dong, Wei-Ngan Chin

      Pages 321-340

ThisvolumecontainstheproceedingsofFM2003,the12thInternationalFormal Methods Europe Symposium which was held in Pisa, Italy on September 8–14, 2003. Formal Methods Europe (FME, www. fmeurope. org) is an independent - sociation which aims to stimulate the use of and research on formal methods for system development. FME conferences began with a VDM Europe symposium in 1987. Since then, the meetings have grown and have been held about once - ery 18 months. Throughout the years the symposia have been notably successful in bringing together researchers, tool developers, vendors, and users, both from academia and from industry. Unlike previous symposia in the series, FM 2003 was not given a speci?c theme. Rather, its main goal could be synthesized as “widening the scope. ” Indeed, the organizers aimed at enlarging the audience and impact of the symposium along several directions. Dropping the su?x ‘E’ from the title of the conference re?ects the wish to welcome participation and contribution from every country; also,contributionsfromoutsidethetraditionalFormalMethodscommunitywere solicited. The recent innovation of including an Industrial Day as an important part of the symposium shows the strong commitment to involve industrial p- ple more and more within the Formal Methods community. Even the traditional and rather fuzzy borderline between “software engineering formal methods” and methods and formalisms exploited in di?erent ?elds of engineering was so- what challenged.

• abstraction
• design
• formal methods
• formal verification
• mathematical program construction
• model checking
• program analysis
• program correctness
• programming
• refinement
• semantic web
• software architecture
• software verification
• structured analysis
• verification

• Department of Computer Science and Communication Engineering, Graduate School of Information Science and Electrical Engineering, Kyushu University, Fukuoka, Japan

  Keijiro Araki

• Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, ISTI - CNR, Pisa, Italy

  Stefania Gnesi

• Dipartimento di Elettronica e Informazione, Politecnico di Milano, Italy

  Dino Mandrioli

Policies and ethics