2 Search Results for "Sifakis, Joseph"

Document
DOI: 10.4230/LIPIcs.CONCUR.2016.30
Parameterized Systems in BIP: Design and Model Checking

Authors: Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, and Joseph Sifakis

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
BIP is a component-based framework for system design that has important industrial applications. BIP is built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP to systems parameterized in the number of components. We show that FOIL captures classical parameterized architectures such as token-passing rings, cliques of identical components communicating with rendezvous or broadcast, and client-server systems. Although the BIP framework includes efficient verification tools for statically-defined systems, none are available for parameterized systems with an unbounded number of components. The parameterized model checking literature contains a wealth of techniques for systems of classical architectures. However, application of these results requires a deep understanding of parameterized model checking techniques and their underlying mathematical models. To overcome these difficulties, we introduce a framework that automatically identifies parameterized model checking techniques applicable to a BIP design. To our knowledge, it is the first framework that allows one to apply prominent parameterized model checking results in a systematic way.
Cite as

Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, and Joseph Sifakis. Parameterized Systems in BIP: Design and Model Checking. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{konnov_et_al:LIPIcs.CONCUR.2016.30,
  author =	{Konnov, Igor and Kotek, Tomer and Wang, Qiang and Veith, Helmut and Bliudze, Simon and Joseph Sifakis},
  title =	{{Parameterized Systems in BIP: Design and Model Checking}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.30},
  URN =		{urn:nbn:de:0030-drops-61670},
  doi =		{10.4230/LIPIcs.CONCUR.2016.30},
  annote =	{Keywords: Rigorous system design, BIP, verification, parameterized model checking}
}
Document
DOI: 10.4230/DagSemProc.08331.5
Modeling Heterogeneous Real-time Components in BIP

Authors: Ananda Basu, Marius Bozga, and Joseph Sifakis

Published in: Dagstuhl Seminar Proceedings, Volume 8331, Perspectives Workshop: Model Engineering of Complex Systems (MECS) (2008)

Abstract
We present a methodology for modeling heterogeneous real-time components. Components are obtained as the superposition of three layers : Behavior, specified as a set of transitions; Interactions between transitions of the behavior; Priorities, used to choose amongst possible interactions. A parameterized binary composition operator is used to compose components layer by layer. We present the BIP language for the description and composition of layered components as well as associated tools for executing and analyzing components on a dedicated platform. The language provides a powerful mechanism for structuring interactions involving rendezvous and broadcast. We show that synchronous and timed systems are particular classes of components. Finally, we provide examples showing the utility of the BIP framework in heterogeneous component modeling.
Cite as

Ananda Basu, Marius Bozga, and Joseph Sifakis. Modeling Heterogeneous Real-time Components in BIP. In Perspectives Workshop: Model Engineering of Complex Systems (MECS). Dagstuhl Seminar Proceedings, Volume 8331, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{basu_et_al:DagSemProc.08331.5,
  author =	{Basu, Ananda and Bozga, Marius and Sifakis, Joseph},
  title =	{{Modeling Heterogeneous Real-time Components in BIP}},
  booktitle =	{Perspectives Workshop: Model Engineering of Complex Systems (MECS)},
  pages =	{1--10},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8331},
  editor =	{Uwe A{\ss}mann and Jean B\'{e}zivin and Richard Paige and Bernhard Rumpe and Douglas C. Schmidt},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08331.5},
  URN =		{urn:nbn:de:0030-drops-16026},
  doi =		{10.4230/DagSemProc.08331.5},
  annote =	{Keywords: Component based construction, Heterogeneous systems, Modeling and simulation, Code generation}
}
  • Refine by Author
  • 1 Basu, Ananda
  • 1 Bliudze, Simon
  • 1 Bozga, Marius
  • 1 Joseph Sifakis
  • 1 Konnov, Igor
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 1 BIP
  • 1 Code generation
  • 1 Component based construction
  • 1 Heterogeneous systems
  • 1 Modeling and simulation
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2008
  • 1 2016

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact