Incremental Specification and Verification of Synchronous Reactive Systems
Josť R. de Diego, Javier Tuya, Claudio de la Riva
In: Fourth Workshop on Models, Environments and tools for Requirements Engineering (Menhir), Burgos, 1999


While verifying a system, inputs from the environment take an important role, the system may know through them how the controlled devices are working. To achieve a correct verification a model of the environment must be used, which if modeled in a lifelike way it may introduce several failure situations during verification. This can eventually make any safety property false if verification is done at the earlier steps of specification. On the other side, the use of a model checker in order to verify a reactive system often forces changes in the model, since it contains non discrete elements which can not be included while verifying the system. This paper presents a gradual approach to specify and verify a reactive system, establishing the different steps to be followed to model the environment, allowing initially to verify the correct functionality of the model within an environment without failures, and gradually incorporate fault situations to make it consistent. A software process model is provided to formalize all the steps.

Index - Testing - Personal Page