A Synchronous Language for Modeling and Verifying Real Time and Embedded Systems.
Thomas Kröpf, Jürgen Ruf, Klaus Schneider, Markus Wild · 1998
. This paper presents the new synchronous language PURR, the system description language of the verification system C@S. The language is mainly based on Esterel, but extends it in several ways. These extensions are necessary to model systems at a high level of abstraction that makes stateof -the-art verification techniques applicable. Moreover, our new language directly supports transformational verification: most steps necessary to make a system description suitable for a correctness proof with a certain decision procedure or a theorem prover can be done inside our language, avoiding conflicts occurring from different semantics of different languages. 1 Introduction The formal verification of systems requires languages to formally model the system implementation and to describe specifications unambiguously. Correctness proofs can then be performed using a calculus or a decision procedure which work on both descriptions. The main emphasis of this paper lies on a new approach to descr...