| 
| Course Descriptions |
| 
| Duration Calculus: A Logical Approach to Real-Time Systems |
|  | UNU-IIST Home |
|
| Formal Software Specification Using RAISE |
II/2/1/1 Formal Software Specification Using RAISE
RAISE stands for Rigorous Approach to Industrial Software
Engineering. RAISE emphasises the use of formal (mathematical)
techniques in the development of software: in requirements analysis
and formulation, specification, design and development. RAISE offers
the RAISE Specification Language (RSL) and the RAISE method.
RAISE was initially developed in the European ESPRIT Project RAISE,
from 1985 to 1990, with the aim of providing a unifying improvement
over formal methods such as VDM, Z, CSP, CCS, Larch and OBJ. It was
later further developed in the ESPRIT Project LaCoS (Large scale
Correct Systems using formal methods), from 1990 to 1995.
RSL provides a rich, mathematically based notation in which
requirements, specifications and steps of design of software may be
formulated and reasoned about. RSL is a wide-spectrum language: it
facilitates abstract, axiomatic styles of description as well as
concrete, operational styles. It may be used from initial domain and
requirements analysis through design to a level at which it may be
translated into code.
The RAISE method provides a set of techniques and
recommendations for how to use RSL in the various life-cycle phases of
software development, as well as techniques for verifying properties
of specifications, implementations and their relationships, formally,
rigorously or informally.
RAISE comes with comprehensive documentation. Books on the language
and method are available. The first [1] on RSL is provided to
institutions from which course attendees come (one per institution or
one per every two participants, whichever is the larger number, in
either case to be given to the institution library). The second [2]
on the RAISE
method is available
by ftp and is copied for all participants.
If at all possible a number (at least one per two or three
participants) of PCs or workstations should be available for exercise
sessions. The tools
usually used for the course have been developed at UNU-IIST by staff
and fellows and are also available by ftp. They will run on PCs under
Dos, Windows or Linux as well as on Sun workstations and may be
downloaded and installed in advance or brought and installed by the
lecturer. Participants are encouraged to make their own copies.
All the course
materials are
available by ftp.
- Introduction
- Formal methods
- RAISE
- Logic
- RAISE Specification Language (RSL)
- Logical expressions in RSL
- Set theory
- RSL types
- Product and function types
- Subtypes and set types
- List and map types
- Variants and patterns
- Record types
- Applicative specifications
- State based specification
- Non-termination and non-determinism
- Modularity
- Concurrency
- RAISE tools
- RAISE method
- Introduction
- Refinement relation
- Development example -- sequential
- Development example -- concurrent
- Workshop example
- Course Attendees
- Participants must be graduates (already have a
BSc or BA) in Computer Science or a discipline with a substantial
computing component. It is useful if people have some experience in
large software projects. They are not expected to know about formal
methods in advance, but some familiarity with basic predicate logic
and simple set theory is assumed.
- Course Materials
- In addition to the two textbooks on RAISE
discussed above, participants receives copies of the course foils,
exercises and solutions.
- Course Length
- The course can be tailored to meet local
requirements, from a minimum of one week to a maximum of two weeks.
Each day consists of approximately six hours of lecture and exercise
sessions. A two week course has a much greater practical component
in the second week.
- The RAISE Language Group:
The RAISE Specification Language.
BCS Practitioner Series. Prentice Hall, 1992.
- The RAISE Method Group:
The RAISE Development Method.
BCS Practitioner Series. Prentice Hall, 1995.
- B. Dandanell, J. Gørtz, J. Storbank Pedersen, and E. Zierau:
Experiences from Applications of RAISE.
In FME'93: Industrial-Strength Formal Methods, First
International Symposium of Formal Methods Europe, volume 670 of Lecture Notes in Computer
Science, pages 52-63. Springer-Verlag, 1993.
- D. Bolignano and M. Debabi:
On the Semantic Foundations of RSL: a
Concurrent, Functional and Imperative Specification
Language.
In Proceedings of FORTE'93, Boston University, 1993.
- F. Erasmy and E. Sekerinsky:
RAISE.
In Formal Development of Reactive Systems: Case Study
Production Cell, volume 891 of Lecture Notes in Computer
Science, Springer-Verlag, 1995.
- C.W. George: The RAISE Specification Language: A Tutorial. In
Proceedings of VDM'91, volume 551 of Lecture Notes in Computer
Science, Springer-Verlag, 1991.
- C.W. George:
The NDB Database Specified in the RAISE
Specification Language.
In Formal Aspects of Computer Science, volume 4, number 1, 1992.
- C.W. George:
A Theory of Distributed Train Rescheduling.
In Proceedings of FME'96: Industrial Benefit and Advances in
Formal Methods, volume 1051 of Lecture Notes in Computer
Science, Springer-Verlag, 1996.
- C.W. George and R.E. Milne:
Specifying and Refining Concurrent Systems --
an Example from the RAISE Project.
In Proceedings of 3rd Refinement Workshop, Springer-Verlag, 1990.
- J. Gørtz:
Specifying Safety and Progress Properties
with RSL.
In Proceedings of FME'94: Industrial Benefits of Formal Methods, volume 873 of Lecture Notes in Computer
Science, Springer-Verlag, 1994.
- A.E. Haxthausen and C.W. George:
A Concurrency Case Study Using RAISE.
In Proceedings of FME'93: Industrial Strength Formal Methods,
volume 670 of Lecture Notes in Computer
Science, Springer-Verlag, 1993.
- A.E. Haxthausen and J. Storbank Pedersen and S. Prehn:
RAISE: a Product Supporting Industrial
Use of Formal Methods.
Technique et Science Informatiques, volume 12, number 3,
Afcet/Hermes, 1993.
- R.E. Milne:
The proof theory for the RAISE specification language.
Technical Report RAISE/STC/REM/12, STC/STL, Harlow, UK, 1990.
- R.E. Milne:
The semantic foundations of the RAISE specification language.
Technical Report RAISE/STC/REM/11, STC/STL, Harlow, UK, 1990.
- R.E. Milne:
Transforming axioms for data types into sequential programs.
In 4th Refinement Workshop, Workshops in Computing. Springer-Verlag, 1991.
- R.E. Milne:
The formal basis for the RAISE specification language.
In Semantics of Specification Languages, Workshops in Computing. Springer-Verlag, 1993.
- E. Zierau:
Use of the Formal Method RAISE in Practice.
In Proceedings of SAFECOMP'94, 1994.
iistinfo@iist.unu.edu, February 1997
| Formal Software Specification Using RAISE |
| |
| Course Descriptions |
| |
| Duration Calculus: A Logical Approach to Real-Time Systems |
| | UNU-IIST Home |
|