Document Type

Technical Report

Department

Computer Science and Engineering

Publication Date

1993-01-01

Filename

WUCS-93-4.PDF

Technical Report Number

WUCS-93-4

Abstract

This paper presents a model of concurrency (Dynamic Synchrony) whose distinctive feature is a novel formal treatment of synchronization. Synchrony is defined as the coordinated execution of two or more actions. The dynamic aspect comes from the fact that the definition of which actions must be executed synchronously can change freely during the execution of the program. This unique modeling capability comes with a UNITY-stype assertional logic that can be applied to program verification and derivation. This paper shows that the proposed proof logic can be used to verify programs expressed using other models of foncurrency without having to translate them to our notation. This capability is illustrated by verifying three versions of a parallel array summation problem, each written using a different model and notation - Swarm, Concurrent Processes, and Input/Output Automata. The new model makes UNITY-stype proofs feasible for a broad range of models of concurrency regardless of the way they handle synchronization and even if they lack an associated proof logic.

Comments

Permanent URL: http://dx.doi.org/10.7936/K74Q7S71

Download

Share

COinS