Verificação de modelos com streams de dados sobre conectores Reo

• Mateus Azeredo Torres UFF
• Bruno Lopes UFF http://orcid.org/0000-0003-1204-0176

DOI: https://doi.org/10.5753/wbl.2020.11453

Resumo

A modelagem e certificação de sistemas, cruciais em sistemas críticos, são tarefas de alto teor de complexidade. O uso de ferramentas que isentem desenvolvedores dessa complexidade permite maior agilidade na construção e validação de software. Reo é uma linguagem gráfica focada em coordenações, promissora para facilitar a modelagem da interação de componentes de sistema. Timed Data Streams denotam, formalmente, o fluxo dos dados nessa linguagem, possibilitando a verificação de um modelo em relação a uma execução de sistema, feita nesse trabalho pela ferramenta nuXmv. Diante disso, este trabalho propõe uma linguagem em alto nível que permita a especificação genérica para Timed Data Streams, junto de uma tradução para o modelo nuXmv.

Palavras-chave: Verificação de modelos, Reo, Constraint Automata, nuXmv

Referências

Arbab, F. (2004).“Reo: a channel-based coordination model for component composition”. Math. Struct. in Comp. Science, vol.14, pp.329–36. Cambridge University.

Arbab, F. (2006).“Coordination for Component Composition”. Electronic Notes inTheoretical Comp. Science vol.160, pp.15–40. Elsevier.

Arena, D. (2019).“Um compilador de circuitos Reo para modelos nuXmv”. Trabalho de conclusão de curso - Instituto de Computação, Universidade Federal Fluminense.

Baier C, Sirjanib M, A. F. and Ruttend, J. (2006).“Modeling component connectors in Reo by constraint automata”. Science of Comp. Programming, vol.61, pp.75–113. Elsevier.

Cavada R, e. a. (2014).The nuXmv Symbolic Model Checker. In:Biere A., Bloem R.(eds).CAV 2014. Lecture Notes in Computer Science, vol 8559. Springer, Cham

Kokash, N. (2012).“Reo +mCRL2: A framework for model-checking dataflow in service compositions”. Formal Aspects of Computing, vol.24, no2, pp.187-216. Hasso Plattner Institute.