Symbolic model checking for channel-based component connectors

DOI10.1016/j.scico.2008.09.020zbMath1167.68035OpenAlexW2000050281MaRDI QIDQ2389338

Christel Baier, Sascha Klüppelholz

Publication date: 15 July 2009

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2008.09.020

zbMATH Keywords

model checkingbinary decision diagramsdata streamsReoconstraint automatabranching time logic

Mathematics Subject Classification ID

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

Related Items (7)

Comparing three coordination models: Reo, ARC, and PBRD ⋮ Symbolic execution of Reo circuits using constraint automata ⋮ Alternating-time stream logic for multi-agent systems ⋮ Synthesis of Reo circuits from scenario-based interaction specifications ⋮ Synthesis of Reo Circuits from Scenario-based Specifications ⋮ Formal Verification for Components and Connectors ⋮ Connector Rewriting with High-Level Replacement Systems

Uses Software

• Reo

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Propositional dynamic logic of regular programs
• Formal methods for components and objects. First international symposium, FMCO 2002, Leiden, The Netherlands, November 5--8, 2002. Revised lectures
• Modeling component connectors in Reo by constraint automata
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Branching Programs and Binary Decision Diagrams
• Reo: a channel-based coordination model for component composition
• Formal Methods for Components and Objects
• Recent Trends in Algebraic Development Techniques

This page was built for publication: Symbolic model checking for channel-based component connectors