Assertional Reasoning about Dynamic Systems
H. Conrad Cunningham, Gruia-Catalin Roman, Jerome Y. Plun · 1993
The desire to model in a straightforward manner complex features of real physical systems is often tempered by difficulties associated with reasoning about the resulting computational models. UNITY, Swarm and Dynamic Synchrony are three models of concurrency that accommodate successively more dynamic systems: from systems that can be characterized in terms of a fixed set of actions to systems involving arbitrary runtime changes in the synchronization pattern among dynamically created actions. This paper shows how, despite fundamental differences in computing styles, the three models were designed to share the same basic assertional proof logic. A sample problem, synchronous array summation, is used to illustrate the features of the three models and their impact on program verification.