×

Compositional specification in rewriting logic. (English) Zbl 1434.68301

Summary: Rewriting logic is naturally concurrent: several subterms of the state term can be rewritten simultaneously. But state terms are global, which makes compositionality difficult to achieve. Compositionality here means being able to decompose a complex system into its functional components and code each as an isolated and encapsulated system. Our goal is to help bringing compositionality to system specification in rewriting logic. The base of our proposal is the operation that we call synchronous composition. We discuss the motivations and implications of our proposal, formalize it for rewriting logic and also for transition structures, to be used as semantics, and show the power of our approach with some examples.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68Q42 Grammars and rewriting systems

Software:

Reo; SCEL; Maude
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Arbab, F.2004. REO: A channel-based coordination model for component composition. Mathematical Structures in Computer Science14, 3, 329-366. · Zbl 1085.68552
[2] Bachmair, L., Tiwari, A. and Vigneron, L.2003. Abstract congruence closure. Journal of Automated Reasoning31, 2, 129-168. · Zbl 1040.03006
[3] Bae, K. and Meseguer, J.2010. The linear temporal logic of rewriting Maude model checker. In Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers, Ölveczky, P. C., Ed. Lecture Notes in Computer Science, vol. 6381. Springer, 208-225. · Zbl 1306.68099
[4] Bae, K. and Meseguer, J.2012. A rewriting-based model checker for the linear temporal logic of rewriting. Electronic Notes in Theoretical Computer Science290, 19-36. · Zbl 1291.68244
[5] Bae, K. and Meseguer, J.2015. Model checking linear temporal logic of rewriting formulas under localized fairness. Science of Computer Programming99, 193-234.
[6] Basu, A., Bozga, M. and Sifakis, J.2008. Modeling heterogeneous real-time components in BIP. In Perspectives Workshop: Model Engineering of Complex Systems (MECS), August 10-13, 2008, Aßmann, U., Bézivin, J., Paige, R. F., Rumpe, B. and Schmidt, D. C., Eds. Dagstuhl Seminar Proceedings, vol. 08331. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany.
[7] Boudol, G. and Castellani, I.1988. A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae11, 433-452. · Zbl 0657.68066
[8] Bruni, R., Melgratti, H. C., Montanari, U. and Sobociński, P.2013. Connector algebras for C/E and P/T nets’ interactions. Logical Methods in Computer Science9, 3. · Zbl 1274.68224
[9] Bruni, R., Meseguer, J. and Montanari, U.2002. Tiling transactions in rewriting logic. Electronic Notes on Theoretical Computer Science71, 90-109. · Zbl 1272.68291
[10] Bruns, G. and Godefroid, P.1999. Model checking partial state spaces with 3-valued temporal logics. In Computer Aided Verification: 11th International Conference, CAV ’99, Halbwachs, N. and Peled, D., Eds. Lecture Notes in Computer Science, vol. 1633. Springer-Verlag, Trento, Italy, 274-287. · Zbl 1046.68583
[11] Bruns, G. and Godefroid, P.2000. Generalized model checking: Reasoning about partial state spaces. In CONCUR 2000—Concurrency Theory: 11th International Conference, Palamidessi, C., Ed. Lecture Notes in Computer Science, vol. 1877. Springer, University Park, PA, USA, 168-182. · Zbl 0999.68524
[12] Butler, M. and Leuschel, M.2005. Combining CSP and B for specification and property verification. In FM 2005: Formal Methods, Fitzgerald, J., Hayes, I. J. and Tarlecki, A., Eds. Springer, Berlin, Heidelberg, 221-236. · Zbl 1120.68411
[13] Chaki, S., Clarke, E. M., Ouaknine, J., Sharygina, N. and Sinha, N.2004. State/event-based software model checking. In IFM, Boiten, E. A., Derrick, J., Smith, G., Eds. Lecture Notes in Computer Science, vol. 2999. Springer, 128-147. · Zbl 1196.68129
[14] Clarke, E. M. J., Grumberg, O. and Peled, D. A.1999. Model Checking. MIT Press, Cambridge, MA, USA. · Zbl 1423.68002
[15] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J. and Talcott, C. L.2007. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. Lecture Notes in Computer Science, vol. 4350. Springer, Berlin, Heidelberg. · Zbl 1115.68046
[16] Clavel, M. and Meseguer, J.1997. Internal strategies in a reflective logic. In Proceedings of the CADE-14 Workshop on Strategies in Automated Deduction, Gramlich, B. and Kirchner, H., Eds. Springer, Townsville, Australia, 1-12.
[17] de Alfaro, L. and Henzinger, T. A.2005. Interface-based design. In Engineering Theories of Software Intensive Systems, Broy, M., Grünbauer, J., Harel, D. and Hoare, T., Eds. Springer Netherlands, Dordrecht, 83-104.
[18] De Nicola, R., Fantechi, A., Gnesi, S. and Ristori, G.1993. An action-based framework for verifying logical and behavioural properties of concurrent systems. Computer Networks and ISDN Systems 25, 7, 761-778. · Zbl 0789.68096
[19] De Nicola, R., Latella, D., Lafuente, A. L., Loreti, M., Margheri, A., Massink, M., Morichetta, A., Pugliese, R., Tiezzi, F. and Vandin, A.2015. The SCEL language: Design, implementation, verification. In Software Engineering for Collective Autonomic Systems: The ASCENS Approach, Wirsing, M., Hölzl, M., Koch, N. and Mayer, P., Eds. Springer International Publishing, Cham, 3-71.
[20] De Nicola, R. and Vaandrager, F. W.1990. Action versus state based logics for transition systems. In Semantics of Systems of Concurrent Processes, Guessarian, I., Eds. Lecture Notes in Computer Science, vol. 469. Springer, 407-419.
[21] De Nicola, R. and Vaandrager, F.1995. Three logics for branching bisimulation. Journal of the Association for Computing Machinery 42, 2, 458-487. · Zbl 0886.68064
[22] Eker, S., Martí-Oliet, N., Meseguer, J. and Verdejo, A.2007. Deduction, strategies, and rewriting. In Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES 2006), Archer, M., de la Tour, T. B. and Muñoz, C., Eds. Electronic Notes in Theoretical Computer Science, vol. 174. Elsevier, Seattle, WA, USA, 3-25. · Zbl 1277.68241
[23] Gadducci, F. and Montanari, U.2000. The tile model. In Proof, Language, and Interaction, Essays in Honour of Robin Milner, Plotkin, G. D., Stirling, C. and Tofte, M., Eds. The MIT Press, 133-166. · Zbl 0968.68018
[24] Garavel, H., Lang, F. and Serwe, W.2017. From LOTOS to LNT. In ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, Katoen, J.-P. and Langerak, R., Eds. Lecture Notes in Computer Science, vol. 10500. Springer, 3-26. DOI: doi:10.1007/978-3-319-68270-9_1. · Zbl 1498.68062
[25] Gianola, A., Kasangian, S. and Sabadini, N.2017. Cospan/span(graph): An algebra for open, reconfigurable automata networks. In 7th Conference on Algebra and Coalgebra in Computer Science, CALCO 2017, June 12-16, 2017, Ljubljana, Slovenia, Bonchi, F. and König, B., Eds. LIPIcs, vol. 72. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2:1-2:17. · Zbl 1433.68223
[26] Godefroid, P. and Huth, M.2005. Model checking vs. generalized model checking: Semantic minimizations for temporal logics. In Proceedings of 20th Annual IEEE Symposium on Logic in Computer Science (LICS ’05). IEEE, Chicago, IL, USA, 158-167.
[27] Harel, D., Marron, A. and Weiss, G.2012. Behavioural Programming. Communications of the Association for Computing Machinery55, 7, 90-100.
[28] Hennicker, R., Knapp, A. and Wirsing, M.2014. Assembly theories for communication-safe component systems. In From Programs to Systems. The Systems perspective in Computing - ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings, Bensalem, S., Lakhnech, Y. and Legay, A., Eds. Lecture Notes in Computer Science, vol. 8415. Springer, 145-160. · Zbl 1310.68057
[29] Hoare, C. A. R.1978. Communicating sequential processes. Communications of the Association for Computing Machinery 21, 8, 666-677. · Zbl 0383.68028
[30] Hopcroft, J. E., Motwani, R. and Ullman, J. D.2006. Introduction to Automata Theory, Languages, and Computation (3rd ed.). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA. · Zbl 0980.68066
[31] Huth, M., Jagadeesan, R. and Schmidt, D.2001. Modal transition systems: A foundation for three-valued program analysis. In Programming Languages and Systems: 10th European Symposium on Programming, ESOP 2001, Sands, D., Ed. Lecture Notes in Computer Science, vol. 2028. Springer, Genova, Italy, 155-169. · Zbl 0987.68849
[32] Jensen, K. and Kristensen, L. M.2009. Coloured Petri Nets. Springer, Berlin, Heidelberg. · Zbl 1215.68153
[33] Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C. V., Loingtier, J.-M., Irwin, J. and Lopes, C.1997. Aspect-oriented programming. In ECOOP ’97—Object-Oriented Programming. Lecture Notes in Computer Science, vol. 1241. Springer-Verlag, Jyväskylä, Finland, 220-242.
[34] Kindler, E. and Vesper, T.1998. ESTL: A temporal logic for events and states. In Application and Theory of Petri Nets 1998: 19th International Conference, ICATPN ’98, Desel, J. and Silva, M., Eds. Lecture Notes in Computer Science, vol. 1420. Springer, Lisbon, Portugal, 365-384. · Zbl 1510.68042
[35] Lescanne, P.1989. Completion Procedures as Transition Rules + Control. In TAPSOFT ’89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Díaz, J. and Orejas, F., Eds. Lecture Notes in Computer Science, vol. 351. Springer, Berlin, Heidelberg, 28-41.
[36] Lynch, N. A. and Tuttle, M. R.1989. An introduction to input/output automata. CWI Quarterly 2, 219-246. · Zbl 0677.68067
[37] Magee, J. and Kramer, J.2006. Concurrency - State Models and Java Programs (2nd ed.). Wiley. · Zbl 0924.68026
[38] Martí-Oliet, N., Meseguer, J. and Verdejo, A.2004. Towards a strategy language for Maude. In Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications (WRLA 2004), Martí-Oliet, N., Ed. Electronic Notes in Theoretical Computer Science, vol. 117. Elsevier, Barcelona, Spain, 417-441.
[39] Martí-Oliet, N., Meseguer, J. and Verdejo, A.2009. A rewriting semantics for Maude strategies. In Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications (WRLA 2008), Rosu, G., Ed. Electronic Notes in Theoretical Computer Science, vol. 238. Elsevier, Budapest, Hungary, 227-247. · Zbl 1347.68199
[40] Martn, Ó., Verdejo, A. and Martí-Oliet, N.2014. Model checking TLR* guarantee formulas on infinite systems. In Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi, Iida, S., Meseguer, J. and Ogata, K., Eds. Lecture Notes in Computer Science, vol. 8373. Springer, 129-150. · Zbl 1407.68296
[41] Martín, Ó., Verdejo, A. and Martí-Oliet, N.2016a. Egalitarian state-transition systems. In Rewriting Logic and Its Applications: WRLA 2016, Lucanu, D., Ed. Lecture Notes in Computer Science, vol. 9942. Springer, Eindhoven, The Netherlands, 98-117. · Zbl 1367.68198
[42] Martín, Ó., Verdejo, A. and Martí-Oliet, N.2016b. Synchronous products of rewrite systems. In Automated Technology for Verification and Analysis: ATVA 2016, Artho, C., Legay, A. and Peled, D. A., Eds. Lecture Notes in Computer Science, vol. 9938. Springer, Cham, 141-156. · Zbl 1398.68279
[43] Martn, Ó., Verdejo, A. and Mart-Oliet, N.2018. Parameterized programming for compositional system specification. In Rewriting Logic and Its Applications: WRLA 2018, Rusu, V., Ed. Lecture Notes in Computer Science, vol. 11152. Springer. · Zbl 1517.68246
[44] Mazurkiewicz, A.1988. Compositional semantics of pure place/transition systems. In Advances in Petri nets: APN 1987, Rozenberg, G., Ed. Lecture Notes in Computer Science, vol. 340. Springer, Oxford, UK, 307-330. · Zbl 0676.68030
[45] Meseguer, J.1992. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science96, 1, 73-155. · Zbl 0758.68043
[46] Meseguer, J.2008. The temporal logic of rewriting: A gentle introduction. In Concurrency, Graphs and Models, Degano, P., Nicola, R. D. and Meseguer, J., Eds. Lecture Notes in Computer Science, vol. 5065. Springer, Berlin, Heidelberg, 354-382. · Zbl 1143.68459
[47] Meseguer, J. and Montanari, U.1997. Mapping tile logic into rewriting logic. In Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT ’97, Tarquinia, Italy, June 1997, Selected Papers. Lecture Notes in Computer Science, vol. 1376. Springer, 62-91. · Zbl 0903.08010
[48] Meseguer, J. and Thati, P.2007. Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation 20, 123-160. · Zbl 1115.68079
[49] Milner, R.1980. A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol. 92. Springer-Verlag, Berlin, Heidelberg. · Zbl 0452.68027
[50] Papadopoulos, G. A. and Arbab, F.1998. Coordination models and languages. Advances in Computers 46, 329-400.
[51] Pnueli, A.1985. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, Apt, K. R., Ed. Springer, Berlin, Heidelberg, 123-144. · Zbl 0578.68014
[52] Reisig, W.1985. Petri Nets: An Introduction. EATCS Monographs in Theoretical Computer Science. Springer, Berlin, Heidelberg. · Zbl 0555.68033
[53] Reisig, W.2013. Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. Springer, Berlin, Heidelberg. · Zbl 1278.68222
[54] Sánchez, C. and Samborski-Forlese, J.2012. Efficient regular linear temporal logic using dualization and stratification. In Proceedings - 2012 19th International Symposium on Temporal Representation and Reasoning, TIME 2012, 13-20. · Zbl 1362.03020
[55] Sobociński, P.2016. Compositional model checking of concurrent systems, with Petri nets. In Developments in Computational Models: DCM 2015 Proceedings, Muñoz, C. A. and Pérez, J. A., Eds. Electronics Proceedings in Theoretical Computer Science, vol. 204. Open Publishing Association, Cali, Colombia, 19-30. · Zbl 1477.68184
[56] Verdejo, A. and Martí-Oliet, N.2012. Basic completion strategies as another application of the Maude strategy language. In Workshop on Reduction Strategies in Rewriting and Programming (WRS2011), Escobar, S., Ed. Electronic Proceedings in Theoretical Computer Science, vol. 82. Open Publishing Association, Novi Sad, Serbia, 17-36.
[57] Welch, P. H. and Barnes, F. R. M.2004. Communicating mobile processes. In Communicating Sequential Processes: The First 25 Years, Symposium on the Occasion of 25 Years of CSP, London, UK, July 7-8, 2004, Revised Invited Papers, Abdallah, A. E., Jones, C. B. and Sanders, J. W., Eds. Lecture Notes in Computer Science, vol. 3525. Springer, 175-210. · Zbl 1081.68657
[58] Wells, G.2005. New issues on coordination and adaptation techniques. In Proceedings of the Second International Workshop on Coordination and Adaptation Techniques for Software Entities WCAT’05, 25 Jul. 2005, Becker, S., Canal, C., Murillo, J. M., Poizat, P. and Tivoli, M., Eds. Glasgow, Scotland, 87-89. Held in conjunction with ECOOP 2005, Technical Report TR ITI-05-07, Dpto. de Lenguajes y Ciencias de la Computación, Universidad de Málaga. URL: https://www.cs.cmu.edu/jcmoreno/files/WCAT05Proceedings.pdf [Accessed on September 26, 2019].
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.