We propose a new approach to the interactive verification of synchronous systems. Our approach is based on two system representations: Systems to be verified are given as synchronous programs that are considered for the selection of proof rules, while the proof rules are applied on equivalent sets of synchronous guarded actions that are obtained by an automatic translation from the programs. Since the obtained guarded actions contain assumptions and assertions, they are directly used as proof goals in our approach. Due to a backannotation via control flow locations, there is still a direct correspondence between the two system representations. This way, the user can still consider the more readable program code while the implementation of the proof system on top of the guarded actions allows much more flexible decompositions of the verification goals.
展开▼
