The proceedings of the fourth Vienna Development Method Symposium, VDM'91, are published here in two volumes. Previous VDM symposia were held in 1987 (LNCS 252), 1988 (LNCS 328), and 1990 (LNCS 428). The VDM symposia have been organized by VDM Europe, formed in 1985 as an advisory board sponsored by the Commission of the European Communities. The VDM Europe working group consisted of researchers, software engineers, and programmers, allinterested in promoting the industrial usage of formal methods for software development. The fourth VDM symposium presented not only VDM but also a large number of other methods for formal software development. Volume 1 contains conference contributions. It has four parts: contributions of invited speakers, papers, project reports, and tools demonstration abstracts. The emphasis is on methods and calculi for development, verification and verification tools support, experiences from doing developments, and the associated theoretical problems. Volume 2 contains four introductory tutorials (on LARCH, Refinement Calculus, VDM, and RAISE) and four advanced tutorials (on ABEL, PROSPECTRA, The B Method, and The Stack). They present a comprehensive account of the state of theart.
Author(s): Michael Jackson (auth.), S. Prehn, W. J. Toetenel (eds.)
Series: Lecture Notes in Computer Science 551
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1991
Language: English
Pages: 705
Tags: Software Engineering; Logics and Meanings of Programs
Description is our business....Pages 1-8
Concurrent processes as objects....Pages 9-9
The Larch approach to specification....Pages 10-10
Formal specification in metamorphic programming....Pages 11-30
Formalizing design spaces: Implicit invocation mechanisms....Pages 31-44
On type checking in VDM and related consistency issues....Pages 45-62
Combining transformation and posit-and-prove in a VDM development....Pages 63-80
A case for structured analysis/formal design....Pages 81-105
A model-oriented method for algebraic specifications using COLD-1 as notation....Pages 106-124
A mechanical formalization of several fairness notions....Pages 125-148
Specification and stepwise development of communicating systems....Pages 149-163
Writing operational semantics in Z: A structural approach....Pages 164-188
EZ: A system for automatic prototyping of Z specifications....Pages 189-203
Z and high level Petri nets....Pages 204-219
An approach to the static semantics of VDM-SL....Pages 220-253
Behavioural extension for CSP....Pages 254-267
Cpo's do not form a cpo, and yet recursion works....Pages 268-278
LPF and MPL ω — A logical comparison of VDM SL and COLD-K....Pages 279-308
Tactical tools for distributing VDM specifications....Pages 309-323
An attempt to reason about shared-state concurrency in the style of VDM....Pages 324-342
Reasoning about VDM specifications....Pages 343-355
On formal specification of a proof tool....Pages 356-370
Reasoning about VDM developments using the VDM support tool in mural....Pages 371-388
EVES: An overview....Pages 389-405
Deriving transitivity of VDM-reification in DEVA....Pages 406-427
Upgrading the pre- and postcondition technique....Pages 428-456
The formal development of a secure transaction mechanism....Pages 457-476
Formal development of a Serial Copy Management System....Pages 477-495
Specification and refinement in an integrated database application environment....Pages 496-510
Techniques for partial specification and specification of switching systems....Pages 511-525
Specification of the MAA standard in VDM....Pages 526-544
Unintrusive ways to integrate formal specifications in practice....Pages 545-569
An overview of HP-SL....Pages 571-587
CICS project report experiences and results from the use of Z in IBM....Pages 588-596
A debugger for a Meta-IV-like meta-language....Pages 597-603
An executable subset of Meta-IV with loose specification....Pages 604-618
Using VDM within an object-oriented framework....Pages 619-628
The integrated software development and verification system ATES....Pages 629-644
Using RAISE — first impressions from the LaCoS applications....Pages 645-657
A specification of a complex programming language statement....Pages 658-667
The prospectra system....Pages 668-669
The visual presentation of VDM specifications....Pages 670-671
Mural and specbox....Pages 672-674
The VDM domain compiler a VDM class library generator....Pages 675-676
The Delft VDM-SL front-end....Pages 677-680
Prototyping with temporal VDM a status report....Pages 681-682
The Exspect tool....Pages 683-684
CADiZ - Computer aided design in Z....Pages 685-686
The HP-ST toolset....Pages 687-688
The RAISE toolset....Pages 689-690
The IBM Z tool....Pages 691-692
The VDM-SL editor and consistency checker....Pages 693-694
B-tool....Pages 695-696
A VDM subset compiler....Pages 697-698
