Automatic Translation of Ada-ECATNet Using Rewriting Logic

One major difficulty that faces developers of concurrent and distributed software is analysis for concurrency based faults like deadlocks. Petri nets are used extensively in the verification of correctness of concurrent programs. ECATNets are a category of algebraic Petri nets based on a sound combination of algebraic abstract types and high-level Petri nets. ECATNets have 'sound' and 'complete' semantics because of their integration in rewriting logic and its programming language Maude. Rewriting logic is considered as one of very powerful logics in terms of description, verification and programming of concurrent systems We proposed previously a method for translating Ada-95 tasking programs to ECATNets formalism (Ada-ECATNet) and we showed that ECATNets formalism provides a more compact translation for Ada programs compared to the other approaches based on simple Petri nets or Colored Petri nets. We showed also previously how the ECATNet formalism offers to Ada many validation and verification tools like simulation, Model Checking, accessibility analysis and static analysis. In this paper, we describe the implementation of our translation of the Ada programs into ECATNets.

Authors:

• N. Boudiaf

Keywords:

• Ada tasking
• Analysis
• Automatic Translation
• ECATNets
• Maude
• Rewriting Logic.

References:

[1] M. Bettaz, M. Maouche, "How to specify Non Determinism and True
Concurrency with Algebraic Term Nets", Vol. 655 of LNCS, Spring-
Verlag, p. 11-30, 1993.
[2] M. Bettaz, A. Chaoui, K. Barkkaoui, "On Finding Structural Deadlocks
in ECATNets Using a Logic of Concurrency", Journal on Computing
and Information, Vol 2 No 1, pp. 495-506, 1996.
[3] N. Boudiaf, A. Chaoui, "Towards Automated Analysis of Ada-95
Tasking Behavior By Using ECATNets", in Proc. Conference ISIIT-04,
Jordan, 2004.
[4] N. Boudiaf, K. Barkaoui, A. Chaoui, "Implémentation Des Règles de
Réduction des ECATNets dans Maude", in Proc. Conference Mosim-06,
Rabat, Maroc, 2006, pp. 1505-514.
[5] N. Boudiaf, K. Barkaoui and A. Chaoui, "Applying Reduction Rules to
ECATNets", in Proc. AVIS'06 Workshop (Co-located with the
conferences ETAPS'06), Vienna, Austria, 2006.
[6] N. Boudiaf, A. Chaoui, "Double Reduction of Ada-ECATNet
Representation Using Rewriting Logic", Enformatika Journal
(Transactions on Engineering, Computing and Technology), Vol. 15,
ISSN 1305-5313, pp. 278-284, October 2006.
[7] E. Bruneton and J-F. Pradat-Peyre, "Automatic Verification of
Concurrent Ada Programs", in Proc. Reliable Software Technologies-
Ada-Europe, 1999.
[8] M. Clavel and aL, "Maude Manual (Version 2.2)", Internal report, SRI
International, December 2005.
[9] S. Evangelista, C. Kaiser, J. F. Pradat-Peyre, and P. Rousseau, "Quasar:
a new tool for analyzing concurrent programs". in Proc. Ada-Europe
2003, LNCS, Springer-Verlag, 2003.
[10] Ravi K. Gedela, Sol M. Shatz and Haiping Xu, "Compositional Petri Net
Models of Advanced Tasking in Ada-95", in Proc. Comput. Lang. 25(2),
1999, pp. 55-87.
[11] ISO/IEC 8652. "Information Technology - Programming Languages -
Ada", 1995.
[12] J. Meseguer, "Rewriting Logic as a Semantic Framework of
Concurrency: a Progress Report", in Proc. Seventh International
Conference on Concurrency Theory, Vol. 1119 of LNCS, Springer
Verlag, 1996, pp. 331-372.
[13] J. Meseguer, "Rewriting logic and Maude: a Wide-Spectrum Semantic
Framework for Object-based Distributed Systems", In S. Smith and C.L.
Talcott, editors, in Proc. Formal Methods for Open Object-based
Distributed Systems. Kluwer, 2000.
[14] T. Murata, B. Shenker, S. M. Shatz, "Detection of Ada Static Deadlocks
Using Petri Nets Invariants", IEEE trans. Oo Software Engineering, vol.
15, No. 3, pp 314-326, 1989.
[15] S. M. Shatz, S. Tu, T. Murata, S. Duri,. "An Application of Petri Net
Reduction for Ada Tasking Deadlock Analysis", IEEE Transactions on
Parallel and Distributed Systems, 1996.
[16] K. Schmidt, "Applying Reduction Rules to Algebraic Petri Nets", TKK
Monoistamo; Otaniemi 1997, ISSN 0783 5396, 1997.