FME '94, industrial benefit of formal methods : Second International Symposium of Formal Methods Europe, Barcelona, Spain, October 24-28, 1994 : proceedings

This Volume Presents The Proceedings Of The Second International Symposium Of Formal Methods Europe, Held In Barcelona, Spain In October 1994. Besides Two Invited Papers And Seven Industrial Usage Reports, There Are 32 Full Papers Selected From Some 150 Submissions. The Industrial Usage Reports Describe Practical Experiences In A Variety Of Areas Including Security Systems And Railway Signalling. The Subjects Of The Research Papers Include Refinement, Proof, Process Modelling, Specification Of Programming Languages, Model Checking, Real-time Aspects, And The Combination Of Formal And Systematic Methods; These Contributions Advance The Foundations Of Formal Methods And Demonstrate Their Practical Value.--publisher's Website. Maurice Naftalin, Tim Denvir, Miquel Bertran (eds.). Includes Bibliographical References. From action systems to modular systems....Pages 1-25 Formal methods in the railways signalling industry....Pages 26-34 Formal and informal specifications of a secure system component: first results in a comparative study....Pages 35-44 Formalising British rail's signalling rules....Pages 45-54 Three applications of formal methods at MITRE....Pages 55-65 Specification and analysis of a security management system....Pages 66-82 Verification techniques for LOTOS....Pages 83-92 Experiences in using the abstract machine notation in a GKS case study....Pages 93-104 Seven more myths of formal methods: Dispelling industrial prejudices....Pages 105-117 Comparing approaches to data reification....Pages 118-133 Towards a formalization of programming-by-difference....Pages 134-153 A new concept of refinement used for behaviour modelling with automata....Pages 154-174 An extended VDM refinement relation....Pages 175-189 On transferring VDM verification techniques to Z....Pages 190-213 Proof-based development of specifications with KIDS/VDM....Pages 214-232 Evaluation of underdetermined explicit definitions....Pages 233-250 A precise examination of the behaviour of process models....Pages 251-270 A theory of presentations....Pages 271-290 Applying a concurrent formal framework to process modelling....Pages 291-305 From MooZ to eiffel — A rigorous approach to system development....Pages 306-325 OPUS: a formal approach to object-orientation....Pages 326-345 A strategy for the production of verifiable code using the B Method....Pages 346-365 Specifying & verifying concurrent systems using Z....Pages 366-380 A critical look at functional specifications....Pages 381-400 Informal strategies in design by refinement....Pages 401-420 An experimental support system for formal mathematical reasoning....Pages 421-440 Literate mathematical development of a revision management system....Pages 441-460 An action semantics for ML concurrency primitives....Pages 461-479 A semantics for NewSpeak in VDM-SL....Pages 480-501 Evaluation semantics in Z....Pages 502-518 Abstract model checking of infinite specifications....Pages 519-531 Case study: Specification and refinement of the PI-Bus....Pages 532-546 Stepwise refinement of control software — A case study using RAISE....Pages 547-566 Specifying safety and progress properties with RSL....Pages 567-581 Validation of a railway interlocking model....Pages 582-601 A formal specification of an automatic train protection system....Pages 602-617 Adding real time to formal program development....Pages 618-638 Combining the design of industrial systems with effective verification techniques....Pages 639-658 RTL and refutation by positive cycles....Pages 659-680 Formalising the semantics of Ward/Mellor SA/RT essential models using a process algebra....Pages 681-702 Deriving relational database programs from formal specifications....Pages 703-723