Modular Verification of Synchronous Programs

In this paper, we develop an approach to the modular verification of synchronous programs. To this end, we have to solve two major problems: First, if a synchronous module is verified without its later context, outputs may not be completely determined (since the calling module may add further actions on the outputs of the called module). It is not difficult to see that the open system obtained by modular compilation simulates the closed one obtained by the linker, and therefore, we can preserve all universal temporal properties. Second, a module call may replace the formal input parameters by expressions which corresponds with a substitution of variables in the symbolic transition relation. In particular, this affects the starting point and potential preemption conditions of the module and can therefore dramatically affect the behavior of the module. For this reason, we have to modify the temporal specifications accordingly. We prove a preservation result for this transformation that defines a simulation preorder modulo substitution. Our results finally determine a proof rule for the verification of module calls in imperative synchronous programs.