Last updated: 4th March 2016
Maintained by: Jan Storbank Pedersen, email@example.com
RAISE is a formal method. RAISE is an acronym for "Rigorous Approach to Industrial Software Engineering". It provides facilities for the industrial use of Formal Methods in the development of software systems. The aim of RAISE is to enable the construction of:
The RAISE language and tools focus on supporting the specification, design and implementation stages of the software development process. RAISE aims to improve the software development process by supporting a discipline which can be planned and carried out in an industrial context. In particular, RAISE supports development all the way to final compilable code. The entire development from specification through to implementation will be formally recorded when using RAISE, and this is the first prerequisite for optimal maintenance activities.
RAISE is a result of 20 years of research and experience in systematic software development using the paradigm of "stepwise refinement" ([Dij76],[Wir71],[Jon86]). More specifically to RAISE, there have been two projects sponsored by the European Commission - RAISE (ESPRIT I 315, 1985 - 1990) and LaCoS (ESPRIT II 5383, 1990 - 1995, LArge scale COrrect Systems using formal methods) which have involved over 200 person years of effort.
The RAISE method includes guidelines for most relevant software and systems development activities, such as requirements capture and project management.
The method is based on the stepwise refinement paradigm. According to this paradigm, software is constructed through a series of steps, where each step represents a refinement of the previous one. In RAISE, each step is produced under the "invent-and-verify" philosophy, i.e. a specification is developed into a design "manually" (the invention aspect) and the relation between the two can afterwards be verified (this aspect is sometimes called a posteriori verification). RAISE supports a type of refinement known as theory extension (see question on theory extension).
In RAISE, there is tool support for this verification. Evidently, such formal verification offers a sound basis for obtaining correct software. Note, however, that formal proof is only one possibility: verification can be done less formally (i.e. producing a rigorous argument) if this suits the practical and economic constraints associated with a particular industrial application.
The RAISE method is not prescriptive, or cookbook-like, but provides a framework and guidelines for the software development process. The adaptability of the method allows the chosen techniques and level of rigour to be governed by the pragmatic concerns of each project. The RAISE method thus allows users to select the level of formality that is appropriate to particular circumstances, project standards, etc.
RSL stands for RAISE Specification Language. It is a wide-spectrum specification language. It is inspired by and unifies features of several specification languages (VDM, CSP & ACT-ONE). RSL is "wide-spectrum" in the sense that it may be used to express high-level, abstract specifications, as well as low-level designs (e.g. using explicit imperative constructs such as loops). One advantage of this is that users only have to know one notation in addition to the programming language used for the implementation, since the whole development is carried through in RSL. The structuring facilities of RSL support decomposition and re-use.
RSL specifications should be considered as mathematical models of software systems. What distinguishes specifications at different levels of development is their level of abstraction.
The kinds of software development projects that will be able to benefit the most from RAISE are developments of systems with inherent complexity, either for data, algorithms, or concurrency, and with strong reliability requirements. Typical applications could be: systems software, embedded systems or safety critical software.
Software development of the types that lend themselves easily to 4th generation tools (such as certain administrative applications involving a large amount of user interface design) might not benefit from RAISE to the same degree.
RAISE has been used successfully on various, diverse applications some of which are listed below:
More details of some of these projects are available.
Non-functional requirements such as timing and space constraints cannot be directly dealt with in RSL specifications. Such requirements are instead taken into account in RAISE via their impact on how developments are carried out. So, different development routes may be taken to fulfil such requirements.
It is possible, however, to model time directly in RSL and then reason about real time properties.
RAISE tools have been commercially available since mid 1991.
There is an integrated set of state-of-the-art tools supporting the language and method. The RAISE tools support a completely formal working style, with tracking and validation of proofs, etc., as well as more lax working styles.
The RAISE tools form a collection of tools for editing and manipulating a variety of entities that are relevant during a development process: modules, relations between modules, theories, justifications and hints. The environment provided by the RAISE tools provides facilities for tracking and documenting complete developments of software systems. The environment supports the maintenance and evolution of software systems throughout their lifetime. The environment is currently based on Unix and X and is operating on Sun workstations.
There are tools for:
The editors can be used as syntax directed editors, in which the user selects and refines syntax categories (using mouse and keys), or as normal text editors, in which the user may type and edit as well as using standard editor facilities such as cut and paste. The editors ensure syntactic correctness and continuously check for static conditions (typing rules, visibility rules etc.) displaying relevant error messages at the points of error. References to other entities are made via "contexts".
The justification editor is used to interactively develop coherent justifications using either backwards or forwards reasoning. The justification editor has some important components:
- simplifier. This component may be used to reduce conditions to
simpler conditions (in the best case to
- implementation condition expander. This component may be used to generate the detailed conditions under which an implementation relation between two modules will actually hold.
The translators are used to generate compilable programming language code from low-level specifications expressed in RSL. There are translators for C++ and Ada. For RSL modules where high performance requirements exist, manual translation or adaptation of generated code may still be necessary.
The document formatter may be used to extract RAISE entities in a form appropriate for producing hard-copy documents containing informal text and RAISE entities. Currently only the LaTeX formatting system is supported. Note, however that entities other than justifications are available in ASCII although special characters are translated to ASCII sequences.
RSL supports the following styles:
pop(push(x,s)) = sfor all stacks
x. With this method, any of a number of models can satisfy the axioms. Within the RAISE method, an algebraic specification is generally developed into a model-oriented one as more concrete data structures are designed.
RSL supports modularisation with parameterisation at the structuring level.
RSL modules are the basic building blocks and abstraction units around which RAISE developments are built. Inside a module the RSL entities: types, values, variables, channels, objects and other modules may be defined. RSL modules correspond to what is called "modules", "packages" or "classes" in programming languages. RSL specifications can be constructed in a hierarchical manner since modules can refer to the entities of other modules in defining their own entities. The modules can be parameterised thus supporting generalised specification. This is an important mechanism in creating reusable modules. A module can be adapted to a given application by renaming and hiding some of its entities.
The basic building block in RSL is the class expression and is often referred to as an RSL module. All declarations are made within a class expression. This includes definitions of types, constants, functions, variables, channels and objects. Schemes are named class expressions and represent models of class expressions. Any scheme or class expression may be instantiated as a named object which represents a single instantiation of the scheme or class expression and has at least all the properties defined in that scheme or class expression.
Class expressions may be parameterised by other class expressions. Such formal parameters define required properties from the actual parameters. These properties are to be made available in the parameterised class expression.
RAISE supports the following pre-requisites for object-orientation: (subtype) polymorphism, inheritance and encapsulation. In general, RAISE supports object-oriented methods rather than incorporating all object-oritneted language features.
RSL does not support parametric polymorphism (as found, for example, in ML). However, function "templates" can be defined which can be instantiated with particular types. For example a module which defines a set of functions over the type ELEM may have as a parameter a module which defines the type ELEM:
scheme LIST_FUNS(E : class type Elem end) =
reverse : E.Elem-list -> E.Elem-list
reverse(seq) is ...
The functions are now defined for any type which is used to instantiate ELEM. The use of parameterisation is more general than parametric polymorphism since, for example, the parameter can inclyde axioms specifying that ELEM forms a total order.
RSL allows function overloading so any function name can be multiply declared as long as the overloading can be statically resolved, i.e. different function definitions must apply to different types and/or numbers of parameters.
Yes: one of the chief design aims of RSL was to integrate concurrent and sequential features in a single specification language. Parallel activities can be specified via the RSL concept of a process. A process can be considered as an entity capable of (i) communicating with other processes along channels, and (ii) possibly accessing a state. Communication is synchronised. The RSL process concept is based on a notion of process algebra as found in CSP ([Hoa85]).
RSL processes can be specified explicitly using expressions involving input, output, internal and external choice and parallel composition, or axiomatic specifications may be given. For axioms specifying concurrent behaviour RSL includes a special "interlock" operator.
No: there are currently no compilers or interpreters for RSL. However, it is possible to write RSL specifications which are very similar to imperative code. It is relatively simple to translate these to code depending on the language chosen. This translation can either be automatic using the translators to C++ or Ada, or manual. Then the produced code can be compiled or interpreted.
The formal, mathematical description of RSL is covered in "Semantic Foundations of RSL" [Mil90a] where a denotational semantics is given and "The Proof Theory for the RAISE Specification Language" [Mil90b] where an axiomatic semantics is given. The construction of the denotational model and a demonstration of its existence are presented in [BD92a] and [BD92b].
Any formal system that aims to provide a means of development as well as a means of specification must provide a notion of implementation. That is, if module A0 is developed to module A1 then we need to know if A1 is a correct development. We say that A1 is correct if it implements A0, i.e. A0 and A1 are in the implementation relation. There are in fact several variations on the notion of implementation (also called refinement or reification); the one in RAISE is theory extension and is chosen to meet two particular requirements. If A1 implements A0 then we want the following to hold:
The following definition is taken from [RMG95]:
- A theory T2 extends a theory T1 if T2 has more entities and/or properties than T1.
- A theory T2 conservatively extends a theory T1 if every property of T2 that can be expressed using entities defined in T1 is a property of T1. In other words T2 adds no new properties to the entities from T1. An extension that is not conservative is described as "non-conservative".
Rather than proof, RAISE uses the term "justification" which means an argument showing the truth of some condition. Such an argument may be totally formal, i.e. be a mathematical proof based on application of proof rules for RSL. Justification can, however, also be done more informally if this suits the practical or economic constraints associated with a particular industrial application. The idea of using informal arguments is to indicate how formal proofs could have been constructed. In other words, whenever informal arguments are used one should be convinced that it is possible to replace them with formal proofs. Such arguments, that depend on a formal underpinning but allow for informal steps, are called rigorous.
There are two types of conditions which can be generated and justified using RAISE:
- formal conditions (predicates stipulated in RAISE theories and development relations). These must be manually generated.
- confidence conditions (predicates whose truth increases the confidence that there are no extreme and unintended semantics in a piece of RSL). These are automatically generated.
RAISE potentially reduces the effort devoted to testing software because programs already written can be re-used, and because some of the development process might be shown correct in a formal sense using the RAISE justification tools. This does not mean that testing should be reduced in scope, but that fewer errors in the code leads to fewer test failures and less re-work and re-testing. The production of a formal specification should also help in guiding the generation of test cases.
Z is basically a specification language. It is generally good for producing specifications but it is more productive to use another notation for development. RSL, on the other hand, can be used for both specification and development.
RSL is more expressive than Z by virtue of its facilities for underspecification and concurrency. As a result, it is easier to translate a Z specification into an RSL specification than vice versa.
The styles of specifications in Z and in RSL are often very different. Z specifications are written in a model-based, primarily applicative, style, whereas RSL provides a choice between applicative and imperative stules on the one hand and algebraic and model-based on the other. By allowing differing levels of abstraction to be specified, RSL supports development from one level to another.
Combination of parts of a specification (in Z, schemas; in RSL, modules) is "easier" in Z than in RSL (there is less syntactic overhead), but arguably less useable on a large scale. The structuring mechanisms of RSL are somewhat like those of Extended ML; for example, modules can be parameterised on other modules, and where an RSL module uses an identifier from a module supplied as a parameter it must prefix it with the parameter name.
Both Z and RSL prefer to split a state into smaller substates, rather than include many vacuous predicates detailing parts of the state that do not change when particular functions are applied. Z generally deals with each substate (and, often, each function applicable to a particular substate) in a separate schema, while RSL often combines functions on substates into one or more larger modules. This means that Z specifications appear generally to be made up of many small schemas, in contrast to RSL specifications which usually consist of fewer, larger modules.
RSL is derived from VDM with added facilities such as concurrency, axiomatic and imperative styles. Modularity is also an integrated feature of the RSL language and RAISE method whereas it is not supported as part of standard VDM; some attempts have been made to add modularistion to VDM but they have not yet been universally accepted. Several aspects of VDM notation which are more or less universally agreed on in the VDM community are included in RSL: type constructors for mappings, sets, lists, Cartesian products, etc., together with the applicative forms of expressions and function definitions (including pre-/post- style).
A substantial body of case studies using VDM has been published. Together with more systematic accounts of the method aspect of using VDM they present a large collection of techniques and strategies for modelling, specifying and developing software; techniques and strategies which may all readily be used with RSL.
Whilst the refinement calculus uses the calculational (or transformational) method of refinement, RAISE uses the invent-and-verify method. The two formal methods essentially have different aims; whilst RAISE is intended for large software developments, the refinement calculus is mainly used for mathematical derivation of programs.
Some participate in the comp.specification newsgroup. If there is much interest, a RAISE mailing list may emerge. For more information contact: Jan Storbank Pedersen (firstname.lastname@example.org)
WWW page: http://spd-web.terma.com/Projects/RAISE/index.html
The RAISE documentation consists of:
The book was originally published as:
The RAISE Specification Language The RAISE Language Group Prentice Hall ISBN: 0-13-752833-7
It is now available from Terma (see contact information below)
It is also meant to serve as a handbook for people wanting to justify properties of RSL specifications. The book describes a syntax for RAISE justifications and provides formal proof rules which may be used in justifications.
This book was originally published as:
The RAISE Development Method The RAISE Method Group Prentice Hall ISBN: 0-13-752700-4
A free PDF file can be requested from Terma (see contact information below)
Terma offers courses in RSL and the RAISE method from one to five days -- contact Jan Storbank Pedersen +45 4594 9657 (email@example.com):
- RAISE Tutorial (1 day)
- RSL and Method Course (3 days)
- RSL Course (5 days)
- RAISE Method Course (5 days)
- RAISE Justification Course (4 days)
Consultancy services are also available from Terma.
See the RAISE WWW page (address http://spd-web.terma.com/Projects/RAISE/index.html)
Contact any of the people currently using RAISE or:
Jan Storbank Pedersen at Terma (firstname.lastname@example.org)
Jan Storbank Pedersen
Tel: +45 4594 9657
Fax: +45 8743 6001
This FAQ was compiled from the knowledge of members of the LaCoS project, various reports and documents including the RSL book [RLG92], various Terma publicity leaflets and the RAISE Development Method [RMG95].
Any suggestions or corrections to this FAQ should be made to Jan Storbank Pedersen at Terma.
Jan Storbank Pedersen
Tel: +45 4594 9657
Fax: +45 8743 6001
[Also see the bibliography.]
[BD92a] D. Bolignano and M. Debabi. On the Foundations of the RAISE Specification Language. LACOS Report Bull/DB/27, Bull Corporate Research Center, June 1992.
[BD92b] D. Bolignano and M. Debabi. Higher Order Communicating Processes with Value-passing, Assignment and Return of Results. In Proceedings of the ISAAC'92 Conference. December 1992.
[Dij76] E.W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976
[Hoa85] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall series in Computer Science. Prentice-Hall International, 1985
[Jon86] C.B. Jones. Systematic Software Development using VDM. Prentice-Hall Series in Computer Science. Prentice-Hall International, 1986
[Mil90a] R. Milne. The proof theory for the RAISE specification language. RAISE Report REM/12, STC Technology Ltd, 1990.
[Mil90b] R. Milne. The semantic foundations of the RAISE specification language. RAISE Report REM/11, STC Technology Ltd, 1990.
[RLG92] The RAISE Language Group. THE RAISE Specification Language. The BCS Practioner Series. Prentice Hall, 1992 ISBN 0-13-752833-7
[RMG95] The RAISE Method Group. The RAISE Development Method. BCS Practitioner Series. Prentice Hall, 1995 ISBN 0-13-752700-4
[Wir71] N. Wirth. Program Development by Stepwise Refinement. Communications of the ACM, (14):221 - 227, 1971