  Synchronous model is a type of formal models for modelling and specifying
reactive systems. It has a great advantage over other real-time models that its
modelling paradigm supports a deterministic concurrent behaviour of systems.
Various approaches have been utilized for verification of synchronous models
based on different techniques, such as model checking, SAT/SMT sovling, term
rewriting, type inference and so on. In this paper, we propose a verification
approach for synchronous models based on compositional reasoning and term
rewriting. Specifically, we initially propose a variation of dynamic logic,
called synchronous dynamic logic (SDL). SDL extends the regular program model
of first-order dynamic logic (FODL) with necessary primitives to capture the
notion of synchrony and synchronous communication between parallel programs,
and enriches FODL formulas with temporal dynamic logical formulas to specify
safety properties -- a type of properties mainly concerned in reactive systems.
To rightly capture the synchronous communications, we define a constructive
semantics for the program model of SDL. We build a sound and relatively
complete proof system for SDL. Compared to previous verification approaches,
SDL provides a divide and conquer way to analyze and verify synchronous models
based on compositional reasoning of the syntactic structure of the programs of
SDL. To illustrate the usefulness of SDL, we apply SDL to specify and verify a
small example in the synchronous model SyncChart, which shows the potential of
SDL to be used in practice.
