Modeling and verification of component connectors

Abstract

Connectors have shown their great potential for coordination of different components in the large-scale distributed systems. Formal modeling and verification of connectors becomes more critical due to the rapid growth of the size of connectors. In this paper, we present a novel modeling and verification approach of Reo connectors in Coq, including the timed and probabilistic extensions of Reo. When failing to prove whether a property is satisfiable or not with Coq, Z3 solver can be used to generate counterexamples automatically. To promote automated theorem proving in Coq, we proposed an approach based on recurrent neural networks (RNNs) to predict tactics in the proving process.