Interpreting Reo Circuits as PDL models
Barra lateral de artigos
Conteúdo do artigo principal
Resumo
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.
INTERPRETANDO CIRCUITOS REO COMO MODELOS PDL
Reo é uma linguagem baseada em coordenação com a proposta de conectar diferentes sistemas e interfaces. Objetiva modelar a comunicação entre diferentes sistemas com um alto nível de abstração e sem muitas restrições. PDL é uma lógica multimodal adaptada para raciocinar sobre programas, consistente, completa, decidível e com uma semântica de Kripke simples. Este trabalho pretende fornecer uma interpretação dos circuitos Reo como modelos PDL. Esses são os primeiros passos para fornecer uma lógica dinâmica próppria para raciocinar diretamente sobre os circuitos Reo.
Detalhes do artigo
Nota de Direitos Autorais
O autor do artigo ou resenha submetido e aprovado para publicação autoriza os editores a reproduzi-lo e publicá-lo na a revista O que nos faz pensar, entendendo-se os termos "reprodução" e "publicação" conforme a licença Creative Commons Atribuição-NãoComercial 4.0 Internacional. O artigo ou resenha poderá ser acessado tanto pela rede mundial de computadores (WWW – Internet), como pela versão impressa, sendo permitidas, a título gratuito, a consulta e a reprodução do texto para uso próprio de quem a consulta. Essa autorização de publicação não tem limitação de tempo, ficando os editores da revista O que nos faz pensar responsável pela manutenção da identificação do autor do artigo.
Referências
[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.