Expected Publication Date: Early Spring 2005
Outline of a Series of Text- &
Handbooks on
Formal & Practical Aspects of
SOFTWARE ENGINEERING
Springer-Verlag, Berlin - Heidelberg
Dines Bjørner,
Professor of Computing Science
E-Mail: db"ad"imm.dtu.dk
Monday, May 31, 2004, 3:30 am
Current volume 1-2-3 *.ps files are DRAFTS
All three volumes will be edited during
Winter and Spring 2004.
Final version will go to Publisher no later
than 30 June 2004.
Publisher is SPRINGER-VERLAG:
[EATCS] Texts in Theoretical Computer
Science
During Spring of 2004 this home page will
change.
I will gradually phase out URLs to volumes
1+2+3.
And I will gradually phase in:
(1) General Course Material - for prospective
lecturers.
(2) URLs to relevant Formal Methods pages - See
Sect. [5.].
(3) ... and much, much more ...
- There is a need for text- & handbooks that tell the formal methods
"story" from the broader software engineering viewpoint.
- Volumes 1-2-3 should serve the above need.
- There is, independently thereof, a need for a text- cum handbook
which links the potential uses of formal methods to the
usual - or a new - process model(s) for software engineering.
- Volume 3, in particular, should serve the latter need.
- The usual software engineering "management stuff" need be
re-told - now in the context of formal methods.
- Volume 4 should serve that need.
- Claim:
Some people claim that
-
Formal Methods
-
do not go, or, that it has not been shown how
they go together with
-
"Best Practices"
-
of current
Software Engineering
approaches.
- Counterclaim:
Volumes 1+2+3 will show you
-
that they do,
-
how they do,
-
and what one does in order to practice
-
Formal Methods
when doing
Software Engineering.
- Claim:
Some people claim that
-
Software Engineering
-
managers
do not know how to incorporate
-
Formal
Methods
-
into any
-
"Best
Practice"
-
process model.
- Counterclaim:
Volume 4,
in more
details than Volume 3,
tells managers how to incorporate
-
Formal Methods,
as an integral part,
-
into the planning, monitoring and
control of small, medium, large scale, and very large scale
-
Software Development
projects.
-
So now - with these volumes - there can no
longer be any excuses !
-
Formal Methods fit naturally into any
Software Development project.
More specifically:
- I expect, currently, four volumes:
- SE 1:
Abstraction and Modelling
- SE 2:
Specification of Systems and Languages
- SE 3:
Domains, Requirements, and Software Design
- SE 4:
Project and Product Management
- Currently volumes 1+2+3 are being written:
-
Volume
1: Abstraction and
Modelling
-
Volume
2: Specification of Systems and
Languages
-
Volume
3: Domains, Requirements, and Software
Design
- S-V has been promised
final versions of Volumes 1-2-3 to be ready by
30 June 2004.
- For volume 4 I expect
- first "full" draft version to be ready by 31 December 2004,
- with a final version 30 June 2005.
- This is not a series of text- & handbooks propagating a special
notation.
- These text- & handbooks will use
- The
RAISE Specification Language RSL
- ER cum UML-like
Class Diagrams
- Condition Event, Place Transition
and Coloured
Petri Nets
- Message Sequence and
Live Sequence Charts.
-
Statecharts.
- The Temporal Logic of the
Duration Calculus.
- The emphasis is on methods, principles, techniques.
- The emphasis will be on specification and informal, yet rigorous
transformation of specifications.
- The present four volumes will not cover verification (sic !).
- We are "UML-ising" uses of formal techniques rather than using
formalised versions of UML.
Volumes 3 and 4, as will be noted below, can be used in either of
two ways: Without or with formulas.
This gives rise to the following sequence of uses of the four, thus
actually six volumes, in up to six one semester courses:
- I3: Non-formula, ie., Informal version of Volume 3.
- I4: Non-formula, ie., Informal version of Volume 4.
- F1: Volume 1.
- F2: Volume 2.
- F3: Formula, ie., Formal version of Volume 3.
- F4: Formula , ie., Formal version of Volume 4.
The following sequences of courses are therefore possible:
- I3 Undergraduate, College or Univ. BSc. SE, single module
- I3+I4 Undergraduate, College or Univ. BSc. SE, double module
- F1 Graduate, Univ. MSc. SE / MSc. CS
- F1+F2 Graduate, Univ. MSc. SE / MSc. CS
- F1+F2+F3 Graduate, Univ. MSc. SE / MSc. CS
- F1+F2+F3+F4 Graduate, Univ. MSc. SE / MSc. CS
If, for example, for a graduate course, in F3 or F4, course I3,
resp. I4 is assumed to have been followed,
then that graduate course in F3, resp. F4, should be organised
as a single module course,
otherwise as a double module course.
Other combinations are possible.
Not all material in all volumes need be covered.
Some material, for example early material in vol.1, may be covered in
already existing courses on Discrete Mathematics.
Material not covered can - anyway - be studied by students.
In all volumes we present numerous examples.
And in all volumes we provide explicit listings of development
procedures. Too numerous to recall.
Therefore:
- Initially the volumes can be used as textbooks.
- Thereafter students can use them as handbooks, for future
reference.
The First volume, SE 1., will contain an approximately 900 entry
Glossary:
We believe that this Glossary is quite a unique feature of this series of
text and handbooks.
Left:
One of my wife's Patchwork &
Quilts:
Multi-
coloured
Asters
Abstract:
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. This book is one, in presently a series of
three volumes, devoted to fill this need. The present series of
strongly related text
books 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 the book provides a sound, but simple basis of insight into
discrete mathematics: Numbers, sets, Cartesians, types, functions, the
Lambda--Calculus, algebras and mathematical logic.
Then the book 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 the book 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 book is targeted at at university undergraduate students and at college lecturers.
- Part I:
Opening
- 1.
Introduction
- Part II:
Discrete Mathematics
- 2.
Numbers
- 3.
Sets
- 4.
Cartesians
- 5.
Types
- 6.
Functions
- 7.
Lambda-Calculus
- 8.
Algebras
- 9.
Logics
- Part III:
Simple RSL
- 10.
Atomic Types & Values in RSL
- 11.
Function Definitions in RSL
- 12.
Property & Model Oriented Abstractions
- 13.
Sets in RAISE
- 14.
Cartesians in RAISE
- 15.
Lists in RAISE
- 16.
Maps in RAISE
- 17.
Higher-order Functions in RAISE
- Part IV:
Specification Types
- 18.
Types in RAISE
- Part V:
Specification Programming
- 19.
Applicative Specification Programming
- 20.
Imperative Specification Programming
- 21.
Parallel Specification Programming
- Part VI:
And So On !
- 22.
Etcetera !
- Part VII:
Appendices
-
References
- A.
Glossary
- B.
Indexes
Left:
One of my wife's Patchwork &
Quilts:
Green
and
Pink
Harlequin
Abstract:
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. This book is one, in presently a series of
three volumes, devoted to fill this need. The present series of
strongly related text
books combine informal, engineeringly sound approaches with the
rigour of formal, mathematics based approaches.
The present volume covers the basic principles and techniques of specifying systems and languages.
First the book teaches and trains its readers in advanced principles
and techniques: Hierarchical versus compositional, denotational
versu
computational, and configurational: Abstracting and modeling
contexts
and states.
Then the book 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 the book 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 the book presents principles and techniques for developing
the
basis for sound and efficient interpreter and compiler development
of
functional, imperative, modular and parallel programming languages.
The present book is targeted at late undergraduate to early graduate university students,
at college lecturers and at researchers of programming methodology.
Volume 2 has Volume 1 of this series as a prerequisite text.
Chapters 12-14 incl.: Main Author: Christian Krog Madsen
- Part I:
Opening
- "empty"
- 1.
Introduction
- Part II:
Specification Facets
- 2.
Hierarchies & Compositions
- 3.
Denotations & Computations
- 4.
Configurations: Contexts and States
- Part III:
A Universal Domain Facet
- 5.
Time, Space & Time/Space
- Part IV:
Linguistics
- 6.
Pragmatics
- 7.
Semantics
- 8.
Syntax
- 9.
Semiotics
- Part V:
Specification Techniques
- 10.
Modularisation
- 11.
Automata & Machines
- 12.
Petri Nets
Main Author: Christian
Krog Madsen
- 13.
Message Sequence and Live Sequence Charts
Main Author: Christian Krog Madsen.
- 14.
Statecharts
Main Author: Christian
Krog Madsen.
- 15.
Varieties of Temporal Logics
- "empty"
- Part VI:
Language Definitions
- 16.
SAL: Simple Applicative Language
- 17.
SIL: Simple Imperative Language
- 18.
SMIL: Simple Modular, Imperative Language
- 19.
SPL: Simple Parallel Language
- Part VII:
Closing
- 20.
Conclusion
- Part VIII:
Appendices
-
References
- A.
Indexes
Left:
One of my wife's Patchwork &
Quilts:
Fence
Rails
Abstract:
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. This book is one, in presently a series of
three volumes, devoted to fill this need. The present series of
strongly related text
books combine informal, engineeringly sound approaches with the
rigour of formal, mathematics based approaches.
The present volume covers the basic principles and techniques of overall software development: From domains via
requirements to software designs.
Thus the book advocates a novel approach to software
engineering
based on the adage: Before requirements can be formulated one must
understand the application domain.
The book 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 book is structured so as to be targetable for two rather
different audiences: In one clearly marked structure -- focusing only
on the informal parts -- the book 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 the book
-- 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 a prerequisite text.
- Part I,
OPENING
- Chapter 1,
The TripTych Software
Engineering Paradigm
- Chapter 2,
Documents
- Part II,
CONCEPTUAL FRAMEWORK
- Chapter 3,
Methods & Methodology
- Chapter 4,
Models & Modelling
- Part III,
DESCRIPTIONS: THEORY &
PRACTICE
- Chapter 5,
Phenomena & Concepts
- Chapter 6,
On Defining and On
Definitions
- Chapter 7,
Jackson's Description
Principles
- Part IV,
DOMAIN ENGINEERING
- Chapter 8,
An Overview of Domain
Engineering
- Chapter 9,
Domain Stakeholders
- Chapter 10,
Domain Attributes
- Chapter 11,
Domain Facets
- Chapter 12,
Domain Acquisition
- Chapter 13,
Domain Analysis & Concept
Formation
- Chapter 14,
Domain Validation &
Verification
- Chapter 15,
Towards Domain Theories
- Chapter 16,
The TripTych Domain
Engineering Process Model
- Part V,
REQUIREMENTS ENGINEERING
- Chapter 17,
An Overview of
Requirements Engineering
- Chapter 18,
Requirements Stakeholders
- Chapter 19,
Requirements Facets
- Chapter 20,
Requirements Acquisition
- Chapter 21,
Requirements Analysis &
Concept Formation
- Chapter 22,
Requirements Validation &
Verification
- Chapter 23,
Requirements
Satisfiability & Feasibility
- Chapter 24,
The TripTych Requirements
Engineering Process Model
- Part VI,
COMPUTING SYSTEMS DESIGN
- Chapter 25,
Hardware/Software Co-design
- Chapter 26,
Software Architecture Design
- Chapter 27,
A Case Study in
Component Design
- Chapter 28,
Domain Specific Architectures
-
To be finished late May 2004
Chapter 29,
&c.: Programming,
Coding, and All That !
-
To be finished early June 2004
Chapter 30,
The TripTych Computing
Systems Design Process Model
- Part VII,
CLOSING
-
To be finished early June 2004
Chapter 31,
The TripTych Development
Process Model
- Chapter 33,
Conclusion
- Part VII,
APPENDICES
-
References
- Appendix A,
Indexes
Volume 3 represents a break with past traditions in teaching
software engineering, and it represents
a break with my own, past,
practice of teaching software engineering only by using formal techniques.
The "non-formula" version of Volume 3 will cover essentially the
same "ground", that is: Principles and techniques as will
the
"formula" version of Volume 3. The 'thesis' being that if the
major principles propagated in the "formula"
version
of Volume III are worth "their salt", then they should be able to
"stand on their own", ie., without the formalisation.
The techniques of the "formula" version of Volume III, go well
beyond those of the "non-formula" version of Volume III.
Needless to say:
- It is only through formal reasoning that we can hope to
achieve a dramatic increase in trust in our software.
Thus:
- The "non-formula" version of Volume 3 will emphasize the
process "technology" (ie., principles), while
- the "formula" version of Volume 3 additionally will
emphasize the production "technology" (ie., techniques).
The present state of this volume is: It is mere
speculation !
This volume will, as for volume 3, have two versions:
- One without formulas,
- one with formulas.
The formulas will meta-model:
- The ontology of software development.
- Version control and configuration management.
- Planning, monitoring and control.
- Specification and program analysis tools.
- Specification and verification tools.
- Document tools.
- Acquisition gathering and analysis tools.
- And many other facets of software engineering management.
A tentative layout is suggested:
-
Part I,
OPENING
- Chapter 1,
Introduction
- Chapter 2,
The Software Life Cycle:
Ontologies of Development, etc.
-
Part II,
SOFTWARE DEVELOPMENT
PROJECT MANAGEMENT
- Chapter 3,
Engineering Management:
Study, Experiment, Apply
- Chapter 4,
Configuration
Management:
Version Monitoring and Control
- Chapter 5,
People Management:
Capability Maturity Model
- Chapter 6,
Risk Management
- Chapter 7,
Quality Management
- Chapter 8,
Project Planning, Monitoring and
Control:
Project Graphs, Resource Allocation & Scheduling, etc.
- Chapter 9,
Development Cost Management
- Chapter 10,
Contracts & Contract Management
-
Part III,
SOFTWARE
PRODUCT MANAGEMENT
- Chapter 11,
Market Analysis
- Chapter 12,
Product Cost Estimates
- Chapter 13,
Consultancy &
Instantiation Costs
- Chapter 14,
Marketing & Sales
- Chapter 15,
Maintenance & Service
-
Part IV,
SOFTWARE
HOUSE MANAGEMENT
- Chapter 16,
Business Plans
- Chapter 17,
Financial Matters
- Chapter 18,
People Management
-
Part V,
TOOL
SUPPORT TECHNOLOGIES
- Chapter 19,
Specification &
Verification Tools
- Chapter 20,
Specification Analysis Tools
- Chapter 22,
Other Document Tools
- Chapter 23,
Domain Engineering Tools
- Chapter 24,
Requirements Engineering Tools
- Chapter 25,
Software Design Tools
- Chapter 26,
Planning, Monitoring and
Control Tools
- Chapter 27,
Cost Estimation Tools
-
Part VI,
STANDARDISATION &c.
- Chapter 28,
ISO 9000, 9001, 9000-3
- Chapter 29,
IEEE and ACM Standards
- Chapter 30,
Software Tool Standards:
UML, VDM, ..., Z
-
Part VII,
CLOSING
- Chapter 31,
Conclusion
-
References
-
Part VIII,
APPENDICES
- Chapter A,
Glossary
- Chapter B,
Indexes
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.
[5.1] Formal Methods Home Pages
-
General
-
Formal
Methods
or
Formal
Methods
-
"The" Formal Methods Home
Page
-
FME: Formal Methods
Europe
-
Industry
-
ForTIA: a Formal
Techniques Industry Association
-
SRI Intl.: Formal Methods and
Dependable
Systems
-
Government
-
US Govt.: NASA Langley Formal Methods
Site
-
US Govt.:
NASA Formal Methods
Guidebooks
-
US Govt.: Center for High Assurance
Computer Systems.
-
ICASE: Formal Methods for Aviation
Safety
-
Natl. Inst. of Aerospace (US Govt.):
Formal Methods for Aviation Safety
-
Universities and Research Centres
- ordered
(approx.) by "city"/country:
-
Århus
University (DK):
Formal
Methods
-
Bell
Labs.:
Formal Methods at Bell
Labs.
- University of
Bremen
(FRG):
Formal Methods
- Univ. of
Cambridge
(UK):
Formal Methods
Literature
- University of
Eindhoven
(NL):
Formal
Methods
- Rice Univ.,
Houston,
TX (USA):
Computer-Aided
Verification and Reasoning
Group
-
India:
Formal
methods
-
Ireland:
Irish Formal Methods Interest
Group
-
Italian
Research Council:
CNR Formal
Methods and Tools Group
-
Korea
Univ.:
Theory and Formal Methods
lab.
- University of
London,
Royal Holloway (UK):
Formal
Methods
-
London
Southbank University (UK):
Formal
Methods
-
Manchester
Univ. (UK):
Formal
Methods
- University of
Maryland
(ML, USA):
Formal Methods in
Interface Design
- University of
Minho
(PT):
Logic and
Formal Methods
-
Ohio
State and Clemson University (USA):
On
Formal Methods
-
Pittsburgh:
CMU + SEI (PA, USA):
-
Formal Methods in
Describing Architectures
-
Video Course on Formal
Methods and Software
Engineering
-
Strategic Directions in
Computing Research Formal Methods Working Group
- University of
Toronto
(CND):
Formal
Methods
- University of
Twente
(NL):
Formal Methods and
Tools
- University of
Waikato
(NZ):
Formal
Methods Lab.
-
Organisations
- ERCIM Working Group:
Formal Methods for
Industrial Critical Systems
(FMICS)
-
A Software Engineering Resource List
for Formal Methods and Formal Methods in Software
Architecture
-
Personal, Individual
- Dines Bjørner:
My Research Interests:
Formal Methods
- Alan Dix:
Formal Methods in
HCI
- Georges Mariano:
mariano's bookmarks: Formal
Methods
- Paul Trafford:
Research Page in Formal
Methods
- R.B.Jones:
A personal home page on Formal
Methods
-
Publishers
- Kluwer:
Journal: Formal Methods in Systems
Design
- Springer:
Journal: Formal Aspects of
Computing
[5.2] Papers/Reports/Company ''Flyers'' on Formal
Methods
-
Formal Methods and the Certification of
Critical
Systems,
319
pages, December 1993 - I can recommend also its Appendix on Logic
-
Formal Methods and their Rôle in the
Certification of Critical
Systems,
60
pages, 1995
-
NASA Langley's Research and
Technology-Transfer Program in Formal Methods
(1995)
-
SRI
Intl.: Formal Methods and Dependable
Systems
-
Formal Methods
Publications
-
Somewhat dated:
Formal Methods Education Resources
...
...
IMM
:
Informatics and Mathematical
Modelling
Rooms 106-110, 1st Floor, Building
322,
Richard Petersens Plads
Technical University of
Denmark
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
latex2html -split 0 -toc_depth 6 /home/db/the-se-books/the-se-books
Back to DB Home Page
This document was generated using the
LaTeX2HTML translator Version 2K.1beta (1.47)
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 the-se-books
The translation was initiated by on 2004-05-31
2004-05-31
