FM 2003: the 12th International FME Symposium

Pisa, Italy -September 8-14, 2003
 

FM 2003 Program

Evening Events

Important Dates

Industry Day

Tutorials

Workshops

Call for Papers

Call for Tool Exhibition

Conference Chairs

Program Committee

Sponsors

Registration and Accommodation

Conference Venue

About Pisa

Related events

FM&&T Group

 

 

FM 2003 Program

 

FM at a glance

September 8, 2003

Registration desk opened since 8:30 a.m.
  • TA1: Architectures for Mobility
  • TB1: Advanced SPIN model Checking
    •
  • W1: WFAST - Workshop on Formal Aspects in Security & Trust
  • W2: FACS - Formal Aspects of Component Software
  • W3: SBSE - Service-based Software Engineering
    •
9:00-13:00

Lunch

 13:00-14:00
  • TA2: Semantic Web and Formal Methods
  • TB2: Formal Methods in Software Engineering Measurement and Software Engineering Measurement in Formal Methods
    •
  • W1: WFAST - Workshop on Formal Aspects in Security & Trust
  • W2: FACS - Formal Aspects of Component Software
  • W3: SBSE - Service-based Software Engineering
    •
14:00-18:00

September 9, 2003

Registration desk opened since 8:00 a.m.
  • TC1: Hybrid Systems for Computer Scientists
  • TD1: Formal Development of Critical Systems with UML: Methods and Tools
    •
  • W2: FACS - Formal Aspects of Component Software
    •
  • Tool Exhibition
 8:30-12:30

Lunch

 12:30-13:30
  • TD2: Integrating OO-Design and Deductive Verification of Software
    •
  • W4: ITCLS CoLogNet Workshop - Implementation Technology for Computational Logic Systems
    •
  • Tool Exhibition
 13:30-17:30

FM 2003 Opening Speech

Invited Talk Chair: Dines Bjørner
Invited Speaker: Kouichi Kishida
Title: Looking Back to the Future - Thoughts on Paradigm Shift in Software Development 		17:30-18:30

FM 2003 Symposium Opening Reception

 18:30

September 10, 2003

Registration desk opened since 8:30 a.m.

FM 2003 Welcome Speech

 8:45-9:15
Invited Talk Chair: Dino Mandrioli
Invited Speaker: Brian Randell
Title: On Failures and Faults 		9:15-10:15

Coffee Break
Tool Exhibition

 10:15-10:45
Plenary Session
Chair: Jonathan Bowen
  • Cliff Jones, Ian Hayes and Michael Jackson
    Determining the Specification of a Control System from that of its environment
  • Donna Stidolph and James Whitehead
    Managerial Issues for the Consideration and Use of Formal Methods
  • Colin Fidge
    Verifying Emulation of Legacy Mission Computer Systems
  • Marco Bozzano, Antonella Cavallo, Massimo Cifaldi, Laura Valacca and Adolfo Villafiorita
    Improving Safety Assessment of Complex Systems: An Industrial Case Study
    •

 
 10:45-11:15
 
11:15-11:45
 
11:45-12:15
 
12:15-12:45

Lunch

 12:45-14:15
Parallel Sessions
Chair: Tom Maibaum Chair: Mehdi Jazayeri
  • Vlad Rusu
    Compositional Verification of an ATM Protocol
  • Shengchao Qin, Jin Song Dong and Wei Ngan Chin
    A Semantic Foundation for TCOZ in Unifying Theories of Programming
    •
14:15-14:45
  • Neil Henderson
    Proving the Correctness of Simpson's 4-slot ACM Using An Assertional Rely-Guarantee Proof Method
  • Arnaud Lanoix and Olga Kouchnarenko
    Refinement and Verification of Synchronized Component-based Systems
    •
14:45-15:15
  • Mihaela Sighireanu and Marc Boyer
    Synthesis and Verification of Constraints in the PGM Protocol
    •
  • Grigore Rosu, Steven Eker, Patrick Lincoln and Jose Meseguer
    Certifying and Synthesizing Membership Equational Proofs
    •
15:15-15:45

Coffee Break
Tool Exhibition

 15:45-16:15
Chair: Alessandro Fantechi Chair: Diego Latella
  • Shengchao Qin, Wei Ngan Chin
    Mapping Statecharts to VERILOG for Hardware/Software Co-Specification
    •
  • Talk by Sponsor: Telelogic
    What's new in UML 2 for building executable models of distributed systems
    Philippe Leblanc
    •
16:15-16:45
  • Adolfo Duran, Ana Cavalcanti and Augusto Sampaio
    A Refinement Strategy for the Compilation of Classes, Inheritance and Dynamic Binding
    •
  • Maurice ter Beek, Jetty Kleijn
    Team Automata Satisfying Compositionality
    •
16:45-17:15
  • Talk by Sponsor: I-Logix
    Automatic Test Generation from Executable Specifications
    Andrew Heaton
    •
  • Michael Charpentier
    Composing Invariants
    •
17:15-17:45

Guided Tour to the "Piazza dei Miracoli" and Leaning Tower

 18:00

September 11, 2003

Registration desk opened since 8:30 a.m.
Invited Talk Chair: Stefania Gnesi
Invited Speaker: Gerard Holzmann
Title: Trends in Software Verification 		9:00-10:15

Coffee Break
Tool Exhibition

 10:15-10:45
Plenary Session
Chair: Kokichi Futatsugi
  • Lilian Burdy, Antoine Requet and Jean-Louis Lanet
    Java Applet Correctness: A Developer-Oriented Approach
  • Patrice Chalin,
    Improving JML: For a Safer and More Effective Language
  • Marc Lettrari
    Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems
  • Maria-Cristina Marinescu, Martin C. Rinard
    A Formal Framework for Modular Synchronous System Design
    •
 
 
10:45-11:15
 
11:15-11:45
 
11:45-12:15
 
12:15-12:45

Lunch

 12:45-14:15
Parallel Sessions
Chair: Dang Van Hung Chair: Han-Myung Chang
  • Marsha Chechik, Arie Gurfinkel
    Generating Conterexamples for Multi-Valued Model-Checking
    •
  • Diyaa-Addein Atiya, Steve King and Jim Woodcock
    A Circus Semantics for Ravenscar Protected Objects
    •
14:15-14:45
  • Andreas Schäfer
    Combining Real-Time Model-Checking and Fault Tree Analysis
    •
  • Pascal Fenkam, Harald Gall, Mehdi Jazayeri
    Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach
    •
14:45-15:15
  • Pierluigi San Pietro, Angelo Morzenti, Matteo Pradella and Paola Spoletini
    Model-Checking TRIO Specifications in SPIN
    •
  • Alessandro Aldini and Marco Bernardo
    A General Approach to Deadlock Freedom Verification for Software Architectures
    •
15:15-15:45

Coffee Break
Tool Exhibition

 15:45-16:15
Chair: Shin Sahara Chair: Nico Plat
  • Michael Rusinovitch and Julien Musset
    Computing Metatransitions for Linear Transition Systems Using Polynomials
    •
  • Marcelo Frias, Carlos G. Lopez Pombo, Gabriel A. Baum, Nazareno Aguirre and Tom Maibaum
    Taking Alloy to the Movies
    •
16:15-16:45
  • Fei Xie, James C. Browne and Robert P. Kurshan
    Translation-Based Compositional Reasoning for Software Systems
    •
  • Thomas Kuhn, David von Oheimb
    Interacting State Machines for Mobility
    •
16:45-17:15
  • Nick Moffat, Michael Goldsmith, Bill Roscoe, Tim Whitworth and Irfan Zakiuddin
    Watchdog Transformations for Property-Oriented Model Checking
    •
  • Jei-Wen Teng and Yih-Kuen Tsay
    Composing Temporal-Logic Specifications with Machine Assistance
    •
17:15-17:45

Conference banquet at "Le Arcate" Restaurant, in Villa Poschi near Pisa

  

September 12, 2003

Registration desk opened since 8:30 a.m.
Invited Talk Chair: Keijiro Araki
Invited Speaker: Jean-Raymond Abrial
Title: Event Based Sequential Program Development: Application to Constructing a Pointer Program 		9:00-10:15

Coffee Break
Tool Exhibition

 10:15-10:45
Plenary Session
Chair: Jim Woodcock
  • Andreas Thums and Gerhard Schellhorn
    Model-Checking FTA
  • Sabine Glesner
    Program Checking with Certificates: Separating Correctness-Critical Code
  • Fabrice Bouquet and Bruno Legeard
    Reification of Executable Test Scripts in Formal Specification-Based Test Generation: The Java Card Transaction Mechanism Case Study
  • Hai Wang, Jin Song Dong and Jing Sun
    Checking and Reasoning about Semantic Web through Alloy
    •

 
 10:45-11:15
 
11:15-11:45
 
11:45-12:15
 
 
12:15-12:45

Lunch

 12:45-14:15
Parallel Sessions
Chair: Shigeru Kusakabe Chair: Pierluigi San Pietro
  • Michael Poppleton and Richard Banach
    Structuring Retrenchments in B by Decomposition
    •
  • Alessandro Armando, Luca Compagna and Pierre Ganty
    SAT-Based Model-Checking of Security Protocols using Planning Graph Analysis
    •
14:15-14:45
  • Amel Mammar and Regine Laleau
    Design of an Automatic Prover Dedicated to the Refinement of Database Applications
    •
  • Ewen Denney and Bernd Fischer
    Correctness of Source-Level Safety Policies
    •
14:45-15:15
  • Michael Leuschel and Michael Butler
    ProB: A Model-Checker for B
    •
  • Giovanni Vigna
    A Topological Characterization of TCP/IP Security
    •
15:15-15:45

Coffee Break
Tool Exhibition

 15:45-16:15
Plenary Session:
  • Panel
    Chair: John Fitzgerald
    •
16:15-17:45

FM 2003 Closing

 17:45-17:55

September 13, 2003

Registration desk opened since 8:30 a.m.
  • W5: FMGALS - Formal Methods for Globally Asynchronous Locally Synchronous Architecture
  • W6: ST.EVE - STate-oriented vs. EVEnt-oriented thinking (in requirement analysis formal specification and software engineering)
  • W7: WTRTES - Testing Real-Time and Embedded Systems
    •
9:00-13:00

Lunch

 13:00-14:00
  • W5: FMGALS - Formal Methods for Globally Asynchronous Locally Synchronous Architecture
  • W6: ST.EVE - STate-oriented vs. EVEnt-oriented thinking (in requirement analysis formal specification and software engineering)
  • W7: WTRTES - Testing Real-Time and Embedded Systems
    •
14:00-18:00