An algebraic method for the extraction of concurrent processing grains from object-based specifications
Jerrold F. Stach · 1996
The ability to expose concurrency in a problem specification is a valuable aid in determining whether a parallel program design is possible and economic, and in selecting an appropriate language and target architecture to support the implementation requirements. Exposing the degree of concurrency inherent in a computational specification provides an enhanced knowledge base from which to proceed into a Software Engineering lifecycle. This research presents an axiomatic, algebraic method, to expose the natural concurrency in an object based problem specification, and to produce the concurrent processing grains associated with the interaction of its sequents. The method employs a disjunctive normal form of specification that allows the specifier to choose freely from objects, processes, procedures and functions, in creating a sequential model of a computational problem. Such a model is expected to be relatively free of methodological artifact. A second order Bridging Algebra (BA) algebra is employed to interpret inconsistent indications of concurrency from first order Process ($\overline{PA}$) and Data (TA) algebras. The Bridging Algebra reorders the specification according to well defined rules. The process and data algebras are developed to accommodate the signature and ontological considerations of formal objects, as well as the nature of their interactions with other forms of sequents. Formal proof of the axiom system is provided. The $\overline{PA}$ and TA are proven to be bisimilar and algebraic by proof of conservative extension to the kernel axiom set of the Algebra of Communicating Processes. Examples of the reductive capability of the method over actual specifications are provided.