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
(ps.zip)
Abstract
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