Modeling and verification of component connectors in Coq

被引：6

作者：

Li, Yi ^{[1
]}

Sun, Meng ^{[1
]}

机构：

[1] Peking Univ, Sch Math Sci, LMAM & DI, Beijing 100871, Peoples R China

来源：

SCIENCE OF COMPUTER PROGRAMMING | 2015年 / 113卷

基金：

高等学校博士学科点专项科研基金; 中国国家自然科学基金;

关键词：

Coordination; Reo; Connector; Coq; Verification; COORDINATION; CHECKING; REO;

D O I：

10.1016/j.scico.2015.10.016

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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 A.-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. (C) 2015 Elsevier B.V. All rights reserved.

引用

页码：285 / 301

页数：17

共 24 条

[11] Coordination models and languages as software integrators [J].

Ciancarini, P .

ACM COMPUTING SURVEYS, 1996, 28 (02) :300-302

[12] Connector colouring I: Synchronisation and context dependency [J].

Clarke, Dave ;

Costa, David ;

Arbab, Farhad .

SCIENCE OF COMPUTER PROGRAMMING, 2007, 66 (03) :205-225

[13] Bounded model checking using satisfiability solving [J].

Clarke, E ;

Biere, A ;

Raimi, R ;

Zhu, Y .

FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (01) :7-34

[14]

Halpern Joseph Y., 1991, ARTIFICIAL INTELLIGE, P325

[15]

Khosravi R, 2008, LECT NOTES COMPUT SC, V5052, P169, DOI 10.1007/978-3-540-68265-3_11

[16] Symbolic model checking for channel-based component connectors [J].

Klueppelholz, Sascha ;

Baier, Christel .

SCIENCE OF COMPUTER PROGRAMMING, 2009, 74 (09) :688-701

[17] Reo+mCRL2: A framework for model-checking dataflow in service compositions [J].

Kokash, Natallia ;

Krause, Christian ;

de Vink, Erik .

FORMAL ASPECTS OF COMPUTING, 2012, 24 (02) :187-216

[18] Service specification by composition of collaborations - An example [J].

Kraemer, Frank Alexander ;

Herrmann, Peter .

2006 IEEE/WIC/ACM INTERNATIONAL CONFERENCE ON WEB INTELLIGENCE AND INTELLIGENT AGENT TECHNOLOGY, WORKSHOPS PROCEEDINGS, 2006, :129-+

[19] Modeling and Analysis of Component Connectors in Coq [J].

Li, Yi ;

Sun, Meng .

FORMAL ASPECTS OF COMPONENT SOFTWARE, 2014, 8348 :273-290

[20] Connectors as designs: Modeling, refinement and test case generation [J].

Meng, Sun ;

Arbab, Farhad ;

Aichernig, Bernhard K. ;

Astefanoaei, Lacramioara ;

de Boer, Frank S. ;

Rutten, Jan .

SCIENCE OF COMPUTER PROGRAMMING, 2012, 77 (7-8) :799-822

← 1 2 3 →