References

Abr96

Jean-Raymond Abrial.
The B Book: Assigning Programs to meanings.
Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, England, 1996.

AC91

W. Atkinson and J. Cunningham.
Proving properties of a safety-critical system.
Software Engineering Journal, 6(2):41-50, March 1991.

Abstract: The paper describes the FOREST approach to formal requirements specification and particularly the role of an automated theorem prover in validating specifications written in MAL, the FOREST logic. The MAL prover uses a tableau method for constructing its proofs, with rules to handle the action modalities and quantification of MAL. The authors illustrate its use in validation by using the prover to establish that a safety-critical railway-signalling specification has some desirable safety properties.

Keywords: formal specification; program verification; safety; software reliability; theorem proving.

BJ78

D. Bjørner and C.B. Jones, editors.
The Vienna Development Method: The Meta-Language, volume 61 of Lecture Notes in Computer Science.
Springer-Verlag, 1978.

CH93

Zhou Chaochen and Michael R. Hansen.
Lecture Notes on Logical Foundations for the Duration Calculus.
Lecture Notes, 13, UNU/IIST, P.O.Box 3058, Macau, August 1993.

Cha93

Zhou Chaochen.
Duration Calculi: An Overview.
Research Report 10, UNU/IIST, P.O.Box 3058, Macau, June 1993.
Published in: Formal Methods in Programming and Their Applications, Conference Proceedings, June 28 - July 2, 1993, Novosibirsk, Russia; (Eds.: D. Bjørner, M. Broy and I. Pottosin) LNCS 736, Springer-Verlag, 1993, pp 36-59.

CHKBM97

M. Cerioli, A. Haxthausen, B. Krieg-Brückner, and T. Mossakowski.
Permissive Sub-sorted Partial Logic in CASL.
In Proceedings, AMAST'97, volume 1349 of Lecture Notes in Computer Science. Springer-Verlag, 1997.

CHR91

Zhou Chaochen, C.A.R. Hoare, and A.P. Ravn.
A Calculus of Durations.
Information Processing Letters, 40(5):269-276, 1991.

CHX95

Zhou Chaochen, Dang Van Hung, and Li Xiaoshan.
A Duration Calculus with Infinite Intervals.
Research Report 40, UNU/IIST, P.O.Box 3058, Macau, February 1995.
Published in: Fundamentals of Computation Theory, Horst Reichel (ed.), pp 16-41, LNCS 965, Springer-Verlag, 1995.

COL90

Algebraic Specifications.
Tutorial Material, April 1990.
This is COLD-K Course Material.

CRH93

Zhou Chaochen, Anders P. Ravn, and Michael R. Hansen.
An Extended Duration Calculus for Real-time Systems.
Research Report 9, UNU/IIST, P.O.Box 3058, Macau, January 1993.
Published in: Hybrid Systems, LNCS 736, 1993.

CX93

Zhou Chaochen and Li Xiaoshan.
A Mean Value Duration Calculus.
Research Report 5, UNU/IIST, P.O.Box 3058, Macau, March 1993.
Published as Chapter 25 in A Classical Mind, Festschrift for C.A.R. Hoare, Prentice-Hall International, 1994, pp 432-451.

DF96

Razvan Diaconescu and Kokichi Futatsugi.
Logical Semantics of CafeOBJ.
Research Report IS-RR-96-0024S, JAIST, 1996.

ELC⁺98

S. Easterbrook, R. Lutz, R. Covington, J. Kelly, Y. Ampo, and D. Hamilton.
Experiences using lightweight formal methods for requirements modeling.
IEEE Transactions on Software Engineering, 24(1):4-14, 1998.

Abstract: The paper describes three case studies in the lightweight application of formal methods to requirements modeling for spacecraft fault protection systems. The case studies differ from previously reported applications of formal methods in that formal methods were applied very early in the requirements engineering process to validate the evolving requirements. The results were fed back into the projects to improve the informal specifications. For each case study, we describe what methods were applied, how they were applied, how much effort was involved, and what the findings were. In all three cases, formal methods enhanced the existing verification and validation processes by testing key properties of the evolving requirements and helping to identify weaknesses. We conclude that the benefits gained from early modeling of unstable requirements more than outweigh the effort needed to maintain multiple representations.

Keywords: aerospace computing; fault tolerant computing; formal specification; program verification; space vehicles; systems analysis.

FD

Kokichi Futatsugi and Razvan Diaconescu.
CafeOBJ Report -- Definition of the Language.
To appear in 1998 as book in the AMAST series at World Scientific

Abstract: .
This is a report on the formal definition of the CafeOBJ algebraic language, which is a modern successor of the famous algebraic language OBJ. While the equational core of CafeOBJ is just a re-shaping of OBJ3, CafeOBJ significantly extends OBJ3 by implementing several recent major developments in the area of algebraic specification, such as behavioural specification and rewriting logic. The definition of the language parallels its logical semantics based on the so-called institutions which also provide a methodological framework for structuring the presentation of the basic constructs of the language and their semantics. This report presents all basic constructs of the language together with their semantics and addressing both the programming in-the-small and in-the-large levels, but also discusses proof systems and technologies, as well as methodologies. Examples are provided all over the report as intuitive support for the definitions of the constructs and for illustrating proof techniques and methodologies.

FL98

John Fitzgerald and Peter Gorm Larsen.
Modelling Systems: Practical Tools and Techniques.
Cambridge University Press, 1997-1998.

GHG⁺93

John V. Guttag, James J. Horning, S.J. Garland, K.D. Jones, A. Modet, , and J.M. Wing.
Larch: Languages and Tools for Formal Specification.
Texts and Monographs in Computer Science. Springer-Verlag, Springer-Verlag New York, Inc., Attn: J. Jeng, 175 Fifth Avenue, New York, NY 10010-7858, USA, 1993.

Abstract: methodology and of specific Larch languages for specifying C and Modula-3 interfaces. Written for practicing programmers and students, it includes both tutorial and advanced material, illustrated by numerous examples, including an extensive handbook of Larch Shared Language specifications. It also provides information on the publicly available tools that support the methodology and the languages, including LP, a powerful tool for reasoning about specifications. 250 pages, 76 illustrations; ISBN 0-387-94006-5, ISBN 3-540-94006-5; US$39.50.

GHRN93a

Dov M. Gabbay, C.J. Hogger, J.A. Robinson, and D. Nute, editors.
Deduction Methodologies, volume 2 of Handbook of Logic in Artificial Intelligence and Logic Programming.
Oxford Science Publications, Clarendon Press, Oxford, England, 1993.

GHRN93b

Dov M. Gabbay, C.J. Hogger, J.A. Robinson, and D. Nute, editors.
Logical Foundations, volume 1 of Handbook of Logic in Artificial Intelligence and Logic Programming.
Oxford Science Publications, Clarendon Press, Oxford, England, 1993.

GHRN94

Dov M. Gabbay, C.J. Hogger, J.A. Robinson, and D. Nute, editors.
Nonmonotonic Reasoning and Uncertain Reasoning, volume 3 of Handbook of Logic in Artificial Intelligence and Logic Programming.
Oxford Science Publications, Clarendon Press, Oxford, England, 1994.

GHRN95

Dov M. Gabbay, C.J. Hogger, J.A. Robinson, and D. Nute, editors.
Epistemic and Temporal Reasoning, volume 4 of Handbook of Logic in Artificial Intelligence and Logic Programming.
Oxford Science Publications, Clarendon Press, Oxford, England, 1995.

GHRN98

Dov M. Gabbay, C.J. Hogger, J.A. Robinson, and D. Nute, editors.
Logic in Logic Programming, volume 5 of Handbook of Logic in Artificial Intelligence and Logic Programming.
Oxford Science Publications, Clarendon Press, Oxford, England, 1998.

GM93

M.J.C. Gordon and T.F. Melham.
Introduction to HOL: A theorem proving environment for higher order logic.
Cambridge Univ. Press, England, 1993.

GP94

J.F. Groote and A. Ponse.
Proof Theory for $\mu$CRL: a Language for Processes with data.
In D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors, International Workshop on Semantics of Specification Languages, pages 232-251. Springer-Verlag, 1994.

GP95

J.F. Groote and A. Ponse.
Syntax and Semantics of $\mu$CRL.
In A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors, Algebra of communicating processes, Utrecht 1994, pages 232-251. Springer-Verlag, 1995.

Gro92

The RAISE Method Group.
The RAISE Method.
The BCS Practitioner Series. Prentice-Hall, Hemel Hampstead, England, 1992.

Gro95

The RAISE Language Group.
The RAISE Specification Language.
The BCS Practitioner Series. Prentice-Hall, Hemel Hampstead, England, 1995.

GvV95

J.F. Groote and S.F.M. van Vlijmen.
A modal logic for $\mu$CRL.
In A. Ponse, M. de Rijke, and Y. Venema, editors, Modal logic and process algebra: a bisimulation perspective, volume 53 of CSLI lecture notes, Stanford, pages 131-150. Springer-Verlag, 1995.

HC94

Dang Van Hung and Zhou Chaochen.
Probabilistic Duration Calculus for Continuous Time.
Research Report 25, UNU/IIST, P.O.Box 3058, Macau, May 1994.
Presented at NSL'94 (Workshop on Non-standard Logics and Logical Aspects of Computer Science, Kanazawa, Japan, December 5-8, 1994), submitted to Formal Aspects of Computing.

HG95

Dang Van Hung and Phan Hong Giang.
A Sampling Semantics of Duration Calculus.
Research Report 50, UNU/IIST, P.O.Box 3058, Macau, November 1995.
Published in: Formal Techniques for Real-Time and Fault Tolerant Systems, Bengt Jonsson and Joachim Parrow (Eds), LNCS 1135, Spriger-Verlag, pp. 188-207, 1996.

Hoa85

C.A.R. Hoare.
Communicating Sequential Processes.
Prentice-Hall International, 1985.

Jac94

Michael Jackson.
Problems, methods and specialisation.
Software Engineering Journal, pages 249-255, November 1994.

Jac95

Michael Jackson.
Software Requirements & Specifications: a lexicon of practice, principles and prejudices.
ACM Press. Addison-Wesley Publishing Company, Wokingham, nr. Reading, England; E-mail: ipc@awpub.add-wes.co.uk, 1995.
ISBN 0-201-87712-0; xiv + 228 pages.

Jac97

Michael Jackson.
The meaning of requirements.
Annals of Software Engineering, 3:5-21, 1997.

Jon88a

Hans Jonkers.
A Concrete Syntax for COLD-K.
Technical Report METEOR/t8/PRLE/2, Philips Research Labs, January 1988.

Jon88b

Hans Jonkers.
An Introduction to COLD-K.
Technical Report METEOR/t8/PRLE/8, Philips Research Labs, July 1988.

Jon90

C.B. Jones.
Systematic Software Development using VDM.
Prentice Hall International, second edition, 1990.

Jon93

Hans Jonkers.
An Overview of the SPRINT Method.
In J.C.P. Woodcock and P.G. Larsen, editors, FME'93: Industrial-Strength Formal Methods, pages 403-427. Formal Methods Europe, Springer-Verlag, April 1993.
Lecture Notes in Computer Science 670.

KvHV91

L.J.Somers K.M.van Hee and M. Voorhoeve.
The ExSpect tool.
In VDM '91: Formal Software Development Methods, pages 683-684. Springer-Verlag, October 1991.

Lan96

K. Lano.
The B Language and Method, A Guide to Pratical Formal Development.
Springer-Verlag, Formal Approaches to Computing and Information Technology (FACIT). Ed.: S.A. Schuman, 1996.

MdL91

Kees Middelburg and G.R.Renardel de Lavalette.
LPF and MPL$_{\omega}$ - A Logical Comparison of VDM SL and COLD-K.
In VDM '91: Formal Software Development Methods, pages 279-308. VDM-Europe, Springer-Verlag, October 1991.

Abstract: This paper compares the finitary three-valued logic LPF and the infinitary two-valued MPL$_{\omega}$, the logics underlying VDM-SL and COLD-K, to acquire insight into the relationship between the different approaches that they reflect with respect to reasoning about partial functions and bringing recursive function definitions into proofs. LPF extended with recursive function definitions is embedded into MPL$_{\omega}$ to justify some ways of bringing definitions into LPF proofs.

Mil80

R. Milner.
Calculus of Communication Systems, volume 94 of Lecture Notes in Computer Science.
Springer-Verlag, 1980.

Mil89

R. Milner.
Communication and Concurrency.
C.A.R. Hoare Series in Computing Science. Prentice Hall, 1989.

Mos97

P.D. Mosses.
COFI: The Common Framework Initiative for Algebraic Specification and Development.
In M. Bidoit and M. Dauchet, editors, TAPSOFT'97, volume 1212 of Lecture Notes in Computer Science. Springer-Verlag, 1997.

MP91

Zohar Manna and Amir Pnueli.
The Temporal Logic of Reactive Systems: Specifications.
Addison Wesley, 1991.

MP95

Zohar Manna and Amir Pnueli.
The Temporal Logic of Reactive Systems: Safety.
Addison Wesley, 1995.

MW93

Ursula Martin and Jeannette M. Wing, editors.
First International Workshop on Larch.
Workshops in Computing. Springer-Verlag, Springer-Verlag New York, Inc., Attn: J. Jeng, 175 Fifth Avenue, New York, NY 10010-7858, USA, July 1993.

Abstract: The seventeen papers in this volume were presented at the First International Workshop on Larch, held at MIT Endicott House in Dedham, MA (near Boston) on 13-15 July 1992. The workshop was attended by active Larch users and developers in industry and universities from Europe and the USA. It was a forum for those who have designed the Larch languages, built tool support for them, particularly LP, and used them to specify and reason about software and hardware systems. Digital Equipment Corporation and the National Science Foundation provided financial support for the workshop. 384 pages, 77 illustrations; ISBN 0-387-19804-0; US$79.00.

Nak97

Kokichi Futatsugiand Ataru Nakagawa.
An Overview of CAFE Specification Environment - An Algebraic Approach for Creating, Verifying, and Maintaining Formal Specifications over Networks.
In ICFEM'97: International Conference on Formal Engineering Methods. IEEE Computer Society, IEEE CS Press, November 1997.

NSF

Ataru T. Nakagawa, Toshimi Sawada, and Kokichi Futatsugi.
CafeOBJ manual (for system version 1.3).
142 pages.

oLD97

CoFI Task Group on Language Design.
CASL -- The Common Algebraic Specification Language Summary.
Available at http://www.brics.dk/Projects/CoFI/Documents/CASL/Summary/, 1997.

oS97

CoFI Task Group on Semantics.
CASL -- The CoFI Algebraic Specification Language (version 0.97) Semantics.
Available at http://www.brics.dk/Projects/CoFI/Notes/S-4/, 1997.

Rei85

W. Reisig.
Petri Nets, volume 4 of EATCS Monographs: Theoretical Computer Science.
Springer-Verlag, Heidelberg, 1985.

Rei98

W. Reisig.
Elements of Distributed Algorithms -- Modeling and Analysis with Petri Nets.
Springer-Verlag, Heidelberg, 1998.

Ros97

A. W. Roscoe.
Theory and Practice of Concurrency.
Prentice-Hall, 1997.

SM98

A. Sutcliffe and N. Maiden.
The domain theory for requirements engineering.
IEEE Transactions on Software Engineering, 24(3):174-96, 1998.

Abstract: Retrieval, validation, and explanation tools are described for cooperative assistance during requirements engineering and are illustrated by a library system case study. Generic models of applications are reused as templates for modeling and critiquing requirements for new applications. The validation tools depend on a matching process which takes facts describing a new application and retrieves the appropriate generic model from the system library. The algorithms of the matcher, which implement a computational theory of analogical structure matching, are described. A theory of domain knowledge is proposed to define the semantics and composition of generic domain models in the context of requirements engineering. A modeling language and a library of models arranged in families of classes are described. The models represent the basic transaction processing or `use case' for a class of applications. Critical difference rules are given to distinguish between families and hierarchical levels. Related work and future directions of the domain theory are discussed.

Keywords: case-based reasoning; computer aided software engineering; formal specification; software reusability; software tools; transaction processing.

SMV

K.L. McMillan
The SMV System
Carnegie Mellon University, School of Computer Science, Pittsburgh, Penn., USA, February 1992

Spi88

J. Michael Spivey.
Understanding Z: A Specification Language and its Formal Semantics, volume 3 of Cambridge Tracts in Theoretical Computer Science.
Cambridge University Press, UK, January 1988.

Spi89

J. Michael Spivey.
The Z Notation: A Reference Manual.
International Series in Computer Science. Prentice Hall, Hemel Hempstead, Hertfordshire HP2 4RG, UK, 1989.

SS90

G. Stålmarck and M. Säflund.
Modelling and Verifying Systems and Software in Propositional Logic.
In B.K. Daniels, editor, Safety of Computer Control Systems 1990 (SAFECOMP'90), pages 31-36. Pergamon Press, Oxford, 1990.

Wor96

John Wordsworth.
Software Engineering with B.
Addison-Wesley Longman, 1996.

ZJ97a

P. Zave and M. Jackson.
Four dark corners of requirements engineering.
ACM Transactions on Software Engineering and Methodology, 6(1):1-30, January 1997.

Abstract: Research in requirements engineering has produced an extensive body of knowledge, but there are four areas in which the foundation of the discipline seems weak or obscure: grounding formal representations in reality, implementation bias, control of actions, and the role of domain knowledge. This article shines some light in the "four dark corners", exposing problems and proposing solutions. We show that all descriptions involved in requirements engineering should be descriptions of the environment. We show that certain control information is necessary for sound requirements engineering, and we explain the close association between domain knowledge and refinement of requirements. Together, these conclusions explain the precise nature of requirements, specifications and domain knowledge, as well as the precise nature of the relationships among them. They establish minimum standards for what information should be represented in a requirements language. They also make it possible to determine exactly what it means for requirements engineering to be successfully completed

Keywords: formal specification; nomenclature; systems analysis.

ZJ97b

P. Zave and M. Jackson.
Requirements for telecommunications services: an attack on complexity.
In Proceedings of the Third IEEE International Symposium on Requirements Engineering (Cat. No.97TB100086), pages 106-117. IEEE Comput. Soc. Press, 1997.

Abstract: In engineering the requirements for a telecommunications system, the greatest obstacle to be overcome is the sheer complexity of the required behavior. We present several ways of managing and minimizing this complexity, all of proven effectiveness. Most of the specification techniques result from specific application of general requirements principles to the telecommunications domain

Keywords: formal specification; systems analysis; telecommunication computing.