Compilação de Código Certificado para Modelos Reo
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.
Referências
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.
