An approach to safety verification of object-oriented design specification for an elevator control system

Several methods have been proposed for verifying the safety of software. We have also proposed a new method to verify both safety and correctness of object-oriented design specifications (Proc. 6th ISSRE, pp.78-83, 1995). In that method, we assumed that, in the design specification, any event results in the same action regardless of what state the system is originally in. In this paper, we relax the assumption as follows: actions of an event are determined by the event and its previous event, and we try to extend the applicability of our previous method. In the new method, the verifiers first construct a correctness table and a safety table based on a component library and standards for safety. Next, the designers construct a design table from a design specification. Then, by comparing the corresponding items on three tables, the verifiers review a given design specification and detect faults in it. Finally, using an elevator control system as an example, we show that faults concerning safety or correctness can be detected by the new design review method