Verificação de modelos Reo com nuXmv
Resumo
Com o advento de sistemas críticos no mundo moderno, a necessidade de validá-los também aumentou. Essa necessidade se deve ao fato de que a falha desses sistemas pode acarretar consequências catastróficas, portanto é necessário garantir que esses programas não vão falhar. Reo é uma linguagem de coordenação de modelagem gráfica que toma vantagem das características naturais dos sistemas distribuídos como transferências de dados e chamadas de funções remotas para modelar esses sistemas. Verificadores de modelos são ferramentas utilizadas para verificar e validar propriedades e características a cerca de modelos. Esse artigo propõe um compilador para gerar um modelo nuXmv (um checador de modelos simbólico) a partir de um modelo Reo.
Palavras-chave:
Sistemas críticos, Reo, Modelagem gráfica, nuXmv, Checador de modelos simbólico
Referências
Arbab, F. (2004). Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science, 14:329–366.
Arbab, F., Baier, C., Rutten, J., and Sirjani, M. (2004). Modeling component connectors in Reo by constraint automata: (extended abstract). Electronic Notes in Theoretical Computer Science, 97:25–46.
Baier, C. and Katoen, J.-P. (2008). Principles of Model Checking. The MIT Press.
Bochot, T., Virelizier, P., Waeselynck, H., and Wiels, V. (2009). Model checking flight control systems: The airbus experience. In Software Engineering-Companion Volume, 2009. ICSE-Companion 2009. 31st International Conference on, pages 18–27. IEEE.
Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., and Tonetta, S. (2014). The nuxmv symbolic model checker. In Biere, A. and Bloem, R., editors, CAV, volume 8559 of Lecture Notes in Computer Science, pages 334–342. Springer.
Gerhart, S., Craigen, D., and Ralston, T. (1994). Case study: Paris metro signaling system. IEEE Software, 11(1):32–28.
Knight, J. C. (2002). Safety critical systems: challenges and directions. In Proceedings of the 24th International Conference on Software Engineering, pages 547–550. ACM.
Arbab, F., Baier, C., Rutten, J., and Sirjani, M. (2004). Modeling component connectors in Reo by constraint automata: (extended abstract). Electronic Notes in Theoretical Computer Science, 97:25–46.
Baier, C. and Katoen, J.-P. (2008). Principles of Model Checking. The MIT Press.
Bochot, T., Virelizier, P., Waeselynck, H., and Wiels, V. (2009). Model checking flight control systems: The airbus experience. In Software Engineering-Companion Volume, 2009. ICSE-Companion 2009. 31st International Conference on, pages 18–27. IEEE.
Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., and Tonetta, S. (2014). The nuxmv symbolic model checker. In Biere, A. and Bloem, R., editors, CAV, volume 8559 of Lecture Notes in Computer Science, pages 334–342. Springer.
Gerhart, S., Craigen, D., and Ralston, T. (1994). Case study: Paris metro signaling system. IEEE Software, 11(1):32–28.
Knight, J. C. (2002). Safety critical systems: challenges and directions. In Proceedings of the 24th International Conference on Software Engineering, pages 547–550. ACM.
Publicado
20/04/2019
Como Citar
TOLEDO, Daniel; LOPES, Bruno.
Verificação de modelos Reo com nuXmv. In: ESCOLA REGIONAL DE INFORMÁTICA DO RIO DE JANEIRO (ERI-RJ), 3. , 2019, Niterói.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2019
.
p. 33-36.
