Compilation of Certified Code for Reo Models
Abstract
Critical Systems are systems which require high reliability and are present in a wide variety of domains. Should they fail, serious problems can occur, resulting in financial loss and even deaths. Standard software engineering techniques does not suffice in guaranteeing the required level of reliability. Reo is a graphical modelling language based in coordination which focuses on model system interaction by means of common primitives in distributed systems. Constraint Automata are defined as primitive formal semantics for Reo, providing means to reason about and prove properties of Reo models. The present work describes a formalization of Constraint Automata in Coq proof assistant, regarding its main formalisms, including a compositional operation.
References
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.
