Vanderlei Moraes Rodrigues e Flávio Rech Wagner
This paper introduces a formalism named SINC aimed at the design and verification
of synchronous concurrent systems. The components of this formalism are a transition system and a first-order linear-time temporal logic.
The SINC transition system adopts a synchronous computation model, includes a method to solve write-conflicts, and represents transitions
as possibly non-terminating imperative commands. The SINC logic allows for formal reasoning about SINC transition systems using compositional and
modular proofs. Such features are missing in other formalisms based on transition systems and temporal logics, although they are important to
verification of a large class of systems. This paper also dscusses some of the pragmatics in verifying systems with SINC, including extensions to deal
with generic parameters and regular structures. SINC is based on the Hoare and the UNITY formalism.