FM 1999: Toulouse, France, Volume 2

Foundations of System Specification (IFIP WG 1.3)

• Pascal Poizat, Christine Choppy, Jean-Claude Royer:
  From Informal Requirements to COOP: A Concurrent Automata Approach. 939-962
  
• Frédéric Lang, Pierre Lescanne, Luigi Liquori:
  A Framework for Defining Object-Calculi. 963-982
  

European Theory and Practice of Software (ETAPS)

• Sanjit A. Seshia, R. K. Shyamasundar, A. K. Bhattacharjee, S. D. Dhodapkar:
  A Translation of Statecharts to Esterel. 983-1007
  
• Xia Yong, Chris George:
  An Operational Semantics for Timed RAISE. 1008-1027
  
• Heike Wehrheim:
  Data Abstraction for CSP-OZ. 1028-1047
  
• Fiona Polack, Susan Stepney:
  Systems Development Using Z Generics. 1048-1067
  
• Perry Alexander, Murali Rangarajan, Phillip Baraona:
  A Brief Summary of VSPEC. 1068-1086
  
• Gary T. Leavens, Albert L. Baker:
  Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. 1087-1106
  

Program Verification

• Markus Müller-Olm, Andreas Wolf:
  On Excusable and Inexcusable Failures. 1107-1127
  
• Richard Verhoeven, Roland Carl Backhouse:
  Interfacing Program Construction and Verification. 1128-1146
  
• S. Dellacherie, Samuel Devulder, Jean-Luc Lambert:
  Software Verification Based on Linear Programming. 1147-1165
  

Integration of Notation and Techniques

• Brendan P. Mahony, Jin Song Dong:
  Sensors and Actuators in TCOZ. 1166-1185
  
• Bernd Krieg-Brückner, Jan Peleska, Ernst-Rüdiger Olderog, Alexander Baer:
  The UniForM Workbench, a Universal Development Environment for Formal Methods. 1186-1205
  
• Bernhard Schätz, Franz Huber:
  Integrating Formal Description Techniques. 1206-1225
  

Formal Description of Programming Concepts (IFIP WG 2.2)

• Stephan Merz:
  A More Complete TLA. 1226-1244
  
• Frank S. de Boer, Ulrich Hannemann, Willem P. de Roever:
  Formal Justification of the Rely-Guarantee Paradigm for Shared-Variable Concurrency: A Semantic Approach. 1245-1265
  
• Andrew Martin:
  Relating Z and First-Order Logic. 1266-1280
  

Open Information Systems

• João Pedro Sousa, David Garlan:
  Formal Modeling of the Enterprise JavaBeans^TM Component Integration Framework. 1281-1300
  
• Leonid Mikhajlov, Emil Sekerinski, Linas Laibinis:
  Developing Components in the Presence of Re-entrance. 1301-1320
  
• H. B. M. Jonkers:
  Communication and Synchronisation Using Interaction Objects. 1321-1342
  
• Loe M. G. Feijs:
  Modelling Microsoft COM Using pi-Calculus. 1343-1363
  

Co-design

• Irina M. Smarandache, Thierry Gautier, Paul Le Guernic:
  Validation of Mixed SIGNAL-ALPHA Real-Time Systems through Affine Calculus on Clock Synchronisation Constraints. 1364-1383
  
• Simin Nadjm-Tehrani, Ove Åkerlund:
  Combining Theorem Proving and Continuous Models in Synchronous Design. 1384-1399
  
• Juliano Iyoda, Augusto Sampaio, Leila Silva:
  ParTS: A Partitioning Transformation System. 1400-1419
  
• Jifeng He:
  A Behavioral Model for Co-design. 1420-1438
  

Refinement

• Ana Cavalcanti, David A. Naumann:
  A Weakest Precondition Semantics for an Object-Oriented Language of Refinement. 1439-1459
  
• Ralph-Johan Back, Anna Mikhajlova, Joakim von Wright:
  Reasoning About Interactive Systems. 1460-1476
  
• John Derrick, Eerke A. Boiten:
  Non-atomic Refinement in Z. 1477-1496
  
• Eric C. R. Hehner, Andrew M. Gravell:
  Refinement Semantics and Loop Rules. 1497-1510
  

Safety

• Michel R. V. Chaudron, Jan Tretmans, Klaas Wijbrans:
  Lessons from the Application of Formal Methods to the Design of a Storm Surge Barrier Control System. 1511-1526
  
• Steve King, Jonathan Hammond, Roderick Chapman, Andy Pryor:
  The Value of Verification: Positive Experience of Industrial Proof. 1527-1545
  
• Anne Elisabeth Haxthausen, Jan Peleska:
  Formal Development and Verification of a Distributed Railway Control System. 1546-1563
  
• Kaisa Sere, Elena Troubitsyna:
  Safety Analysis in Formal Specification. 1564-1583
  
• Alessandro Cimatti, P. L. Pieraccini, Roberto Sebastiani, Paolo Traverso, Adolfo Villafiorita:
  Formal Specification and Validation of a Vital Communication Protocol. 1584-1604
  
• Hervé Marchand, Mazen Samaan:
  Incremental Design of a Power Transformer Station Controller Using a Controller Synthesis Methodology. 1605-1624
  

OBJ/Cafe OBJ/Maude

• Akira Mori, Kokichi Futatsugi:
  Verifying Behavioural Specifications in CafeOBJ Environment. 1625-1643
  
• Razvan Diaconescu, Kokichi Futatsugi, Shusaku Iida:
  Component-Based Algebraic Specification and Verification in CafeOBJ. 1644-1663
  
• Shin Nakajima:
  Using Algebraic Specification Techniques in Development of Object-Oriented Frameworks. 1664-1683
  
• Manuel Clavel, Francisco Durán, Steven Eker, José Meseguer, Mark-Oliver Stehr:
  Maude as a Formal Meta-tool. 1684-1703
  
• Joseph A. Goguen, Grigore Rosu:
  Hiding More of Hidden Algebra. 1704-1719
  

Abstract State Machines (ASM) and Algebraic Methods in Software Technology (AMAST)

• Robert Eschbach:
  A Termination Detection Algorithm: Specification and Verification. 1720-1737
  
• Erich Grädel, Marc Spielmann:
  Logspace Reducibility via Abstract State Machines. 1738-1757
  
• Martin Dunstan, Tom Kelsey, Ursula Martin, Steve Linton:
  Formal Methods for Extensions to CAS. 1758-1777
  
• Rosa M. Jiménez, Fernando Orejas:
  An Algebraic Framework for Higher-Order Modules. 1778-1797
  

Avionics

• Famantanantsoa Randimbivololona, Jean Souyris, Patrick Baudin, Anne Pacalet, Jacques Raguideau, Dominique Schoen:
  Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach. 1798-1815
  
• P. Garbett, J. P. Parkes, M. Shackleton, S. Anderson:
  Secure Synthesis of Code: A Process Improvement Experiment. 1816-1835
  
• Olivier Hainque, Laurent Pautet, Yann Le Biannic, Eric Nassor:
  Cronos: A Separate Compilation Toolset for Modular Esterel Applications. 1836-1853
  

Works-in-Progress

• John C. Knight, P. Thomas Fletcher, Brian R. Hicks:
  Tool Support for Production Use of Formal Techniques. 1854
  
• Jin Song Dong, Brendan P. Mahony, Neale Fulton:
  Modeling Aircraft Mission Computer Task Rates. 1855
  
• Henri Habrias, Pascal Poizat, Jean-Yves Lafaye:
  A Study of Collaborative Work: Answers to a Test on Formal Specification in B. 1856-1857
  
• Pertti Kellomäki, Tommi Mikkonen:
  Archived Design Steps in Temporal Logic. 1858
  
• Michel Levy, Laurent Trilling:
  A PVS-Based Approach for Teaching Constructing Correct Iterations. 1859-1860
  
• Bernd Baumgarten:
  A Minimal Framework for Specification Theory. 1861
  
• Ian MacColl, David A. Carrington:
  A Model of Specification-Based Testing of Interactive Systems. 1862
  
• Radu Ocica, Dan Ionescu:
  Algebraic Aspects of the Mapping between Abstract Syntax Notation One and CORBA IDL. 1863
  
• Richard Banach, Michael Poppleton:
  Retrenchment. 1864-1865
  
• Anamaria Martins Moreira:
  Proof Preservation in Component Generalization. 1866
  

Industrial Experience

• Michael Meyer zu Hörste, Eckehard Schnieder:
  Formal Modelling and Simulation of Train Control Systems Using Petri Nets. 1867
  
• Johann Hörl, Bernhard K. Aichernig:
  Formal Specification of a Voice Communication System Used in Air Traffic Control. 1868
  
• Bettina Buth, Mike Schrönen:
  Model-Checking the Architectural Design of a Fail-Safe Communication System for Railway Interlocking Systems. 1869
  
• Georg Droschl:
  Analyzing the Requirements of an Access Control Using VDMTools and PVS. 1870
  
• Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark R. Tuttle, Yuan Yu:
  Cache Coherence Verification with TLA+. 1871-1872