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

From informal requirements to COOP: a concurrent automata approach....Pages 939-962
A framework for defining Object-Calculi extended abstract....Pages 963-982
A translation of statecharts to esterel....Pages 983-1007
An operational semantics for timed RAISE....Pages 1008-1027
Data abstraction for CSP-OZ....Pages 1028-1047
Systems development using Z generics....Pages 1048-1067
A brief summary of VSPEC....Pages 1068-1086
Enhancing the pre- and postcondition technique for more expressive specifications....Pages 1087-1106
On excusable and inexcusable failures towards an adequate notion of translation correctness....Pages 1107-1127
Interfacing program construction and verification....Pages 1128-1146
Software verification based on linear programming....Pages 1147-1165
Sensors and actuators in TCOZ....Pages 1166-1185
The UniForM workbench a universal development environment for formal methods....Pages 1186-1205
Integrating formal description techniques....Pages 1206-1225
A more complete TLA....Pages 1226-1244
Formal justification of the rely-guarantee paradigm for shared-variable concurrency: a semantic approach....Pages 1245-1265
Relating Z and first-order logic....Pages 1266-1280
Formal modeling of the enterprise javabeans™ component integration framework....Pages 1281-1300
Developing components in the presence of re-entrance....Pages 1301-1320
Communication and synchronisation using interaction objects....Pages 1321-1342
Modelling microsoft COM using π-calculus....Pages 1343-1363
Validation of mixed signal-alpha real-time systems through affine calculus on clock synchronisation constraints....Pages 1364-1383
Combining theorem proving and continuous models in synchronous design....Pages 1384-1399
Parts a partitioning transformation system....Pages 1400-1419
A behavioral model for co-design....Pages 1420-1438
A weakest precondition semantics for an object-oriented language of refinement....Pages 1439-1459
Reasoning about interactive systems....Pages 1460-1476
Non-atomic refinement in Z....Pages 1477-1496
Refinement semantics and loop rules....Pages 1497-1510
Lessons from the application of formal methods to the design of a storm surge barrier control system....Pages 1511-1526
The value of verification: positive experience of Industrial proof....Pages 1527-1545
Formal development and verification of a distributed railway control system....Pages 1546-1563
Safety analysis in formal specication....Pages 1564-1583
Formal specification and validation of a vital communication protocol....Pages 1584-1604
Incremental design of a Power transformer station controller using a controller synthesis methodology....Pages 1605-1624
Verifying behavioural specifications in CafeOBJ environment....Pages 1625-1643
Component-based algebraic specification and verification in cafeOBJ....Pages 1644-1663
Using algebraic specification techniques in development of object-oriented frameworks....Pages 1664-1683
Maude as a formal meta-tool....Pages 1684-1703
Hiding more of hidden algebra....Pages 1704-1719
A termination detection algorithm: specification and verification....Pages 1720-1737
Logspace reducibility via abstract state machines....Pages 1738-1757
Formal methods for extensions to CAS....Pages 1758-1777
An lgebraic framework for higher-order odules....Pages 1778-1797
Applying formal proof techniques to avionics software: a pragmatic approach....Pages 1798-1815
Secure synthesis of code: a process improvement experiment....Pages 1816-1835
Cronos: a separate compilation tool set for modular esterel applications....Pages 1836-1853
Tool support for production use of formal techniques....Pages 1854-1854
Modeling aircraft mission computer task rates....Pages 1855-1855
A study of collaborative work: answers to a test on formal specification in B....Pages 1856-1857
Archived design steps in temporal logic....Pages 1858-1858
A PVS-based approach for teaching constructing correct iterations....Pages 1859-1860
A minimal framework for specification theory....Pages 1861-1861
A model of specification-based testing of interactive systems....Pages 1862-1862
Algebraic aspects of the mapping between abstract syntax notation one and CORBA IDL....Pages 1863-1863
Retrenchment....Pages 1864-1865
Proof preservation in component generalization....Pages 1866-1866
Formal modelling and simulation of train control systems using petri nets....Pages 1867-1867
Formal specification of a voice communication system used in air traffic control an industrial application of light-weight formal methods using vdm....Pages 1868-1868
Model-checking the architectural design of a fail-safe communication system for railway interlocking systems....Pages 1869-1869
Analyzing the requirements of an access control using VDMTools and PVS....Pages 1870-1870
Cache coherence verification with TLA%....Pages 1871-1871