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

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

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item

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