Double Reduction of Ada-ECATNet Representation using Rewriting Logic

Authors: Noura Boudiaf, Allaoua Chaoui

Abstract:

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.

Keywords: Ada tasking, ECATNets, Algebraic Petri Nets, Compact Representation, Analysis, Rewriting Logic, Maude.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1080971

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.