Specifying and verifying reactive systems in a multi-language environment1 1Work partially supported by the project TOSCA.

AbstractThe multi-language environment Synchronie supports the design and formal verificationof synchronous reactive systems. It integrates three synchronous languages and also three ways to specify properties: the temporal logic with future operators CTL, the temporal logic with past operators Past TL, and observers, which are particular synchronous programs. It is argued that this multi-language feature provides an answer to two major issues of formal verification: facility of formalizing properties and facility of verifying large systems. The approach is illustrated with the case study of a time-triggered protocol