A Logic to Specify and Verify Synchronous Transitions

Abstract

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 important to the verification of a large class of systems, but they are missing in other formalisms based on transition systems and temporal logics. This paper also discusses some of the pragmatics in specifying and verifying systems using SINC, and presents extensions to deal with generic parameters and regular structures. SINC is based on the Hoare logic and the UNITY formalism.

Contributors

Vanderlei Moraes Rodrigues

Flávio Rech Wagner

Conference

Publication date: July 1999

Publication date (Print): July 1999

Pages: 1-16

Affiliations

Instituto de Informática, UFRGS

Porto Alegre, RS, Brazil

Article

DOI: 10.14236/ewic/IWFM1999.14

Copyright statement: © Vanderlei Moraes Rodrigues et al. Published by BCS Learning and Development Ltd. 3rd Irish Workshop on Formal Methods

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: 3rd Irish Workshop on Formal Methods

Conference acronym: IWFM

Conference number: 3

Conference location: Galway, Ireland

Conference date: 1st - 2nd July 1999

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Formal Methods

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/IWFM1999.14

Self URI (journal page): https://ewic.bcs.org/

Categories

Series title: Electronic Workshops in Computing