Reasoning about connectors using Coq and Z3
| Autor: | Xiyue Zhang, Meng Sun, Yi Li, Weijiang Hong |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Programming language
Computer science 020207 software engineering 02 engineering and technology Coordination language computer.software_genre Cable gland TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 020204 information systems Satisfiability modulo theories Bounded function 0202 electrical engineering electronic engineering information engineering Equivalence (formal languages) computer Software Axiom Communication channel Counterexample |
| Zdroj: | Science of Computer Programming. 170:27-44 |
| ISSN: | 0167-6423 |
| DOI: | 10.1016/j.scico.2018.10.002 |
| Popis: | Reo is a channel-based exogenous coordination language in which complex coordinators, called connectors, are compositionally built out of simpler ones. In this paper, we present an approach to model and reason about connectors using Coq and Z3. Both models reflect the original structure of connectors as closely as possible. In our framework, both basic connectors (channels) and composition operations are modeled as axioms. Then complex connectors are modeled as the combination of logical predicates which correspond to simpler connectors. With such definitions provided, connector properties, as well as equivalence and refinement relations between different connectors, can be formalized as goals in Coq and proved using pre-defined tactics, if satisfied by connectors. When failing to prove whether a property is satisfiable or not with Coq, we use Z3, an SMT solver, to search for possible bounded counter examples automatically. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect