Safety aspects of generic real-time embedded software model checking in the fuzing domain

Software reliability of embedded software of safety critical hard real-time one-shot devices is an important issue for safety critical systems with high risk potential, e.g. in the military fuzing domain. In particular the avoidance of systematic software errors of the code is of interest. This paper shows how the formal software assessment method of model checking can be applied usefully in this domain. A small generic real-time embedded software code is presented that generates output depending on its function mode, chronological sensor data input and time. First the domain specific C-code is expressed as PROcess MEta LAnguage (PROMELA) model. Second typical safety-critical requirements for the generic code are formulated in terms of temporal logic. In a third step it is checked whether the PROMELA model fulfills the temporal logic requirements. Along with the generic code we present the stepwise approach that contains the generation of safety properties. The tool chain and preliminary results of the model checking process are presented, as well.