Integrating tools to reason about Reo circuits
Resumo
Critical systems are present in many applications and require high reliability. However, there are still challenges for the verification and certification of these systems. The graphical language Reo is based on coordination and model the communication of software components. A set of existing tools offers compilers and reasoners based on proof assistants and model checkers for Reo-specified systems. This paper proposes the integration of these compilers through an interface that allows building Reo circuits, converting the model to the compilers' input language, simplifying the use of logic tools and allowing the creation of new channels in addition to the canonical ones. The theory used, integrated tools, features of interface and some examples are presented.
Palavras-chave:
Reo, model checkers, proof assistants
Referências
Arbab, F. (2004). Reo: a channel-based coordination model for component composition. Mathematical structures in computer science, 14(3):329–366.
Arbab, F., Koehler, C., Maraikar, Z., Moon, Y.-J., and Proença, J. (2008). Modeling, testing and executing reo connectors with the eclipse coordination tools. Tool demo session at FACS, 8.
Baier, C. and Katoen, J.-P. (2008). Principles of model checking. MIT press.
Baier, C., Sirjani, M., Arbab, F., and Rutten, J. (2006). Modeling component connectors in reo by constraint automata. Science of computer programming, 61(2):75–113.
Dokter, K. and Arbab, F. (2018). Treo: Textual syntax for Reo connectors. arXiv preprint arXiv:1806.09852.
Grilo, E., Toledo, D., and Lopes, B. (2022). A logical framework to reason about Reo circuits. Journal of Applied Logics IFColog Journal of Logic and Their Applications, 9:199–254.
Pierce, B., de Amorim, A., Casinghino, C., Gaboardi, M., Greenberg, M., Hrit¸cu, C., Sjöberg, V., and Yorgey, B. (2018). Software Foundations volume 1: Logical foundations.
Torres, M. A. and Lopes, B. (2020). Verificação de modelos com streams de dados sobre conectores reo. In Anais do I Workshop Brasileiro de Lógica, pages 9–16.
Arbab, F., Koehler, C., Maraikar, Z., Moon, Y.-J., and Proença, J. (2008). Modeling, testing and executing reo connectors with the eclipse coordination tools. Tool demo session at FACS, 8.
Baier, C. and Katoen, J.-P. (2008). Principles of model checking. MIT press.
Baier, C., Sirjani, M., Arbab, F., and Rutten, J. (2006). Modeling component connectors in reo by constraint automata. Science of computer programming, 61(2):75–113.
Dokter, K. and Arbab, F. (2018). Treo: Textual syntax for Reo connectors. arXiv preprint arXiv:1806.09852.
Grilo, E., Toledo, D., and Lopes, B. (2022). A logical framework to reason about Reo circuits. Journal of Applied Logics IFColog Journal of Logic and Their Applications, 9:199–254.
Pierce, B., de Amorim, A., Casinghino, C., Gaboardi, M., Greenberg, M., Hrit¸cu, C., Sjöberg, V., and Yorgey, B. (2018). Software Foundations volume 1: Logical foundations.
Torres, M. A. and Lopes, B. (2020). Verificação de modelos com streams de dados sobre conectores reo. In Anais do I Workshop Brasileiro de Lógica, pages 9–16.
Publicado
31/07/2022
Como Citar
FERREIRA, Mariana; LOPES, Bruno.
Integrating tools to reason about Reo circuits. In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 3. , 2022, Niterói.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2022
.
p. 17-24.
ISSN 2763-8731.
DOI: https://doi.org/10.5753/wbl.2022.222914.
