FME '94: Industrial Benefit of Formal Methods : Second International Symposium of Formal Methods Europe, Barcelona, Spain, October 24 - 28, 1994. Proceedings - Couverture souple
Synopsis
From action systems to modular systems.- Formal methods in the railways signalling industry.- Formal and informal specifications of a secure system component: first results in a comparative study.- Formalising British rail's signalling rules.- Three applications of formal methods at MITRE.- Specification and analysis of a security management system.- Verification techniques for LOTOS.- Experiences in using the abstract machine notation in a GKS case study.- Seven more myths of formal methods: Dispelling industrial prejudices.- Comparing approaches to data reification.- Towards a formalization of programming-by-difference.- A new concept of refinement used for behaviour modelling with automata.- An extended VDM refinement relation.- On transferring VDM verification techniques to Z.- Proof-based development of specifications with KIDS/VDM.- Evaluation of underdetermined explicit definitions.- A precise examination of the behaviour of process models.- A theory of presentations.- Applying a concurrent formal framework to process modelling.- From MooZ to eiffel - A rigorous approach to system development.- OPUS: a formal approach to object-orientation.- A strategy for the production of verifiable code using the B Method.- Specifying & verifying concurrent systems using Z.- A critical look at functional specifications.- Informal strategies in design by refinement.- An experimental support system for formal mathematical reasoning.- Literate mathematical development of a revision management system.- An action semantics for ML concurrency primitives.- A semantics for NewSpeak in VDM-SL.- Evaluation semantics in Z.- Abstract model checking of infinite specifications.- Case study: Specification and refinement of the PI-Bus.- Stepwise refinement of control software - A case study using RAISE.- Specifying safety and progress properties with RSL.- Validation of a railway interlocking model.- A formal specification of an automatic train protection system.- Adding real time to formal program development.- Combining the design of industrial systems with effective verification techniques.- RTL and refutation by positive cycles.- Formalising the semantics of Ward/Mellor SA/RT essential models using a process algebra.- Deriving relational database programs from formal specifications.
Les informations fournies dans la section « Synopsis » peuvent faire référence à une autre édition de ce titre.
