If you know of other projects which have used RAISE or RSL and which you would like to see included here, please mail a short summary to Jan Storbank Pedersen
RAISE (Rigorous Approach to Industrial Software Engineering) was the Esprit I project which completed the development of the RAISE software development method, its associated formal specification language RSL and its supporting tool set. The RAISE project ran from 1985 until 1990.
LaCoS (Large Scale Correct Systems), Esprit II project 5383, was the successor project to the RAISE project, and has concentrated on applying the RAISE method; its aim is to demonstrate the RAISE method as a viable, industrial technique in the scalable production of large, correct IT systems.
The partners in the LaCoS project were: CRI (DK), Lloyd's Register (UK), Matra Transport (F), Bull S.A. (F), INISEL S.A. (E), Space Software Italia (I), CAP Programator (DK), BNR Europe (UK, withdrawn) and Technisystems (G, withdrawn).
The LaCoS project ran from 1990 until 1995.
MORSE (Method for Object Reuse in Safety-critical Environments) concentrated on applications of various formal and standardised techniques to safety-critical systems. These techniques were used to state, prove and reason about safety properties of these systems.
Some uses of RSL within the MORSE project included:
Advanced Methods in ESSDE
A project entitled "Advanced Methods in ESSDE" has been carried out for ESA (the European Space Agency) by a consortium led by EDS-Scicon (UK). One of the main aims of the project was to assess the feasibility of using formal methods in ESA projects in the future. The project consisted of two phases, the first of which ended by the end of 1992.
The first phase evaluated a number of existing formal methods including their available toolsets. The outcome of the evaluation was that RAISE and LOTOS were selected as complementary methods for further studies in phase two.
In phase two each of these two methods and their tools were further evaluated based on their use on an on-board demonstration application to be developed in Ada. The ESSDE (European Space Software Development Environment) is currently based on Concerto (from SEMA Group, F) and part of the second phase therefore consisted of integrating a set of LOTOS tools from ITA (NL) and the RAISE tools from CRI (DK) with Concerto. This enabled the application partner, CRISA (ES), to use both LOTOS and RAISE within the same development environment.
The current ESA life-cycle is defined in the "ESA software engineering standards" (ESA PSS-05-0, issue 2), and even though it does mention the possibility of using formal techniques, it does not explicitly integrate their use in the life-cycle. One goal of this project was to provide more explicit guidelines on the use of formal methods within the ESA life-cycle, and try these out on the above mentioned demonstration application.
RAISE was used to specify and develop part of a standard on-board instrument control unit, and the Ada translator was used to produce a prototype of the code.
Various reports from this project are available at ftp://ftp.estec.esa.nl/pub/wm/wme/FORMAL_METHODS/
PRaCoSy : People's Republic of China Railway Computing System
PRaCoSy is a collaborative project between the PRC Ministry of Railways and the United Nations University International Institute for Software Technology (UNU/IIST).
Long term aims are development of software engineering skills for automation of Chinese railways and development of their software centre. Immediate aim is development of a Computer Aided system for Stage Plans (CASP), specifically a stage plan running map. This is a method of monitoring the movement of trains and rescheduling their arrivals and departures according to actual running and operational constraints.
CRI, now part of Terma, was prime contractor for a consortium of industrial companies and research institutions developing the Ørsted microsatellite, named after physicist Hans Christian Ørsted, the discoverer of electromagnetism. The Ørsted satellite carries four science instruments with the objectives of mapping the Earth's magnetic field (vector and scalar), and measuring the charged particle environment from approximately 800 km altitude sun-synchronous polar orbit. The project is funded by the Ministries for Research, Education and Industry, and by the industrial consortium.
Comprehensive and accurate mapping of the geomagnetic field is of particular interest to geophysical studies. Preferably, such mapping should be done continuously, or at least every 3-5 years. As such, the Ørsted Satellite fills an important gap between similar measurements made by the NASA Magsat mission (1979-80), and planned for the NASA/CNES Games mission (1998+). The geomagnetic field is continuously changing in a way which today is only poorly understood, and which is thought to relate to physical processes in the Earth's inner fluid core.
The Ørsted Control Centre and EGSE were developed according to the recommendations of the ESA Committee for Operations and EGSE Standards (COSE). Maximum system reuse is gained as the Control Centre is designed to be the controlling component of the EGSE facility. Through the planned use of the new ESA standards for packet telemetry and packet telecommands any SCOE component will be handled in exactly the same way as any on-board subsystem.
The ABB/SYPRO (and later also CRI) application consisted of the specification and development of a software system for controlling an X-ray telescope onboard a joint Russian and Danish scientific satellite (the "XSPECT" project). The system was developed together with the Danish Space Research Institute.
The main purpose of the system was to receive, process, store and transmit data received from the detector part of an X-ray telescope. The detector and its associated control system was one experiment on board a scientific satellite.
In addition to the main function of the system it was able to perform supervision and control of various parts of the X-ray telescope and to shut down the X-ray detector in case of hazardous environmental conditions such as excessive radiation or high temperatures.
The system was implemented in concurrent C on a transputer-based system, and the fact that the RSL concurrency model is based on synchronous message passing on named channels, similar to that used on transputers, was a great help in the communication with the team at the Danish Space Research Institute.
ICL incident reporting system
The ICL application specified and developed an on-line incident reporting system. An incident report is a form used for recording faults, change requests etc against an item under change control, such as a piece of software. An incident report contains a number of standard fields, and as the incident is followed up and actions are taken, the report is updated to form a complete and up-to-date record of progress. The incident reports are kept in a database that also supports the extraction of statistics.
The work was carried out using an earlier version of RSL that is somewhat different from the current one and it tested prototype versions of the RAISE toolset. The application was a concurrent system and the specification and development utilized the concurrency features of RSL.