Offre d'emploi
Centres Inria associés
Type de contrat
Contexte
<p style="text-align: justify;">In the field of systems engineering, <strong>contract-based design</strong> [1] is a modular methodology that enables independent component development while ensuring correct system-wide integration. A specific instance is the <em>assume--guarantee contract</em>: <em>Contract = (A, G)</em>. Here, <strong>Assumptions</strong> <em>A</em> describe what the component expects from its environment, while <strong>Guarantees</strong> <em>G</em> specify what the component promises to deliver, provided that the assumptions hold. Formally, a contract can be represented as an implication:</p>
<p><span class="base"><span class="mord mathnormal"> E </span><span class="mrel amsrm">≼ </span></span><span class="base"><span class="mord mathnormal">A </span><span class="mrel">⇒ (</span></span><span class="base"><span class="mord">Σ </span><span class="mbin">∧ </span></span><span class="base"><span class="mord mathnormal">E)</span><span class="mrel amsrm">≼ </span></span><span class="base"><span class="mord mathnormal">G</span></span></p>
<p style="text-align: justify;">meaning that if the environment satisfies the assumptions <em>A</em>, the system under the environment must ensure the guarantees <em>G</em>. This contract-based perspective supports <strong>modular and compositional</strong> system design.</p>
<p style="text-align: justify;">In recent years, the design and analysis of large-scale <strong>control systems</strong> have become increasingly challenging. To address this, contract-based design has been introduced into the control systems domain. Two notable studies [2,3] develop contract frameworks for linear time-invariant (LTI) control systems:</p>
<p style="text-align: justify;"><br /> Σ: \dot{x} = A x + B u, \\<br /> y = C x + D u.</p>
<p style="text-align: justify;">In [2], the classical behavioral theory introduced by Jan Willems is used to formalize key contract-theoretic notions such as assumptions, guarantees, refinement, and composition---for Σ. In [3], geometric control theory is employed to define simulation relations between two control systems, providing a foundation for implementing assume--guarantee contracts.A contract-based control design algorithm is then proposed based on these results.</p>
<p><span style="font-size: 10pt;">[1] A. Benveniste, B. Caillaud, et all, <em>Contracts for System Design</em>. Foundations and Trends in Electronic Design Automation, Now Publishers, 2018.</span></p>
<p><span style="font-size: 10pt;">[2] B. M. Shali, A. van der Schaft, and B. Besselink, “Composition of behavioural assume-guarantee contracts,” <em>IEEE Transactions on Automatic Control</em>, pp. 1–16, 2022.</span></p>
<p><span style="font-size: 10pt;">[3] B. M. Shali, A. van der Schaft, and B. Besselink, “Design and control for implementation of</span><br /><span style="font-size: 10pt;">simulation-based assume-guarantee contracts,” <em>IEEE Transactions on Automatic Control</em>, pp. 1–15, 2025.</span></p>
<p><span style="font-size: 10pt;">[4] Y. Chen, and W. Respondek. "Geometric analysis of differential-algebraic equations via linear control theory." <em>SIAM Journal on Control and Optimization</em> 59.1 (2021): 103-130.</span></p>
<p><span style="font-size: 10pt;">[5] F. L. Lewis "A survey of linear singular systems." <em>Circuits, systems and signal processing 5.1 (1986): 3-36</em>.</span></p>
<p><span class="base"><span class="mord mathnormal"> E </span><span class="mrel amsrm">≼ </span></span><span class="base"><span class="mord mathnormal">A </span><span class="mrel">⇒ (</span></span><span class="base"><span class="mord">Σ </span><span class="mbin">∧ </span></span><span class="base"><span class="mord mathnormal">E)</span><span class="mrel amsrm">≼ </span></span><span class="base"><span class="mord mathnormal">G</span></span></p>
<p style="text-align: justify;">meaning that if the environment satisfies the assumptions <em>A</em>, the system under the environment must ensure the guarantees <em>G</em>. This contract-based perspective supports <strong>modular and compositional</strong> system design.</p>
<p style="text-align: justify;">In recent years, the design and analysis of large-scale <strong>control systems</strong> have become increasingly challenging. To address this, contract-based design has been introduced into the control systems domain. Two notable studies [2,3] develop contract frameworks for linear time-invariant (LTI) control systems:</p>
<p style="text-align: justify;"><br /> Σ: \dot{x} = A x + B u, \\<br /> y = C x + D u.</p>
<p style="text-align: justify;">In [2], the classical behavioral theory introduced by Jan Willems is used to formalize key contract-theoretic notions such as assumptions, guarantees, refinement, and composition---for Σ. In [3], geometric control theory is employed to define simulation relations between two control systems, providing a foundation for implementing assume--guarantee contracts.A contract-based control design algorithm is then proposed based on these results.</p>
<p><span style="font-size: 10pt;">[1] A. Benveniste, B. Caillaud, et all, <em>Contracts for System Design</em>. Foundations and Trends in Electronic Design Automation, Now Publishers, 2018.</span></p>
<p><span style="font-size: 10pt;">[2] B. M. Shali, A. van der Schaft, and B. Besselink, “Composition of behavioural assume-guarantee contracts,” <em>IEEE Transactions on Automatic Control</em>, pp. 1–16, 2022.</span></p>
<p><span style="font-size: 10pt;">[3] B. M. Shali, A. van der Schaft, and B. Besselink, “Design and control for implementation of</span><br /><span style="font-size: 10pt;">simulation-based assume-guarantee contracts,” <em>IEEE Transactions on Automatic Control</em>, pp. 1–15, 2025.</span></p>
<p><span style="font-size: 10pt;">[4] Y. Chen, and W. Respondek. "Geometric analysis of differential-algebraic equations via linear control theory." <em>SIAM Journal on Control and Optimization</em> 59.1 (2021): 103-130.</span></p>
<p><span style="font-size: 10pt;">[5] F. L. Lewis "A survey of linear singular systems." <em>Circuits, systems and signal processing 5.1 (1986): 3-36</em>.</span></p>
Mission confié
<p>The goal of this internship is to extend contract theory to linear <strong>differential--algebraic equations (DAEs)</strong>:<br /><br /> E\dot{z} = A z.<br /><br />As a modular modeling approach derived from first-principle physics, DAEs frequently appear in constrained mechanical systems, power networks, and analog circuit design. Mathematically, DAEs offer several potential advantages for contract-based analysis:</p>
<ul>
<li style="text-align: justify;">System interconnections can be naturally expressed as algebraic equations, supporting a compositional framework.</li>
<li style="text-align: justify;">DAEs treat all variables uniformly---states, inputs, and outputs---aligning well with the behavioral approach.<br /> </li>
<li style="text-align: justify;">The geometric analysis of DAEs is well established [4] [5], providing effective tools for describing relations between systems and specifications.<br /><br /></li>
</ul>
<ul>
<li style="text-align: justify;">System interconnections can be naturally expressed as algebraic equations, supporting a compositional framework.</li>
<li style="text-align: justify;">DAEs treat all variables uniformly---states, inputs, and outputs---aligning well with the behavioral approach.<br /> </li>
<li style="text-align: justify;">The geometric analysis of DAEs is well established [4] [5], providing effective tools for describing relations between systems and specifications.<br /><br /></li>
</ul>
Principales activités
<p>• Conduct literature reviews on both contract theory and linear DAEs.</p>
<p>• Define notions from contract theory for DAE systems and develop theories on their verifications.</p>
<p>• Apply the proposed DAE-based contracts to simple examples.</p>
<p>• Participate actively in team meetings and brainstorming sessions.</p>
<p>• Define notions from contract theory for DAE systems and develop theories on their verifications.</p>
<p>• Apply the proposed DAE-based contracts to simple examples.</p>
<p>• Participate actively in team meetings and brainstorming sessions.</p>
Compétences
<p> </p>
<ul>
<li>Strong mathematical reasoning and problem-solving skills.<br /><br /></li>
<li>Familiarity with one or more of the following topics is an advantage: DAEs, contract theory, geometric control</li>
</ul>
<ul>
<li>Scientific curiosity, <strong>autonomy</strong>, and the ability to work independently</li>
</ul>
<ul>
<li>Strong mathematical reasoning and problem-solving skills.<br /><br /></li>
<li>Familiarity with one or more of the following topics is an advantage: DAEs, contract theory, geometric control</li>
</ul>
<ul>
<li>Scientific curiosity, <strong>autonomy</strong>, and the ability to work independently</li>
</ul>
Référence
2026-09706
Domaine d'activité