Formal modeling of synchronization methods for concurrent objects in Ada 95

ABSTRACT

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 distributed- object 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.

REFERENCES

• 1: Alan Burns , Andy Wellings, Concurrency in Ada, Cambridge University Press, New York, NY, 1995
• 2: John Barnes, Programming in Ada95, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1995
• 3: T. Murata, "Petri Nets: Properties, Analysis and Applications," Proceedings of the IEEE, 77(4):541-580, April 1989.
• 4: D. Mandrioli , R. Zicari , C. Ghezzi , F. Tisato, Modeling the ADA task system by Petri nets, Computer Languages, v.10 n.1, p.43-61, 1985 [doi>10.1016/0096-0551(85)90010-4]
• 5: Sol M. Shatz , Shengru Tu , Tadao Murata , Sastry Duri, An Application of Petri Net Reduction for Ada Tasking Deadlock Analysis, IEEE Transactions on Parallel and Distributed Systems, v.7 n.12, p.1307-1322, December 1996 [doi>10.1109/71.553301]
• 6: S. Duri , U. Buy , R. Devarapalli , S. M. Shatz, Application and experimental evaluation of state space reduction methods for deadlock analysis in Ada, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.4, p.340-380, Oct. 1994 [doi>10.1145/201024.201038]
• 7: Ravi K. Gedela , Sol M. Shatz, Modeling of Advanced Tasking in Ada-95: A Petri Net Perspective, Proceedings of the 2nd International Workshop on Software Engineering for Parallel and Distributed Systems, p.4, May 17-18, 1997
• 8: Kurt Jensen, Coloured Petri Nets: a high level language for system design and analysis, Proceedings on Advances in Petri nets 1990, p.342-416, March 1991
• 9: S. M. Shatz , K. Mai , C. Black , S. Tu, Design and Implementation of a Petri Net Based Toolkit for Ada Tasking Analysis, IEEE Transactions on Parallel and Distributed Systems, v.1 n.4, p.424-441, October 1990 [doi>10.1109/71.80172]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
  D.4 OPERATING SYSTEMS

General Terms:
Languages, Management, Theory

Keywords:
Ada-95, Petri net formalism, concurrent objects, distributed software, synchronization methods