Introduction to formal methods and experiences from the LaCoS and Orsted projects

The LaCoS project was an ESPRIT project that was carried out between 1990 and 1994. Its aims were to conduct extensive industrial trials using the formal method RAISE (Rigorous Approach to Industrial Software Engineering) within a number of industrial sectors, and to further evolve and industrialise the RAISE products, i.e. the RAISE Specification Language (RSL), the RAISE method and the RAISE tools. The Orsted satellite is a Danish microsatellite whose mission is to measure the magnetic fields and fluxes of charged particles near the Earth. The satellite carries five scientific instruments including an Overhauser magnetometer, a fluxgate magnetometer and a star imager, all these three instruments being placed on a deployable 8 metre boom. The development is now complete and the satellite is to be launched in the autumn of 1997. The onboard software that was developed by CRI constitutes two command and data handling subsystems and consists of approximately 60,000 lines of Ada code. The command and data handling subsystems are responsible for up and down link telecommunication, acquisition and preprocessing of scientific data, failure detection and recovery based on housekeeping collection, and autonomous control of data acquisition. The software is hence critical to the mission. It was decided to divide the considerations of functional and performance correctness, and to use RAISE as the primary method for achieving the former