Compilação de Código Certificado para Modelos Reo

  • Erick Grillo UFF
  • Bruno Lopes UFF

Resumo


Sistemas críticos são sistemas que necessitam de alta confiabilidade e estão presentes nos mais variados domínios. Em caso de falha, tais sistemas podem provocar problemas sérios, causando prejuízos financeiros e até morte. A engenharia de software padrão não é o suficiente para garantir o nível requerido de confiabilidade. Reo é uma linguagem gráfica de modelagem baseada em coordenação cujo foco é em modelar a interação de sistemas por meio do uso de primitivas comuns em sistemas distribuídos. Constraint Automata são definidos como a semântica formal primitiva para Reo, providenciando meios formais para raciocinar sobre e provar propriedades acerca de modelos Reo. O presente trabalho descreve uma formalização de Constraint Automata no assistente de provas Coq, onde os principais formalismos da teoria são formalizados, junto de uma operação de composição.

Palavras-chave: Sistemas críticos, Engenharia de software, Modelagem gráfica, Reo, Constraint Automata

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. (2006). Coordination for component composition. Electronic Notes in Theoretical Computer Science, 160:15 – 40. Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 2005).

Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C., Paulin-Mohring, C., and Werner, B. (1992). The COQ Proof Assistant: User’s Guide: Version 5.6. INRIA.

Gerhart, S., Craigen, D., and Ralston, T. (1994). Case study: Paris metro signaling system. IEEE Software, 11(1):32–28.

Grilo, E. and Lopes, B. (2018). Formalization and certification of software for smart cities. In International Joint Conference on Neural Networks (IJCNN), pages 662–669. IEEE.

Knight, J. C. (2002). Safety critical systems: challenges and directions. In Proceedings of the 24th International Conference on Software Engineering, pages 547–550. ACM.

Kokash, N. and Arbab, F. (2009). Formal Behavioral Modeling and Compliance Analysis for Service-Oriented Systems, pages 21–41. Springer Berlin Heidelberg, Berlin, Heidelberg.

Loveland, D. W. (2014). Automated Theorem Proving: a logical basis. Elsevier.

Zhang, X., Hong, W., Li, Y., and Sun, M. (2016). Reasoning about connectors in coq. In International Workshop on Formal Aspects of Component Software, pages 172–190. Springer.
Publicado
20/04/2019
GRILLO, Erick; LOPES, Bruno. Compilação de Código Certificado para Modelos Reo. 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. 29-32.