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

• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• 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
• 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)

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

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)