Hierarchical correctness verification in multiphase real-time software design

A hierarchical approach to correctness verification of real-time software specifications is presented. The verification is distributed into successive steps that correspond to the design phases. The three languages: Rule Charts, LACTATRE (graphical specification) and Communicating Real Time State Machines are used for specification of real-time software within corresponding abstraction levels. The correctness is defined as a coincidence of a system specified in a phase w.r.t. requirements established ing the previous phase. This correctness concept leads to an application of the relative correctness methods (developed in former works) for the verification. The approach is examined in Preliminary and Detailed Design phases for the verification of several types of properties: structure, functions and time constraints.