Search Results

Documents authored by Bozga, Marius

Document
DOI: 10.4230/LIPIcs.CONCUR.2022.24
On an Invariance Problem for Parameterized Concurrent Systems

Authors: Marius Bozga, Lucas Bueri, and Radu Iosif

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We consider concurrent systems consisting of replicated finite-state processes that synchronize via joint interactions in a network with user-defined topology. The system is specified using a resource logic with a multiplicative connective and inductively defined predicates, reminiscent of Separation Logic [John C. Reynolds, 2002]. The problem we consider is if a given formula in this logic defines an invariant, namely whether any model of the formula, following an arbitrary firing sequence of interactions, is transformed into another model of the same formula. This property, called havoc invariance, is quintessential in proving the correctness of reconfiguration programs that change the structure of the network at runtime. We show that the havoc invariance problem is many-one reducible to the entailment problem ϕ ⊧ ψ, asking if any model of ϕ is also a model of ψ. Although, in general, havoc invariance is found to be undecidable, this reduction allows to prove that havoc invariance is in 2EXP, for a general fragment of the logic, with a 2EXP entailment problem.
Cite as

Marius Bozga, Lucas Bueri, and Radu Iosif. On an Invariance Problem for Parameterized Concurrent Systems. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bozga_et_al:LIPIcs.CONCUR.2022.24,
  author =	{Bozga, Marius and Bueri, Lucas and Iosif, Radu},
  title =	{{On an Invariance Problem for Parameterized Concurrent Systems}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.24},
  URN =		{urn:nbn:de:0030-drops-170874},
  doi =		{10.4230/LIPIcs.CONCUR.2022.24},
  annote =	{Keywords: parameterized verification, invariant checking, resource logics, reconfigurable systems, tree automata}
}
Document
DOI: 10.4230/LITES-v006-i001-a001
Local Planning Semantics: A Semantics for Distributed Real-Time Systems

Authors: Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, and Marius Bozga

Published in: LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1

Abstract
Design, implementation and verification of distributed real-time systems are acknowledged to be very hard tasks. Such systems are prone to different kinds of delay, such as execution time of actions or communication delays implied by distributed platforms. The latter increase considerably the complexity of coordinating the parallel activities of running components. Scheduling such systems must cope with those delays by proposing execution strategies  ensuring global consistency while satisfying the imposed timing constraints. In this paper, we investigate a formal model for such systems as compositions of timed automata subject to multiparty interactions, and propose a semantics aiming to overcome the communication delays problem through anticipating the execution of interactions. To be effective in a distributed context, scheduling an interaction should rely on (as much as possible) local information only, namely the state of its participating components. However, as shown in this paper these information is not always sufficient and does not guarantee a safe execution of the system as it may introduce deadlocks. Moreover, delays may also affect the satisfaction of timing constraints, which also corresponds to deadlocks in the former model. Thus, we also explore methods for analyzing such deadlock situations and for computing  deadlock-free scheduling strategies when possible.
Cite as

Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, and Marius Bozga. Local Planning Semantics: A Semantics for Distributed Real-Time Systems. In LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1, pp. 01:1-01:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{dellabani_et_al:LITES-v006-i001-a001,
  author =	{Dellabani, Mahieddine and Combaz, Jacques and Bensalem, Saddek and Bozga, Marius},
  title =	{{Local Planning Semantics: A Semantics for Distributed Real-Time Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{01:1--01:27},
  ISSN =	{2199-2002},
  year =	{2019},
  volume =	{6},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v006-i001-a001},
  doi =		{10.4230/LITES-v006-i001-a001},
  annote =	{Keywords: Distributed Real-Time Systems, Timed Automata, Formal Verification}
}
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.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}
}
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