Interpreting Reo Circuits as PDL models
Article Sidebar
Published:
Jan 15, 2022
Keywords:
Reo circuits, PDL models, coordination-based language, multimodal logic
Main Article Content
Abstract
Reo is a coordination-based language with the proposal of connecting different systems and interfaces. It aims to develop communication between different systems with a high level of abstraction and without many restrictions. PDL is a multimodal logic tailored to reason about programs. It is proved to be sound, complete, decidable and has a simple Kripke semantics. This work intends to provide an interpretation of Reo circuits as PDL models. These are the first steps towards providing a dynamic logic tailored to reason directly about Reo circuits.
Article Details
Section
Articles
Copyright Notice
The author of the article or book reviews submitted and approved for publication authorizes the editors to reproduce it and publish it in the journal O que nos faz pensar, with the terms “reproduction” and “publication” being understood in accordance with the definitions of the Creative Commons Attribution-NonCommercial 4.0 International license. The article or book reviews may be accessed both via the World Wide Web – Internet (WWW – Internet), and in printed form, its being permitted, free of charge, to consult and reproduce the text for the personal use of whoever consults it. This authorization of publication has no time limit, with the editors of the journal O que nos faz pensar being responsible for maintaining the identification of the author of the article.
References
[1] F. Arbab. Reo: a channel-based coordination model for component composition. Mathematical structures in computer science, 14(3):329–366, 2004.
[2] F. Arbab. Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science, 14(3):329–366, 2004.
[3] F. Arbab. Coordination for component composition. Electronic Notes in Theoretical Computer Science, 160:15 – 40, 2006. Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 2005).
[4] C. Baier, M. Sirjani, F. Arbab, and J. Rutten. Modeling component connectors in reo by constraint automata. Science of computer programming, 61(2):75–113, 2006.
[5] M. Benevides, B. Lopes, and E. H. Haeusler. Towards reasoning about petri nets: A propositional dynamic logic based approach. Theoretical Computer Science, 774(5):22–36, 2018.
[6] M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journal of computer and system sciences, 18(2):194–211, 1979.
[7] D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. Foundations of Computing Series. MIT Press, 2000.
[8] N. Kokash, C. Krause, and E. De Vink. Reo+ mcrl2: A framework for model-checking dataflow in service compositions. Formal Aspects of Computing, 24(2):187–216, 2012.
[9] M. Lange. Model checking propositional dynamic logic with all extras. Journal of Applied Logic, 4(1):39–49, 2006.
[10] B. Lopes, M. Benevides, and E. H. Haeusler. Extending propositional dynamic logic for Petri nets. Electronic Notes in Theoretical Computer Science, 305(11):67–83, 2014.
[11] B. Lopes, M. Benevides, and E. H. Haeusler. Propositional dynamic logic for Petri nets. Logic Journal of the IGPL, 22(5), 2014.
[12] M. Marx. Xpath and modal logics of finite dag‘s. In M. Cialdea Mayer and F. Pirri, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 150–164, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg.
[13] M. Marx. Xpath with conditional axis relations. In E. Bertino, S. Christodoulakis, D. Plexousakis, V. Christophides, M. Koubarakis, K. Böhm, and E. Ferrari, editors, Advances in Database Technology - EDBT 2004, pages 477–494, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.
[14] S. Navidpour and M. Izadi. Linear temporal logic of constraint automata. In Advances in Computer Science and Engineering, pages 972–975. Springer, 2008.
[15] C. Sinz, W. Kuchlin, and T. Lumpp. Towards a verification of the rule-based expert system of the ibm sa for os/390 automation manager. In Quality Software, 2001. Proceedings. Second Asia-Pacific Conference on, pages 367–374. IEEE, 2001.
[16] H. Tuominen. Elementary net systems and dynamic logic. In European Workshop on Applications and Theory in Petri Nets, pages 453–466. Springer, 1988.
[17] H. Tuominen. Elementary net systems and Dynamic Logic. In G. Rozenberg, editor, Advances in Petri Nets 1989, Lecture Notes in Computer Science, pages 453–466. Springer Berlin Heidelberg, 1990.
[18] F. Wolter and M. Zakharyaschev. Dynamic Description Logics. In Proceedings of AiML’98, pages 290–300. CSLI Publications, 2000.
[19] J. Klein, S. Klüppelholz, A. Stam, and C. Baier. Hierarchical modeling and formal verification. an industrial case study using reo and vereofy. In International Workshop on Formal Methods for Industrial Critical Systems, pages 228–243. Springer, 2011
[20] N. Kokash and F. Arbab. Formal design and verification of long-running transactions with extensible coordination tools. IEEE Transactions on Services Computing, 6(2):186–200, 2011.
[21] N. Kokash, C. Krause, and E. De Vink. Reo+ mcrl2: A framework for model-checking dataflow in service compositions. Formal Aspects of Computing, 24(2):187–216, 2012.-21
[22] Y. Li, X. Zhang, Y. Ji, and M. Sun. A formal framework capturing real-time and stochastic behavior in connectors. Science of Computer Programming, 2019. -31
[23] M. R. Mousavi, M. Sirjani, and F. Arbab. Formal semantics and analysis of component connectors in reo. Electronic Notes in Theoretical Computer Science, 154(1):83–99, 2006.- 32
[24] B. Pourvatan, M. Sirjani, H. Hojjat, and F. Arbab. Automated analysis of reo circuits using symbolic execution. Electronic Notes in Theoretical Computer Science, 255:137–158, 2009. -37
[25] S.-S. T. Jongmans and F. Arbab. Overview of thirty semantic formalisms for reo. Scientific Annals of Computer Science, 22(1), 2012.- 24
[26] F. Arbab, C. Baier, F. de Boer, and J. Rutten. Models and temporal logical specifications for timed component connectors. Software & Systems Modeling, 6(1):59–82, 2007. -5
[27] E. Ardeshir-Larijani, A. Farhadi, and F. Arbab. Simulation of hybrid reo connectors. In 2020 CSI/CPSSI International Symposium on Real-Time and Embedded Systems and Technologies (RTEST), pages 1–10. IEEE, 2020.- 8
[28] Y. Li, X. Zhang, Y. Ji, and M. Sun. Capturing stochastic and real-time behavior in reo connectors. In Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings, pages 287–304, 2017.
[29] M. Sun and Y. Li. Formal modeling and verification of complex interactions in e-government applications. In Proceedings of the 8th International Conference on Theory and Practice of Electronic Governance, pages 506–507. ACM, 2014.
[30] X. Zhang, W. Hong, Y. Li, and M. Sun. Reasoning about connectors in coq. In International Workshop on Formal Aspects of Component Software, pages 172–190. Springer, 2016.
[31] X. Zhang, W. Hong, Y. Li, and M. Sun. Reasoning about connectors using coq and z3. Science of Computer Programming, 170:27–44, 2019.
[2] F. Arbab. Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science, 14(3):329–366, 2004.
[3] F. Arbab. Coordination for component composition. Electronic Notes in Theoretical Computer Science, 160:15 – 40, 2006. Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 2005).
[4] C. Baier, M. Sirjani, F. Arbab, and J. Rutten. Modeling component connectors in reo by constraint automata. Science of computer programming, 61(2):75–113, 2006.
[5] M. Benevides, B. Lopes, and E. H. Haeusler. Towards reasoning about petri nets: A propositional dynamic logic based approach. Theoretical Computer Science, 774(5):22–36, 2018.
[6] M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journal of computer and system sciences, 18(2):194–211, 1979.
[7] D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. Foundations of Computing Series. MIT Press, 2000.
[8] N. Kokash, C. Krause, and E. De Vink. Reo+ mcrl2: A framework for model-checking dataflow in service compositions. Formal Aspects of Computing, 24(2):187–216, 2012.
[9] M. Lange. Model checking propositional dynamic logic with all extras. Journal of Applied Logic, 4(1):39–49, 2006.
[10] B. Lopes, M. Benevides, and E. H. Haeusler. Extending propositional dynamic logic for Petri nets. Electronic Notes in Theoretical Computer Science, 305(11):67–83, 2014.
[11] B. Lopes, M. Benevides, and E. H. Haeusler. Propositional dynamic logic for Petri nets. Logic Journal of the IGPL, 22(5), 2014.
[12] M. Marx. Xpath and modal logics of finite dag‘s. In M. Cialdea Mayer and F. Pirri, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 150–164, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg.
[13] M. Marx. Xpath with conditional axis relations. In E. Bertino, S. Christodoulakis, D. Plexousakis, V. Christophides, M. Koubarakis, K. Böhm, and E. Ferrari, editors, Advances in Database Technology - EDBT 2004, pages 477–494, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.
[14] S. Navidpour and M. Izadi. Linear temporal logic of constraint automata. In Advances in Computer Science and Engineering, pages 972–975. Springer, 2008.
[15] C. Sinz, W. Kuchlin, and T. Lumpp. Towards a verification of the rule-based expert system of the ibm sa for os/390 automation manager. In Quality Software, 2001. Proceedings. Second Asia-Pacific Conference on, pages 367–374. IEEE, 2001.
[16] H. Tuominen. Elementary net systems and dynamic logic. In European Workshop on Applications and Theory in Petri Nets, pages 453–466. Springer, 1988.
[17] H. Tuominen. Elementary net systems and Dynamic Logic. In G. Rozenberg, editor, Advances in Petri Nets 1989, Lecture Notes in Computer Science, pages 453–466. Springer Berlin Heidelberg, 1990.
[18] F. Wolter and M. Zakharyaschev. Dynamic Description Logics. In Proceedings of AiML’98, pages 290–300. CSLI Publications, 2000.
[19] J. Klein, S. Klüppelholz, A. Stam, and C. Baier. Hierarchical modeling and formal verification. an industrial case study using reo and vereofy. In International Workshop on Formal Methods for Industrial Critical Systems, pages 228–243. Springer, 2011
[20] N. Kokash and F. Arbab. Formal design and verification of long-running transactions with extensible coordination tools. IEEE Transactions on Services Computing, 6(2):186–200, 2011.
[21] N. Kokash, C. Krause, and E. De Vink. Reo+ mcrl2: A framework for model-checking dataflow in service compositions. Formal Aspects of Computing, 24(2):187–216, 2012.-21
[22] Y. Li, X. Zhang, Y. Ji, and M. Sun. A formal framework capturing real-time and stochastic behavior in connectors. Science of Computer Programming, 2019. -31
[23] M. R. Mousavi, M. Sirjani, and F. Arbab. Formal semantics and analysis of component connectors in reo. Electronic Notes in Theoretical Computer Science, 154(1):83–99, 2006.- 32
[24] B. Pourvatan, M. Sirjani, H. Hojjat, and F. Arbab. Automated analysis of reo circuits using symbolic execution. Electronic Notes in Theoretical Computer Science, 255:137–158, 2009. -37
[25] S.-S. T. Jongmans and F. Arbab. Overview of thirty semantic formalisms for reo. Scientific Annals of Computer Science, 22(1), 2012.- 24
[26] F. Arbab, C. Baier, F. de Boer, and J. Rutten. Models and temporal logical specifications for timed component connectors. Software & Systems Modeling, 6(1):59–82, 2007. -5
[27] E. Ardeshir-Larijani, A. Farhadi, and F. Arbab. Simulation of hybrid reo connectors. In 2020 CSI/CPSSI International Symposium on Real-Time and Embedded Systems and Technologies (RTEST), pages 1–10. IEEE, 2020.- 8
[28] Y. Li, X. Zhang, Y. Ji, and M. Sun. Capturing stochastic and real-time behavior in reo connectors. In Formal Methods: Foundations and Applications - 20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings, pages 287–304, 2017.
[29] M. Sun and Y. Li. Formal modeling and verification of complex interactions in e-government applications. In Proceedings of the 8th International Conference on Theory and Practice of Electronic Governance, pages 506–507. ACM, 2014.
[30] X. Zhang, W. Hong, Y. Li, and M. Sun. Reasoning about connectors in coq. In International Workshop on Formal Aspects of Component Software, pages 172–190. Springer, 2016.
[31] X. Zhang, W. Hong, Y. Li, and M. Sun. Reasoning about connectors using coq and z3. Science of Computer Programming, 170:27–44, 2019.