Formal Modeling of Synchronization Methods for Concurrent Objects in Ada 95

One important role for Ada programming is to aid engineering of concurrent and distributed software. In a concurrent and distributed environment, objects may execute concurrently and need to be synchronized to serve a common goal. Three basic methods by which objects in a concurrent environment can be constructed and synchronized have been identified [1]. To formalize the semantics of these methods and to provide a formal model of their core behavior, we provide some graphic models based on the Petri net formalism. The purpose of this formal modeling is to illustrate the possibility of automatic program analysis for object-oriented features in Ada-95. Models for the three distributedobject synchronization methods are discussed, and a potential deadlock situation for one of the methods/models is illustrated. We conclude with some comparison of the three methods in terms of the model abstractions. 1.1 Keywords Ada-95, concurrent objects, distributed software, synchronization methods, Petri net formalism Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee