Publiée 12 juin 2026
DAE-based Contracts
Inria
Rennes, Hauts-de-France 60420, France
CDI
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):
Edot{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:
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
Avantages
Rémunération
Gratification
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):
Edot{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
- Strong mathematical reasoning and problem-solving skills.
- Familiarity with one or more of the following topics is an advantage: DAEs, contract theory, geometric control
- Scientific curiosity, autonomy, and the ability to work independently
Avantages
- Subsidized meals
- Partial reimbursement of public transport costs
- Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
Rémunération
Gratification
