FM 1999: Toulouse, France, Volume 1

Jeannette M. Wing, Jim Woodcock, Jim Davies (Eds.): FM'99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume I. Lecture Notes in Computer Science 1708 Springer 1999, ISBN 3-540-66587-0

Invited Papers

C. A. R. Hoare:
Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle. 1-27
Cliff B. Jones:
Scientific Decisions which Characterize VDM. 28-47
John M. Rushby:
Mechanized Formal Methods: Where Next? 48-51
Joseph Sifakis:
Integration, the Price of Success. 52-55
Michael Jackson:
The Role of Formalism in Method. 56

Eric Conquet, Jean-Luc Marty:
Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project. 57-75
Henk Eertink, Wil Janssen, Paul Oude Luttighuis, Wouter B. Teeuw, Chris A. Vissers:
A Business Process Design Language. 76-95

Jan Philipps, Bernhard Rumpe:
Refinement of Pipe-and-Filter Architectures. 96-115
John Herbert, Bruno Dutertre, Robert A. Riemenschneider, Victoria Stavridou:
A Formalization of Software Architecture. 116-133

Reino Kurki-Suonio:
Component and Interface Refinement in Closed-System Specifications. 134-154
Dusko Pavlovic:
Semantics of First Order Parametric Specifications. 155-172

Yonit Kesten, Amit Klein, Amir Pnueli, Gil Raanan:
A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. 173-194
Frank Reffel, Stefan Edelkamp:
Error Detection with Directed Symbolic Model Checking. 195-211
Rajeev Alur, Joel M. Esposito, M. Kim, Vijay Kumar, Insup Lee:
Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination. 212-232
Stavros Tripakis, Karine Altisen:
On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems. 233-252
Jean-Michel Couvreur:
On-the-Fly Verification of Linear Temporal Logic. 253-271
David Déharbe, Anamaria Martins Moreira:
Symbolic Model Checking with Fewer Fixpoint Computations. 272-288
Roberto Barbuti, Nicoletta De Francesco, Antonella Santone, Gigliola Vaglini:
Formula Based Abstractions of Transition Systems for Real-Time Model Checking. 289-306
Marius Bozga, Jean-Claude Fernandez, Lucian Ghirvu, Susanne Graf, Jean-Pierre Krimm, Laurent Mounier:
IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. 307-327
Farn Wang:
Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes. 328-347

Denis Sabatier, Pierre Lartigue:
The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications. 348-368
Patrick Behm, Paul Benoit, Alain Faivre, Jean-Marc Meynadier:
Météor: A Successful Application of B in a Large Project. 369-387
Brian Matthews, Elvira Locuratolo:
Formal Development of Databases in ASSO and B. 388-410
Yann Rouzaud:
Interpreting the B-Method in the Refinement Calculus. 411-430
Martin Büchi, Ralph-Johan Back:
Compositional Symmetric Sharing in B. 431-451
César Muñoz, John M. Rushby:
Structural Embeddings: Mechanization with Method. 452-471
Steve Dunne:
The Safe Machine: A New Specification Construct for B. 472-489
Michael J. Butler:
csp2B: A Practical Approach to Combining CSP and B. 490-508
Salimeh Behnia, Hélène Waeselynck:
Test Criteria Definition for B Models. 509-529

Richard F. Paige, Eric C. R. Hehner:
Bunches for Object-Oriented, Concurrent, and Real-Time Specification. 530-550
Enn Tyugu, Mihhail Matskin, Jaan Penjam:
Applications of Structural Synthesis of Programs. 551-569
Michel Charpentier, K. Mani Chandy:
Towards a Compositional Approach to the Design and Verification of Distributed Systems. 570-589

Andre Wong, Marsha Chechik:
Formal Modeling in a Commercial Setting: A Case Study. 590-607
Igor B. Burdonov, Alexander Kossatchev, Alexandre Petrenko, Dmitri Galter:
KVEST: Automated Generation of Test Suites from Formal Specifications. 608-621
Lydie du Bousquet:
Feature Interaction Detection Using Testing and Model-Checking Experience Report. 622-641
Nisse Husberg, Tapio Manner:
Emma: Developing an Industrial Reachability Analyser for SDL. 642-661
Jean-François Monin, Francis Klay:
Correctness Proof of the Standardized Algorithm for ABR Conformance. 662-681
Thomas Arts, Mads Dam:
Verifying a Distributed Database Lookup Manager Written in Erlang. 682-700

Fred Gilham, Robert A. Riemenschneider, Victoria Stavridou:
Secure Interoperation of Secure Distributed Databases. 701-717
Volkmar Lotz, Volker Kessler, Georg Walter:
A Formal Security Model for Microprocessor Hardware. 718-737
Steve Schneider:
Abstraction and Testing. 738-757
Dan Zhou, Shiu-Kai Chin:
Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol. 758-775
Patrick Lincoln, John C. Mitchell, Mark Mitchell, Andre Scedrov:
Probabilistic Polynomial-Time Equivalence and Security Analysis. 776-793
Riccardo Focardi, Fabio Martinelli:
A Uniform Approach for the Definition of Security Properties. 794-813
Paul F. Syverson, Stuart G. Stubblebine:
Group Principals and the Formalization of Anonymity. 814-833

Richard F. Paige, Jonathan S. Ostroff:
Developing BON as an Industrial-Strength Formal Method. 834-853
Luis Mandel, María Victoria Cengarle:
On the Expressive Power of OCL. 854-874
Eric Meyer, Jeanine Souquières:
A Systematic Approach to Transform OMT Diagrams to a B Specification. 875-895

Shaoying Liu:
Verifying Consistency and Validity of Formal Specifications by Testing. 896-914
Marine Tabourier, Ana R. Cavalli, Melania Ionescu:
A GSM-MAP Protocol Experiment Using Passive Testing. 915-934