Reo + \(\mathrm{mCRL2}\): a framework for model-checking dataflow in service compositions

DOI10.1007/s00165-011-0191-6zbMath1259.68129MaRDI QIDQ1941851

Christian Krause, E. P. de Vink, Natallia Kokash

Publication date: 22 March 2013

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-011-0191-6

zbMATH Keywords

model checking; coordination languages; formal methods for service-oriented computing

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

ReLo: a Dynamic Logic to Reason About Reo Circuits, Combine and conquer: relating BIP and Reo, From symbolic constraint automata to Promela

Uses Software

• PRISM
• CPN/Tools
• mCRL2
• Design/CPN
• TINA
• Reo
• Woflan

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• TINA
• A theory of timed automata
• Connector colouring. I: Synchronisation and context dependency
• Modeling component connectors in Reo by constraint automata
• Verification of Context-Dependent Channel-Based Service Models
• A Coordination Model for Interactive Components
• Logic–Based Detection of Conflicts in Appel Policies
• Analysis of Realizability Conditions for Web Service Choreographies
• Formal Verification for Components and Connectors
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Reo: a channel-based coordination model for component composition