# Modeling and Analysis of Reo Connectors Using Alloy

@inproceedings{Khosravi2008ModelingAA, title={Modeling and Analysis of Reo Connectors Using Alloy}, author={Ramtin Khosravi and Marjan Sirjani and Nesa Asoudeh and Shaghayegh Sherry Sahebi and Hamed Iravanchi}, booktitle={COORDINATION}, year={2008} }

Reo is an exogenous coordination language based on a calculus of channel composition. Different formal models have been developed for this language. In this paper, we present a new approach to modeling and analysis of Reo connectors using Alloy which is a lightweight modeling language based on first-order relational logic. We provide a reusable library of Reo channels in Alloy that can be used to create a model of a Reo connector in Alloy. The model is simple and reflects the original structure… Expand

#### 24 Citations

Modeling and verification of component connectors in Coq

- Computer Science
- Sci. Comput. Program.
- 2015

This paper presents a new approach to modeling and verification of Reo connectors via Coq, a proof assistant based on higher-order logic and λ-calculus, and proposes a simulation-based approach to verify connectors' properties specified in LTL. Expand

Reasoning about connectors using Coq and Z3

- Computer Science
- Sci. Comput. Program.
- 2019

This paper presents an approach to model and reason about connectors using Coq and Z3, a channel-based exogenous coordination language in which complex coordinators, called connectors, are compositionally built out of simpler ones. Expand

Modeling and Analysis of Component Connectors in Coq

- Computer Science
- FACS
- 2013

This paper presents a new approach to modeling and analysis of Reo connectors via Coq, a proof assistant based on high-order logic and \(\lambda \)-calculus that can automatically prove connectors’ properties using the Coq proof assistant. Expand

Encoding Context-Sensitivity in Reo into Non-Context-Sensitive Semantic Models

- Computer Science, Biology
- COORDINATION
- 2011

This paper shows that context-dependency in Reo can be encoded in basic semantic models, namely connector coloring with two colors and constraint automata, by introducing additional fictitious ports for Reo's primitives. Expand

Reo2PVS: Formal Specification and Verification of Component Connectors

- Computer Science
- SEKE
- 2018

This paper uses the proof assistant PVS for formal modeling, analysis and verification of component connectors and presents the modeling of primitive channels and the composition operators that are used to combine channels for building complex connectors. Expand

A model of context-dependent component connectors

- Computer Science
- Sci. Comput. Program.
- 2012

An intuitive automata-based formal model of context-dependent connectors is presented, and it is argued that it is superior to previous attempts at such a model for the coordination language Reo. Expand

Reasoning About Connectors in Coq

- Computer Science
- FACS
- 2016

A new approach to model connectors in Coq which is a proof assistant based on higher-order logic and \(\lambda \)-calculus is presented which reflects the original structure of connectors simply and clearly. Expand

Automata for Context-Dependent Connectors

- Computer Science
- COORDINATION
- 2009

This paper presents an intuitive automata-based formal model of context-dependent connectors, and argues that it is superior to previous attempts at such a model for the coordination language Reo. Expand

Input-output Conformance Testing for Channel-based Service Connectors

- Computer Science
- PACO
- 2011

An approach for model-based testing of coordination protocols designed in Reo is presented based on the input-output conformance (ioco) testing theory and exploits the mapping of automata-based semantic models for Reo to equivalent process algebra specifications. Expand

Using Coq for Formal Modeling and Verification of Timed Connectors

- Computer Science
- SEFM Workshops
- 2017

This paper uses the proof assistant Coq for modeling and verification of timed connectors and presents the definition of timed channels and the composition operators for constructing timed connectors in Coq, finding timed connector properties can be naturally formalized and proved in Coqu. Expand

#### References

SHOWING 1-10 OF 14 REFERENCES

Reo: a channel-based coordination model for component composition

- Computer Science
- Mathematical Structures in Computer Science
- 2004

It is shown that exogenous coordination patterns that can be expressed as (meta-level) regular expressions over I/O operations can be composed in Reo out of a small set of only five primitive channel types. Expand

Formal Semantics and Analysis of Component Connectors in Reo

- Computer Science
- Electron. Notes Theor. Comput. Sci.
- 2006

An operational semantics for a component composition language called Reo, which allows the rewriting engine and the model-checking module in the Maude tool-set to symbolically run and model-check the behavior of Reo connectors. Expand

Modeling component connectors in Reo by constraint automata

- Computer Science, Mathematics
- Sci. Comput. Program.
- 2006

This paper covers the foundations for building tools to address concerns such as the automated construction of the automaton for a given component connector, equivalence checking or containment checking of the behavior of two given connectors, and verification of coordination mechanisms. Expand

A Coinductive Calculus of Component Connectors

- Computer Science
- WADT
- 2002

A simple and transparent semantical model for Reo, in which connectors are relations on timed data streams, and coinduction is the main reasoning principle and it is used to prove properties such as connector equivalence. Expand

Symbolic Model Checking for Channel-based Component Connectors

- Computer Science
- Electron. Notes Theor. Comput. Sci.
- 2007

The paper reports on the foundations and experimental results with a model checker for component connectors modelled by networks of channels in the calculus Reo, which relies on variants of standard automata-based approaches and model checking for CTL-like logics. Expand

Extraction of Structured Programs from Specification Proofs

- Computer Science
- WADT
- 1999

This paper presents a method using an extended logical system for obtaining programs from specifications written in a sublanguage of CASL, and provides a method for producing a program module that maximally respects the original structure of the specification. Expand

A simple process algebra based on atomic actions with resources

- Mathematics, Computer Science
- Mathematical Structures in Computer Science
- 2004

A congruence theorem is proved relating the two semantics, which implies the operational model itself is compositional, and implies the denotational model is adequate with respect to the operational semantics. Expand

Software Abstractions - Logic, Language, and Analysis

- Computer Science
- 2006

This revised edition of Software Abstractions updates the text, examples, and appendixes to be fully compatible with the latest version of Alloy, a language that captures the essence of software abstractions simply and succinctly, using a minimal toolkit of mathematical notions. Expand

Connector Colouring I: Synchronisation and Context Dependency

- Computer Science
- Electron. Notes Theor. Comput. Sci.
- 2006

This paper proposes a scheme based on connector colouring for determining the behaviour of a Reo connector by resolving its synchronisation and exclusion constraints, and models Reo connectors more closely to their envisaged semantics than existing formal models. Expand

Coordination Models and Languages

- Computer Science
- Adv. Comput.
- 1998

This chapter defines and presents in sufficient detail the fundamental concepts of what constitutes a coordination model or language and describes the main existing coordination models and languages as either ``data-driven'' or ``control-driven'''' (also called ``process-'''' or ``task-oriented''). Expand