Automatic Translation of Ada-ECATNet Using Rewriting Logic

Authors: N. Boudiaf

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

Keywords: Ada tasking, Analysis, Automatic Translation, ECATNets, Maude, Rewriting Logic.

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

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.