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.
Author(s): R. J. R. Back, K. Sere (auth.), Maurice Naftalin, Tim Denvir, Miquel Bertran (eds.)
Series: Lecture Notes in Computer Science 873
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1994
Language: English
Pages: 732
Tags: Programming Techniques; Software Engineering; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Business Information Systems
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
