Specification of Environment Properties for Simulation of Reactive Systems

A reactive system is a system that makes immediate and continuous reactions to the stimuli from its environment. Manual generation of test input values for a reactive system is labor-intensive and error-prone. Relations between output and input signals can be used to automatically generate values of corresponding input signals. In this paper, we propose a method to specify relations between a system in an imperative synchronous language Esterel and its environment. We can translate the specification into the code that simulates the environment and generates proper input signals. When the target system is simulated with the generated code, the number of input signals that require manual intervention is reduced, so that the simulation and verification processes are simplified. We have shown that the proposed method is useful to reduce the effort for simulation and verification with an elevator system.