DAE-based Contracts

Télécharger l'offre au format PDF
Le descriptif de l’offre ci-dessous est en Anglais

Type de contrat : Stage

Niveau de diplôme exigé : Bac + 3 ou équivalent

Fonction : Stagiaire de la recherche

A propos du centre ou de la direction fonctionnelle

The Inria Centre at Rennes University is one of Inria's eight centres and has more than thirty research teams. The Inria Centre is a major and recognized player in the field of digital sciences. It is at the heart of a rich R&D and innovation ecosystem: highly innovative PMEs, large industrial groups, competitiveness clusters, research and higher education players, laboratories of excellence, technological research institute, etc.

Contexte et atouts du poste

In the field of systems engineering, contract-based design [1] is a modular methodology that enables independent component development while ensuring correct system-wide integration. A specific instance is the assume--guarantee contract: Contract = (A, G). Here, Assumptions A describe what the component expects from its environment, while Guarantees G specify what the component promises to deliver, provided that the assumptions hold. Formally, a contract can be represented as an implication:

                                                                E ≼ A ⇒ (Σ ∧ E)≼ G

meaning that if the environment satisfies the assumptions A, the system under the environment must ensure the guarantees G. This contract-based perspective supports modular and compositional system design.

In recent years, the design and analysis of large-scale control systems 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:


                                                  Σ: \dot{x} = A x + B u, \\
                                                               y = C x + D u.

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.

[1] A. Benveniste, B. Caillaud, et all, Contracts for System Design. Foundations and Trends in Electronic Design Automation, Now Publishers, 2018.

[2] B. M. Shali, A. van der Schaft, and B. Besselink, “Composition of behavioural assume-guarantee contracts,” IEEE Transactions on Automatic Control, pp. 1–16, 2022.

[3] B. M. Shali, A. van der Schaft, and B. Besselink, “Design and control for implementation of
simulation-based assume-guarantee contracts,” IEEE Transactions on Automatic Control, pp. 1–15, 2025.

[4] Y. Chen, and W. Respondek. "Geometric analysis of differential-algebraic equations via linear control theory." SIAM Journal on Control and Optimization 59.1 (2021): 103-130.

[5] F. L. Lewis "A survey of linear singular systems." Circuits, systems and signal processing 5.1 (1986): 3-36.

Mission confiée

The goal of this internship is to extend contract theory to linear differential--algebraic equations (DAEs):

                            E\dot{z} = A z.

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:

  • System interconnections can be naturally expressed as algebraic equations, supporting a compositional framework.
  • DAEs treat all variables uniformly---states, inputs, and outputs---aligning well with the behavioral approach.
     
  • The geometric analysis of DAEs is well established [4] [5], providing effective tools for describing relations between systems and specifications.

Principales activités

• Conduct literature reviews on both contract theory and linear DAEs.

• Define notions from contract theory for DAE systems and develop theories on their verifications.

• Apply the proposed DAE-based contracts to simple examples.

• Participate actively in team meetings and brainstorming sessions.

Compétences

 

  • Scientific curiosity, autonomy, and the ability to work independently

Avantages

  • Restauration subventionnée
  • Possibilité de télétravail (après 6 mois d'ancienneté) et aménagement du temps de travail
  • Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
  • Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)

Rémunération

Gratification