Dines Bjørner Department of Computer Science, Office S15 06-04 August 16, 2005 School of Computing,
National University of SingaporeSOFTWARE ENGINEERING
A Series of Text cum Handbooks
Software engineering: The art, craft, discipline, logic, practice and science of developing large scale software products is in increasing need of a trustworthy, believable and professional base. These volumes are devoted to fill this need. The present series of strongly related volumes combine informal, engineeringly sound approaches with the rigour of formal, mathematics based approaches.
The present volume covers the basic principles and techniques of abstraction and modeling.
First this volume provides a sound, but simple basis of insight into discrete mathematics: Numbers, sets, Cartesians, types, functions, the Lambda-Calculus, algebras and mathematical logic.
Then this volume goes on to teach and train its readers in basic property and model oriented specification principles and techniques.
The model oriented concepts, that are common to such specification languages as B, VDM-SL, and Z, will be propagated here through he use of the RAISE specification language RSL.
Finally this volume will cover basic principles of functional, imperative and parallel specification programming - the latter based on the use of CSP: Hoare's language of Communicating Sequential Processes.
The present volume covers the basic principles and techniques of specifying systems and languages.
First this volume teaches and trains its readers in advanced principles and techniques: Hierarchical versus compositional, denotational versus computational, and configurational: Abstracting and modeling contexts and states.
Then this volume goes on to teach and train its readers in basic principles and techniques of modeling the semiotics: Pragmatics, semantics and syntax of systems and languages.
An important part covers principles and techniques of modeling spatial and simple temporal phenomena.
A major section of this volume is devoted to such specialised topics as: Modularity (incl. UML's Class Diagrams); Petri Nets; Live Sequence Charts; Statecharts; and Temporal Logics, including the Duration Calculus.
This part epitomises the adage: We ``UML''-lise formal techniques. Thus the reader is brought, on a firm, precise, formal basis, on to the (trustworthy, believable and) professional use of such ideas as are also the mainstay of UML.
Finally this volume presents principles and techniques for developing the basis for sound and efficient interpreter and compiler development of functional, imperative, modular and parallel programming languages.
Volume 2 has Volume 1 as prerequisite text.
The present volume covers the basic principles and techniques of overall software development: From domains via requirements to software designs.
Thus this volume advocates a novel approach to software engineering based on the adage: Before requirements can be formulated one must understand the application domain.
This volume is therefore structured this way: From (i) the principles and techniques for the development of domain descriptions, via (ii) principles and techniques for the derivation of requirements prescriptions from domain models, to (iii) principles and techniques for the refinement of requirements into software designs: Architectures and component design.
Emphasis in the coverage of domain and requirements engineering is on `what goes into a proper domain description', respectively `requirements prescription', and on `how does one acquire and analyse the domain knowledge', respectively `the requirements expectations, and `how does one validate and verify domain and requirements models'.
The present volume is structured so as to be targetable for two rather different audiences: In one clearly marked structure - focusing only on the informal parts - this volume is targeted at undergraduate students in a second semester course on software engineering, as well as at college lecturers in that field. In another - for the full version of this volume - it is targeted at advanced students, lecturers and researchers.
This is a novel feature for textbooks.
As such Volume 3 - in the first, simple version - has no prerequisite texts. In the full version Volume 3 has Volume 2 as prerequisite text.
We plan further volumes. These plans are only the responsibility of Dines Bjørner. Springer is aware of these plans - but have no commitment. Should the volumes materialise, then it is hoped that they will appear in the current series as respective volumes.
This volume is suggested as an outcome of a very successful PhD + PostDoctoral Summer School held at the Slovak Academy Centre, Stara Lesna, June 6-19, 2004, on the subject of "Logics of Specification Languages".
We refer to The Summer School Home Page..
The summer school was based on a number of papers published in the Slovak Academy Journal: Computing and Informatics. These papers were:
For abstracts we refer to:
For the actual Summer School the above mentioned lecturers (some with colleagues) had worked out extensive lecture notes.
The intension of this, the fifth volume, is to published these extended versions of the "Computing and Informatics" papers in a seriously edited format.
A major drawback, some may think, of the present series of text cum handbooks, is their scant treatment of verification.
Hence it is planned, in parallel with the writing of Vol. 4, and the preparation and editing of Vol. 5, to also carefully edit a series of papers on verification into Vol. 6 !
The kind of papers that I have in mind are:
It is expected to add/remove a few
RSL
(Raise Specification
Language) and
DC
(Duration Calculus) verified development papers.
And it is
hoped to add a few
B
and
Z
verified development papers.
Neither authors nor previous publishers have yet been contacted ! Their permission need be secured first.
You may not have heard of the term "formal method" (we ourselves prefer the term: "formal techniques").
Therefore, please take time to browse below references.
latex2html -split 0 -toc_depth 6 /home/db/thebooks/Software_Engineering/Software_Engineering
This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.70)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html -split 0 -toc_depth 6 Software_Engineering
The translation was initiated by on 2005-08-16