Modeling and verification of component connectors in Coq
In: Science of Computer Programming, Jg. 113 (2015-12-01), S. 285-301
Online
unknown
Zugriff:
We present a new approach to modeling of Reo connectors via the Coq proof assistant.We propose a simulation-based approach to verify connectors' properties specified in LTL.We investigate an access control system to show the usefulness of the approach. 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.
Titel: |
Modeling and verification of component connectors in Coq
|
---|---|
Autor/in / Beteiligte Person: | Li, Yi ; Sun, Meng |
Link: | |
Zeitschrift: | Science of Computer Programming, Jg. 113 (2015-12-01), S. 285-301 |
Veröffentlichung: | Elsevier BV, 2015 |
Medientyp: | unknown |
ISSN: | 0167-6423 (print) |
DOI: | 10.1016/j.scico.2015.10.016 |
Schlagwort: |
|
Sonstiges: |
|