Double Reduction of Ada-ECATNet Representation 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 [2] 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 [12] and its programming language Maude [13]. Rewriting logic is considered as one of very powerful logics in terms of description, verification and programming of concurrent systems. We proposed in [4] a method for translating Ada-95 tasking programs to ECATNets formalism (Ada-ECATNet). In this paper, we show 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 (CPNs). Such translation doesn-t reduce only the size of program, but reduces also the number of program states. We show also, how this compact Ada-ECATNet may be reduced again by applying reduction rules on it. This double reduction of Ada-ECATNet permits a considerable minimization of the memory space and run time of corresponding Maude program.

Authors:

• Noura Boudiaf
• Allaoua Chaoui

Keywords:

• Ada tasking
• ECATNets
• Algebraic Petri Nets
• Compact Representation
• Analysis
• Rewriting Logic
• Maude.

References:

[1] K. Barkaoui and J-F Pradat-Peyre. "Verification in Concurrent
Programming with Petri nets Structural Techniques". In Proceedings
Third IEEE International High-Assurance Systems Engineering
Symposium November 13 - 14, 1998 Washi, 1998.
[2] M. Bettaz, M. Maouche. "How to specify Non Determinism and True
Concurrency with Algebraic Term Nets". Volume 655 of LNCS, Spring-
Verlag, p. 11-30, 1993.
[3] 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.
[4] N. Boudiaf, A. Chaoui, "Towards Automated Analysis of Ada-95
Tasking Behavior By Using ECATNets". ISIIT-04, Jordan, 2004.
[5] N. Boudiaf, K. Barkaoui, Allaoua Chaoui. "Implémentation Des Règles
de Réduction des ECATNets dans Maude". Proceedings de la
Conférence Mosim-06, 2-5 avril, Rabat, Maroc, pp. 1505-514, 2006.
[6] N. Boudiaf, K. Barkaoui and Allaoua Chaoui. "Applying Reduction
Rules to ECATNets". Proceedings of AVIS'06 Workshop (Co-located
with the conferences ETAPS'06), 1st April, Vienna, Austria, To appear
in ENTCS, 2006.
[7] E. Bruneton and J-F. Pradat-Peyre. "Automatic Verification of
Concurrent Ada Programs", In Proceedings Reliable Software
Technologies-Ada-Europe'99, 1999.
[8] M. Clavel and al., "The Maude 2.0 System". In Proc. Rewriting
Techniques and Applications, V. 2706 of LNCS, Spring-Verlag, 2003.
[9] S. Evangelista, C. Kaiser, J. F. Pradat-Peyre, and P. Rousseau. "Quasar:
a new tool for analyzing concurrent programs". In 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". Comput. Lang. 25(2): 55-87,
1999.
[11] ISO/IEC 8652. "Information Technology - Programming Languages -
Ada", 1995.
[12] J. Meseguer "Rewriting Logic as a Semantic Framework of
Concurrency: a Progress Report". Seventh International Conference on
Concurrency Theory (CONCUR'96), Volume 1119 of LNCS, Springer
Verlag, p. 331-372, 1996.
[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, 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, ISBN 951-22-3495-5,
1997.