Model checking Reo connectors with data streams

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

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

Abstract

System modeling and certification, crucial for critical systems, are high complexity tasks. Using tools for exempt such complexity from developers may grant increased productivity on software construction and validation. Reo is a graphical language focused on coordination, promising to aid modeling of system components interaction. Time Data Streams denote, formally, the data flow in the aforementioned language, allowing model checking against a system execution, performed on this work by the tool nuXmv. Thus, this work proposes a high-level language that allows generic specification for Time Data Streams, along with a translation to the nuXmv model.

Keywords: Verificação de modelos, Reo, Constraint Automata, nuXmv

References

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.