Inproceedings1357745150: Unterschied zwischen den Versionen

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
(Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christel |ErsterAutorNachname=Baier |FurtherAuthors=Tobias Blechmann; Joachim Klein; Sascha Klüppelholz}} {{Inproceedings |Booktitle=Proc. of the 7th International Symposium on Formal Methods for Components and Objects (FMCO) |Pages=82--101 |Publisher=Springer |Series=Lecture Notes in Computer Science |Title=Formal Verification for Components and Connectors |Volume=5751 |Year=2008 }} {{Publikati…“)
 
Johannes Lehmann (Diskussion | Beiträge)
K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“)
 
Zeile 15: Zeile 15:
|DOI Name=10.1007/978-3-642-04167-9_5
|DOI Name=10.1007/978-3-642-04167-9_5
|Abstract=In previous work, constraint automata have been introduced as a uniform model for behavioral interfaces of components, (possibly dynamic) component connectors and systems consisting of several components and their glue code. The purpose of the paper is to provide an overview of the techniques for specifying and verifying temporal requirements, conditions on the data flow at the I/O-ports of components and alternating-time properties that have been designed for constraint automata. The paper presents the syntax and semantics of the logics, sketches the model checking algorithms, summarizes the main features of the implementation within the tool Vereofy and reports on experimental studies.
|Abstract=In previous work, constraint automata have been introduced as a uniform model for behavioral interfaces of components, (possibly dynamic) component connectors and systems consisting of several components and their glue code. The purpose of the paper is to provide an overview of the techniques for specifying and verifying temporal requirements, conditions on the data flow at the I/O-ports of components and alternating-time properties that have been designed for constraint automata. The paper presents the syntax and semantics of the logics, sketches the model checking algorithms, summarizes the main features of the implementation within the tool Vereofy and reports on experimental studies.
|Forschungsgruppe=Verifikation und formale quantitative Analyse
|Forschungsgruppe=Algebraische und logische Grundlagen der Informatik
}}
}}

Aktuelle Version vom 5. März 2025, 14:40 Uhr

Toggle side column

Formal Verification for Components and Connectors

Christel BaierChristel Baier,  Tobias BlechmannTobias Blechmann,  Joachim KleinJoachim Klein,  Sascha KlüppelholzSascha Klüppelholz
Christel Baier, Tobias Blechmann, Joachim Klein, Sascha Klüppelholz
Formal Verification for Components and Connectors
Proc. of the 7th International Symposium on Formal Methods for Components and Objects (FMCO), volume 5751 of Lecture Notes in Computer Science, 82--101, 2008. Springer
  • KurzfassungAbstract
    In previous work, constraint automata have been introduced as a uniform model for behavioral interfaces of components, (possibly dynamic) component connectors and systems consisting of several components and their glue code. The purpose of the paper is to provide an overview of the techniques for specifying and verifying temporal requirements, conditions on the data flow at the I/O-ports of components and alternating-time properties that have been designed for constraint automata. The paper presents the syntax and semantics of the logics, sketches the model checking algorithms, summarizes the main features of the implementation within the tool Vereofy and reports on experimental studies.
  • Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-04167-9_5.
@inproceedings{BBKK2008,
  author    = {Christel Baier and Tobias Blechmann and Joachim Klein and Sascha
               Kl{\"{u}}ppelholz},
  title     = {Formal Verification for Components and Connectors},
  booktitle = {Proc. of the 7th International Symposium on Formal Methods for
               Components and Objects (FMCO)},
  series    = {Lecture Notes in Computer Science},
  volume    = {5751},
  publisher = {Springer},
  year      = {2008},
  pages     = {82--101},
  doi       = {10.1007/978-3-642-04167-9_5}
}