Using Coq and Recurrent Neural Network to Model and Verify Timed Connectors

2/7/2018

By Prof. Meng Sun, Peking University, China.

Abstract. Formal modeling and verification of connectors in component-based software systems are getting more interest with recent advancements and evolution in modern software systems. In this work, we use the proof assistant Coq for modeling and verification of timed connectors. Timed channels and the composition operators for constructing timed connectors are defined in Coq. Basic timed channels are interpreted as axioms and inference rules are used for building complex connectors. Timed connectors being built by composing basic timed / untimed channels, are defined as logical predicates which describe the relations between inputs and outputs. Various properties of timed connectors can be specified as high-order logic propositions and verified using theorem proving techniques. Furthermore, we propose an approach based on recurrent neural networks (RNNs) to predict the correct tactics in the proving process. Under this framework, properties of timed connectors can be naturally formalized and semi-automatically proved in Coq.

Keywords. Software engineering, Formal modeling, recurrent neural networks, Coq.

About the Speaker. Meng Sun is a professor at Department of Informatics, School of Mathematical Sciences, Peking University. He received Bachelor and PhD degrees in applied mathematics from Peking University in 1999 and 2005. He then spent one year as a postdoctoral researcher at National University of Singapore. From 2006 to 2010, he worked as a scientific staff member at CWI. He has been a faculty member of Peking University since 2010 and became a full professor in 2017. His research interests include software engineering, formal methods, software verification and testing, coordination models and languages, coalgebra theory, cyber-physical systems, service-oriented and cloud computing, big data analysis.