The benefits of formal description techniques for space on-board systems and their integration in an on-board architecture

This paper is split in two parts. In the first one, it relates the present experience of the space industry in the use of Formal Description Techniques. In particular, the initiative intending to spread the awareness and the use of FDT in space industry will be reported. It was implemented in 1996 by two workshops on Executable Specification. The first one allowed to understand a trend in industry amongst the various languages and methods available. The second allowed to confirm the industry interest for SDL to model spacecraft data systems. The second workshop reported also industrial experience coming from a study using SDL in FDIR (DDV) and another one using LOTOS for conformance tests (LVARTS). This part of the paper also mentions the danish experience with Raise for the satellite Oersted, an Aerospatiale survey on Vdm++ and the dissemination action initiated by Formal Method Europe (a European Community group). The second part of the paper will focus more on the selected SDL method and will propose a way to integrate its engineering into the present architecture of the seacecraft on-board software, mainly based on HRT-HOOD. As the trend is to merge several subsystem software into one single computer, it is likely that their integration will not be easy. Moreover, to improve the productivity of such a large sized software, it is necessary to improve the continuity of the life cycle by new techniques such as automatic code generation. The problem is then to combine two ways of producing software. The first classical way is based on an HRT-HOOD architecture and the manual coding of the final modules (although supported by an automatic generation of the skeletons). The second innovative way is the automatic code generation from a FDT environment such as SDL or MatrixX. SDL is the candidate for this exercise, and a mapping from SDL to HRT-HOOD is proposed.