Formal Verification for Components and Connectors

DOI10.1007/978-3-642-04167-9_5MaRDI QIDQ3638992zbMATH OpenOpenAlexFDO

Authors Tobias Blechmann, Joachim Klein, Sascha Klüppelholz, Christel Baier

Publication date 28 October 2009

Published in Formal Methods for Components and Objects (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-04167-9_5

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Modeling component connectors in Reo by constraint automata
• SAT-based verification for timed component connectors
• SAT-based verification for timed component connectors
• Automata-based component composition analysis
• Using Coq for formal modeling and verification of timed connectors

Cites work

• Alternating-time temporal logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• CCS expressions, finite state processes, and three problems of equivalence
• Characterizing finite Kripke structures in propositional temporal logic
• Dynamic linear time temporal logic
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Modeling component connectors in Reo by constraint automata
• Reo: a channel-based coordination model for component composition
• Symbolic model checking for channel-based component connectors
• Tableau-based automata construction for dynamic linear time temporal logic

Cited in

(13)

• Reo + \(\mathrm{mCRL2}\): a framework for model-checking dataflow in service compositions
• Static and dynamic property-preserving updates
• Compositional construction of most general controllers
• Symbolic model checking for channel-based component connectors
• Intentional automata: a context-dependent model for component connectors (extended abstract)
• Component constraint detection based on proposition logic
• Documenting and verifying systems assembled from components
• Using Coq for formal modeling and verification of timed connectors
• Programming and verifying component ensembles
• Automata-based component composition analysis
• Most General Property-Preserving Updates
• Formal design and implementation of constraints in software components
• Alternating-time stream logic for multi-agent systems

Describes a project that uses

Uses Software

• Reo

This page was built for publication: Formal Verification for Components and Connectors

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