Formal Methods in Standards: A Report from the BCS Working Group

ISBN-13: 9783540195771 / Angielski / Miękka / 1990 / 135 str.

Clive L. N. Ruggles; Derek Andrews; David Blyth

Opis

3. 1 What are formal methods? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3. 2 A survey of formal methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3. 2. 1 FDTs and FSLs for sequential software . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3. 2. 1. 1 VDM (Vienna Development Method). . . . . . . . . . . . . . . . . . . . . 19 3. 2. 1. 2 Z. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3. 2. 1. 3 me too . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3. 2. 1. 4 HOS and AXES. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3. 2. 1. 5 Gist. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3. 2. 1. 6 Clear . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3. 2. 1. 7 OBJ. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3. 2. 1. 8 ACT ONE and ACT TWO. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3. 2. 1. 9 CIP-L. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3. 2. 1. 10 LPG. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3. 2. 1. 11 Larch. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3. 2. 1. 12 Logic languages-the Prolog family. . . . . . . . . . . . . . . . . . . 22 3. 2. 1. 13 Functional languages. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3. 2. 2 FDTs and FSLs for concurrent software. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3. 2. 2. 1 LOTOS. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3. 2. 2. 2 Estelle. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3. 2. 2. 3 SDL. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3. 2. 2. 4 ASN. l . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3. 2. 2. 5 TTCN. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3. 2. 2. 6 Gypsy. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3. 2. 3 Graphical formalisms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3. 2. 3. 1 Petri nets. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3. 2. 3. 2 Higraphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3. 2. 4 Less formal methods and notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3. 2. 4. 1 SADT. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3. 2. 4. 2 Structured Design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3. 2. 4. 3 SSADM and LSDM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3. 2. 4. 4 JSPandJSD. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3. 2. 4. 5 HDM and the SPECIAL language . . . . . . . . . . . . . . . . . . . . . . . . . . 27 3. 2. 4. 6 Structured analysis and design of real-time systems. . 27 3. 3 Support tools for FDTs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Spis treści

1 The Formal Methods in Standards Working Group.- 1.1 Terms of reference.- 1.2 Constitution.- 1.3 Modus operandi.- 1.4 Membership.- 2 Standards: the Background.- 2.1 What is a standard?.- 2.1.1 Concepts.- 2.1.2 Why standardise?.- 2.1.3 Principles of standardisation.- 2.1.4 Problems.- 2.2 The standards-making structure.- 2.2.1 The protagonists.- 2.2.1.1 Overview.- 2.2.1.2 Formative committees.- 2.2.1.3 ISO.- 2.2.2 The ISO/IEC Joint Technical Committee on Information Technology.- 2.3 The standards development process.- 2.3.1 International standards generation: an overview.- 2.3.1.1 Identification of user requirements.- 2.3.1.2 Advancement of user requirements.- 2.3.1.3 Development and review.- 2.3.2 An analogy with the software development process.- 2.4 The quality of standards.- 2.4.1 Failure to serve a useful purpose.- 2.4.2 Difficulty of use.- 2.4.3 Incompatibility with other standards.- 2.4.4 Difficulty of maintenance.- 2.4.5 Malfunction.- 3 Formal Methods: the Background.- 3.1 What are formal methods?.- 3.2 A survey of formal methods.- 3.2.1 FDTs and FSLs for sequential software.- 3.2.1.1 VDM (Vienna Development Method).- 3.2.1.2 Z.- 3.2.1.3 me too.- 3.2.1.4 HOS and AXES.- 3.2.1.5 Gist.- 3.2.1.6 Clear.- 3.2.1.7 OBJ.- 3.2.1.8 ACT ONE and ACT TWO.- 3.2.1.9 CIP-L.- 3.2.1.10 LPG.- 3.2.1.11 Larch.- 3.2.1.12 Logic languages-the Prolog family.- 3.2.1.13 Functional languages.- 3.2.2 FDTs and FSLs for concurrent software.- 3.2.2.1 LOTOS.- 3.2.2.2 Estelle.- 3.2.2.3 SDL.- 3.2.2.4 ASN.1.- 3.2.2.5 TTCN.- 3.2.2.6 Gypsy.- 3.2.3 Graphical formalisms.- 3.2.3.1 Petri nets.- 3.2.3.2 Higraphs.- 3.2.4 Less formal methods and notations.- 3.2.4.1 SADT.- 3.2.4.2 Structured Design.- 3.2.4.3 SSADM and LSDM.- 3.2.4.4 JSP and JSD.- 3.2.4.5 HDM and the SPECIAL language.- 3.2.4.6 Structured analysis and design of real-time systems.- 3.3 Support tools for FDTs.- 3.3.1 Introduction.- 3.3.2 The nature of FDT tools.- 3.3.3 Validation and verification tools.- 3.3.4 Tool environments.- 3.4 A survey of methods and tools: the STARTS guide.- 4 Formal Methods in Standards: Four Case Studies.- 4.1 Introduction.- 4.2 Programming languages.- 4.2.1 Overview.- 4.2.2 The denotational approach to the formal definition of a programming language.- 4.2.3 Formal definitions of real languages.- 4.2.4 Discussion.- 4.3 Document structure.- 4.3.1 The Standard Generalised Markup Language (SGML).- 4.3.1.1 What is SGML?.- 4.3.1.2 The development of SGML.- 4.3.1.3 Discussion.- 4.3.2 Office Document Architecture (ODA).- 4.3.2.1 What is ODA9.- 4.3.2.2 FODA.- 4.3.2.3 History and development of FODA.- 4.3.2.4 Definition and uses of FODA.- 4.3.2.5 Developments in formalising ODA.- 4.3.2.6 Conclusions.- 4.4 Graphics.- 4.4.1 Introduction.- 4.4.2 Standards for computer graphics.- 4.4.3 Applications of formal specification to computer graphics.- 4.4.3.1 Early work.- 4.4.3.2 Specification of standards for computer graphics.- 4.4.3.3 Applications to GKS.- 4.4.4 Future developments.- 4.5 Open systems interconnection.- 4.5.1 Formal methods in computer communication standards.- 4.5.1.1 Introduction.- 4.5.1.2 Historical background.- 4.5.1.3 The current situation.- 4.5.1.4 An example: multiplexing.- 4.5.1.5 Limitations and prospects.- 4.5.2 OSI Protocol Conformance Testing.- 4.5.2.1 The ISO method of conformance test (derivation and) specification.- 4.5.2.2 Tree and Tabular Combined Notation (TTCN).- 4.5.2.3 Conformance testing of FTAM in the CTS-WAN project.- 4.5.2.4 Conclusion.- 5 Current Practice: Issues and Guidelines.- 5.1 Introduction.- 5.2 Quality and correctness.- 5.3 Phased introduction of formal methods.- 5.4 Parallel and retrospective application of formal methods.- 5.5 Choice of formal notation.- 5.6 Tools.- 5.7 General conclusions.- Bibliography of standards.- General bibliography.- Appendix A.- List of Acronyms.- Appendix B.- Glossary of Formal Methods Terminology.

O autorze

Report produced by the Formal Methods in Standards Working Group of the British Computer Society.