Article609517984: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Sascha |ErsterAutorNachname=Klüppelholz |FurtherAuthors=Christel Baier}} {{Article |Journal=Science of Computer Programming |Number=9 |Pages=688--701 |Title=Symbolic model checking for channel-based component connectors |Volume=74 |Year=2009 }} {{Publikation Details |DOI Name=10.1016/J.SCICO.2008.09.020 |Abstract=This paper introduces a temporal logic framework to reason about the coordination…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 14: | Zeile 14: | ||
|DOI Name=10.1016/J.SCICO.2008.09.020 | |DOI Name=10.1016/J.SCICO.2008.09.020 | ||
|Abstract=This paper introduces a temporal logic framework to reason about the coordination mechanisms and data flow of exogenous coordination models. We take a CTL-like branching time logic, augmented with regular expressions that specify the observable I/O-operations, as a starting point. The paper provides the syntax and semantics of our logic and introduces the corresponding model checking algorithm. The second part of the paper reports an implementation that relies on a symbolic representation of the coordination network and the connected components by means of binary decision diagrams. A couple of examples are given to illustrate the efficiency of the model checking techniques and their implementation. | |Abstract=This paper introduces a temporal logic framework to reason about the coordination mechanisms and data flow of exogenous coordination models. We take a CTL-like branching time logic, augmented with regular expressions that specify the observable I/O-operations, as a starting point. The paper provides the syntax and semantics of our logic and introduces the corresponding model checking algorithm. The second part of the paper reports an implementation that relies on a symbolic representation of the coordination network and the connected components by means of binary decision diagrams. A couple of examples are given to illustrate the efficiency of the model checking techniques and their implementation. | ||
|Forschungsgruppe= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 14:43 Uhr
Symbolic model checking for channel-based component connectors
Sascha KlüppelholzSascha Klüppelholz, Christel BaierChristel Baier
Sascha Klüppelholz, Christel Baier
Symbolic model checking for channel-based component connectors
Science of Computer Programming, 74(9):688--701, 2009
Symbolic model checking for channel-based component connectors
Science of Computer Programming, 74(9):688--701, 2009
- KurzfassungAbstract
This paper introduces a temporal logic framework to reason about the coordination mechanisms and data flow of exogenous coordination models. We take a CTL-like branching time logic, augmented with regular expressions that specify the observable I/O-operations, as a starting point. The paper provides the syntax and semantics of our logic and introduces the corresponding model checking algorithm. The second part of the paper reports an implementation that relies on a symbolic representation of the coordination network and the connected components by means of binary decision diagrams. A couple of examples are given to illustrate the efficiency of the model checking techniques and their implementation. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@article{KB2009,
author = {Sascha Kl{\"{u}}ppelholz and Christel Baier},
title = {Symbolic model checking for channel-based component connectors},
journal = {Science of Computer Programming},
volume = {74},
number = {9},
year = {2009},
pages = {688--701},
doi = {10.1016/J.SCICO.2008.09.020}
}
