FM’99 — Formal Methods: World Congress on Formal Methods in the Development of Computing Systems Toulouse, France, September 20–24, 1999 Proceedings, Volume I

Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle....Pages 1-27
Scientific Decisions which Characterize VDM....Pages 28-47
Mechanized Formal Methods: Where Next?....Pages 48-51
Integration, the Price of Success....Pages 52-55
The Role of Formalism in Method....Pages 56-56
Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project....Pages 57-75
A Business Process Design Language....Pages 76-95
Refinement of Pipe-and-Filter Architectures....Pages 96-115
A Formalization of Software Architecture....Pages 116-133
Component and Interface Refinement in Closed-System Specifications....Pages 134-154
Semantics of First Order Parametric Specifications....Pages 155-172
A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software....Pages 173-194
Error Detection with Directed Symbolic Model Checking....Pages 195-211
Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination....Pages 212-232
On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems....Pages 233-252
On-the-fly Verification of Linear Temporal Logic....Pages 253-271
Symbolic Model Checking with Fewer Fixpoint Computations....Pages 272-288
Formula Based Abstractions of Transition Systems for Real-Time Model Checking....Pages 289-306
If: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems....Pages 307-327
Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes....Pages 328-347
The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications....Pages 348-368
Météor: A Successful Application of B in a Large Project....Pages 369-387
Formal Development of Databases in ASSO and B....Pages 388-410
Interpreting the B-Method in the Refinement Calculus....Pages 411-430
Compositional Symmetric Sharing in B....Pages 431-451
Structural Embeddings: Mechanization with Method....Pages 452-471
The Safe Machine: A New Specification Construct for B....Pages 472-489
csp2B: A Practical Approach to Combining CSP and B....Pages 490-508
Test Criteria Definition for B Models....Pages 509-528
Bunches for Object-Oriented, Concurrent, and Real-Time Specification....Pages 530-550
Applications of Structural Synthesis of Programs....Pages 551-569
Towards a Compositional Approach to the Design and Verification of Distributed Systems....Pages 570-589
Formal Modeling in a Commercial Setting: A Case Study....Pages 590-607
KVEST: Automated Generation of Test Suites from Formal Specifications....Pages 608-621
Feature Interaction Detection Using Testing and Model-Checking Experience Report....Pages 622-641
Emma: Developing an Industrial Reachability Analyser for SDL....Pages 642-661
Correctness Proof of the Standardized Algorithm for ABR Conformance....Pages 662-681
Verifying a Distributed Database Lookup Manager Written in Erlang....Pages 682-700
Secure Interoperation of Secure Distributed Databases....Pages 701-717
A Formal Security Model for Microprocessor Hardware....Pages 718-737
Abstraction and Testing....Pages 738-757
Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol....Pages 758-775
Probabilistic Polynomial-Time Equivalence and Security Analysis....Pages 776-793
A Uniform Approach for the Definition of Security Properties....Pages 794-813
Group Principals and the Formalization of Anonymity....Pages 814-833
Developing BON as an Industrial-Strength Formal Method....Pages 834-853
On the Expressive Power of OCL....Pages 854-874
A Systematic Approach to Transform OMT Diagrams to a B Specification....Pages 875-895
Verifying Consistency and Validity of Formal Specifications by Testing....Pages 896-914
A GSM-MAP Protocol Experiment Using Passive Testing....Pages 915-934