PoK

Authors: Gruia-Catalin Roman, Jerome Y. Plun, C. Donald Wilcox

Description:
Synchrony continues to be an important concern in concurrent programming. Existing languages and models have introduced a great variety of constructs for expressing and managing synchronization among sequential processes or atomic actions. This paper puts forth a model in which synchrony is viewed as a relation among atomic actions, a relation which may evolve with time. The model is shown to be convenient for expressing formally the semantics of synchrony as it appears in many of the languages and models proposed to date. Among such models Swarm is singled out for its use of dynamic synchrony. The Swarm notation is briefly reviewed. A new concurrent algorithm for the leader election problem provides a vehicle for illustrating the use of dynamic synchrony in Swarm.

Authors: Gruia-Catalin Roman, C. Donald Wilcox, Jerome Y. Plun

Description:
The design of distributed programs is a difficult task which can greatly benefit from the application of formal methods. Since design solutions are determined not only by functional requirements imposed by the application but also by the structure and behavior of the underlying hardware architecture, a complete formal treatment of the program derivation process becomes a significant challenge. The common approach is to start with a formal specification of the functional requirements and to derive the desired program through systematic refinements which factor in the architectural constraints informally, in an ad-hoc manner. This paper shows how one can employ a single specification method (program-wide assertions) to express both functional requirements and architectural constraints. A distributed simulation problem is used to illustrate a formal strategy for deriving a distributed program from assertions about its functionality and the constraints imposed by the choice of underlying architecture.

Authors: Gruia-Catalin Roman, Kenneth C. Cox

Description:
In this paper program visualization is defined as a mapping from programs to graphical representations. Simple forms of program visualization are frequently encountered in software engineering. For this reason current advances in program visualization are likely to influence future developments concerning software engineering tools and environments. This paper provides a new taxonomy of program visualization research. The proposed taxonomy becomes the vehicle through which we carry out a systematic review of current systems, techniques, trends, and ideas in program visualization.

Authors: Gruia-Catalin Roman, C. Donald Wilcox

Description:
As critical computer systems continue to grow in complexity, the task of showing that they execute correctly becomes more difficult. For this reason, research in software engineering has turned to formal methods, i.e., rigorous approaches to demonstrating the correctness of software systems. Unfortunately, the formal methods currently used in the design of concurrent systems do not provide any mechanisms for specifying and reasoning about the mapping of software to hardware. As a result, architectural constraints, even though they play an important role in the design process, are left out of the formal framework. In this paper, we show how to state architectural constraints in a formal notation, how to prove that programs are allocated correctly to the underlying architecture, and how to factor architectural considerations into a program derivation process which uses a mixture of specification and program refinements. The approach is illustrated by the derivation of two related programs that solve the same problem but are designed to work on distinct architectures.

Authors: Gruia-Catalin Roman, Kenneth C. Cox

Description:
Program visualization may be viewed as a mapping from programs to graphical representations. This simple idea provides a formal framework for a new taxonomy of program visualization systems. The taxonomy is compared briefly against previous attempts to organize the program visualization field. The taxonomic principles and their motivation are explained in detail with reference to a number of existing systems, especially Balsa, Tango, and Pavane.