English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Compositional coordination models such as Reo provide powerful support for the development of large-scale distributed systems by allowing construction of complex connectors that coordinate behavior among different components. The reliability of such distributed systems highly depends on the correctness of connectors. In this paper, we use the proof assistant PVS for formal modeling, analysis and verification of component connectors. We first present the modeling of primitive channels and the composition operators that are used to combine channels for building complex connectors. Furthermore, we show how to model and analyze connector’s behavior in PVS and prove some interesting connector properties. The model reflects the original topological structure of connectors simply and clearly. With the provided approach, different kinds of connector properties can be naturally formalized and proved in PVS.

Reo2PVS: Formal Specification and Verification of Component Connectors