Modeling and verification of component connectors in Coq

摘要

Connectors have emerged as a powerful concept for composition and coordination of concurrent activities encapsulated as components and services. Compositional coordination languages, like Reo, serve as a means to formally specify and implement connectors. They support large-scale distributed applications by allowing construction of complex component connectors out of simpler ones. In this paper, we present a new approach to modeling and verification of Reo connectors via Coq, a proof assistant based on higher-order logic and λ-calculus. Basic notions in Reo, like nodes and channels, are defined by inductive types. By tracing the data streams, we provide a method for simulation of the behavior and output of a given Reo connector. With input constraints specified, connectors' properties can be proved by induction. Furthermore, properties specified in LTL can be verified using a simulation-based model-checking approach. An access control system is investigated to show our approach.