Symbolic model checking for channel-based component connectors

DOI10.1016/J.SCICO.2008.09.020MaRDI QIDQ2389338zbMATH OpenOpenAlexFDO

Authors Sascha Klüppelholz, Christel Baier

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 checkingdata streamsbinary decision diagramsReoconstraint automatabranching time logic

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 4180789
• Automata based model checking for Reo connectors
• Formal Verification for Components and Connectors
• Linear Temporal Logic of Constraint Automata
• A coinductive calculus of component connectors.

Cites work

• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• scientific article; zbMATH DE number 918600 (Why is no real title available?)
• A coinductive calculus of component connectors.
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Branching Programs and Binary Decision Diagrams
• Formal Methods for Components and Objects
• Formal methods for components and objects. First international symposium, FMCO 2002, Leiden, The Netherlands, November 5--8, 2002. Revised lectures
• Graph-Based Algorithms for Boolean Function Manipulation
• Modeling component connectors in Reo by constraint automata
• Propositional dynamic logic of regular programs
• Reo: a channel-based coordination model for component composition

Cited in

(8)

• Formal Verification for Components and Connectors
• Alternating-time stream logic for multi-agent systems
• Synthesis of Reo circuits from scenario-based interaction specifications
• Connector rewriting with high-level replacement systems
• Symbolic execution of Reo circuits using constraint automata
• Synthesis of Reo circuits from scenario-based specifications
• Using Coq for formal modeling and verification of timed connectors
• Comparing three coordination models: Reo, ARC, and PBRD

Describes a project that uses

Uses Software

• Reo

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2389338)