An object-oriented approach to the specification of applications for office automation
Hossein Saiedian · 1990
The thesis of this dissertation is that formal specification is an essential prerequisite to the successful and effective construction of applications for office automation. The problems associated with the design and development of office systems are identified and the specification requirements of these systems are studied. A formal methodology, call A scBSL, is developed as a formalism to address the specification of problem of office systems. The A scBSL methodology supports the object paradigm and is principally based on the formal theory of the actor model with certain extensions. The central concepts in A scBSL are the object and message passing. Every entity, whether abstract or concrete, that is relevant to some office computation is conceptually viewed as an object. Computations among the objects are uniformly represented as patterns of message passing. Acceptance of a message is referred to as an event. Objects are capable of participating in different events, i.e., they may accept multiple kinds of messages, each requesting a different kind of operation. For an object to participate in an event, certain pre-conditions may have to be true. That state of an object after participating in an event is captured via the post-conditions. The syntax and semantics of A scBSL are formally defined. The syntax of A scBSL is given via a variation of BNF formalism, while its semantics are presented by proving that ten basic laws of parallel processing that hold for the actor model also hold for the A scBSL methodology. Properties of a system of A scBSL objects that are related to distributed computation, such as liveness and safety of objects' computations, consistency of states of objects, synchronous, and asynchronous communications, and deadlock occurrence are also investigated. The situations in which deadlock may occur in a system of A scBSL objects are identified; it is shown that deadlock may occur only in those identified situations. Also, it is shown that a system of objects is always in a consistent state by appeals to the indivisibility of operations of an object in response to a message and atomic state change properties of the A scBSL objects. These properties of objects are also used to prove the safety of A scBSL computations. The pragmatics of A scBSL is explored through a number of examples.