A logic for synchronous transitions with dynamic conflict resolution

This paper introduces a formalism named DSYNC aimed at. the design and verification of synchronous concurrent systems. The components of this formalism are a transition system and first-order linear-time temporal logic. The DSYNC transition system adopts a synchronous computation model, includes a method to solve write-conflicts, and represents transitions as possibly non-terminating imperative commands. The conflict resolution method is dynamic because it detects conflicts at run-time. The DSYNC logic allows for formal reasoning about DSYNC 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 for the verification of a large class of systems. This paper also discusses some of the pragmatics in verifying systems with DSYNC; and considers some extensions to the formalism. DSYNC is based on hte Hoare logic and the UNITY formalism.