Formal Verification for Components and Connectors

DOI10.1007/978-3-642-04167-9_5zbMATH Open1254.68143OpenAlexW1553374920MaRDI QIDQ3638992FDOQ3638992

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

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

Mathematics Subject Classification ID

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

Cites Work

• Reo: a channel-based coordination model for component composition
• Characterizing finite Kripke structures in propositional temporal logic
• Alternating-time temporal logic
• Title not available (Why is that?)
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• CCS expressions, finite state processes, and three problems of equivalence
• Modeling component connectors in Reo by constraint automata
• Symbolic model checking for channel-based component connectors
• Dynamic linear time temporal logic
• 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
• Formal design and implementation of constraints in software components
• Component constraint detection based on proposition logic
• Alternating-time stream logic for multi-agent systems
• Most General Property-Preserving Updates
• Compositional construction of most general controllers
• Static and dynamic property-preserving updates
• Automata-based component composition analysis
• Programming and verifying component ensembles
• Using Coq for formal modeling and verification of timed connectors
• Documenting and verifying systems assembled from components
• Symbolic model checking for channel-based component connectors
• Intentional automata: a context-dependent model for component connectors (extended abstract)

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)