<figure><img src="image_29.png" /><figcaption>Figure 4.17: Bound effect lemma</figcaption></figure>

<figure><img src="image_30.png" /><figcaption>Figure 4.18: Coincidence lemma on alphabet d</figcaption></figure>

**Coincidence Lemma** The last lemma we need is the coincidence lemma on alphabet. The coincidence lemma used for the uniform substitution calculus [Pla17, lemma 12], expresses that if a transition $(s, f)$ satisfies $a$, then for every state $s'$ that is equal to the initial state $s$ on at least the free variables, there exists a state $f'$ such that $(s', f')$ satisfies $a$ and $f'$ is equal to $f$ on those variables. A free variable of a program is a variable that change the evaluation of the program. In our construction only the variables in the alphabet $d$ can change the behavior of a program. Which means that every free variable is in the alphabet, thus we can deduce the coincidence lemma on alphabet. The lemma4 is summarised on Figure 4.18

**Lemma 4 (Coincidence Lemma on alphabet).** For states $s, f$ and $s'$ such as $s \xrightarrow{a} f$ and $s'(d) = s(d)$ then

$$ \exists f', s' \xrightarrow{a} f' \wedge f'(d) = f(d) $$

**Theorem coincidence_program_on_d (P : Program) (p_in_d : prog_in_d P) (s s' f: KState) :**
$$ \begin{array}{l} (\text{map s dl} = \text{map s' dl}) \rightarrow \\ \text{dynamic Semantics program I P s f} \rightarrow \\ \text{exists f', dynamic Semantics program I P s' f' \wedge} \\ \text{map f dl} = \text{map f' dl.} \end{array} $$

### 4.4.4 Proof that Differential Refinement Implies Refinement

We now prove that the refinement defined from the refinement calculus implies the refinement from the contract theory. We give the mathematical proof, and the mechanized proof is available in the file DifferentialContracts.v of the library.
**Theorem refine_KFrefine**

(a b : Program) (a_in_d : prog_in_d a) (b_in_d : prog_in_d b) :
(∀ preS : KState, dynamic Semantics formula I (KFrefine a b) preS) →
to_component I a a_in_d ⊆ to_component I b b_in_d.

**Theorem 8 (Differential Refinement Implies Refinement).** For a and b two
hybrid programs with variables in d, if a ≲<sub>dL</sub> b then a ≲ b.

*Proof.* We consider two programs *a* and *b* such as *a* ≲<sub>*dL*</sub> *b*. We assume *d* ⊆ V the set of all variables used in *a* or *b*. Since the set is finite we can create a vector **d** = (*d*<sub>1</sub>, ..., *d*<sub>*n*</sub>) of all variables used in *a* or *b*. We assume *d'* ⊆ V a set of fresh variables with the same size as *d*. Similarly, we have **d'** = (*d*'<sub>1</sub>, ..., *d*'<sub>*n*</sub>) a vector of fresh variables.

We consider two states s, f : V → R, such as s $\xrightarrow{a}$ f. We will demonstrate
that s $\xrightarrow{b}$ f which, by definition of the refinement, will prove that a ≲ b.

We create a new state, $s'$, equal to $s$ on every variables except that $\forall i \in [1; n]$, $s'(d'_i) = f(d_i)$, namely:

$$
s'(\boldsymbol{d}') = f(\boldsymbol{d}) \tag{4.6}
$$

Since $s \xrightarrow{a} f$ and $s(\mathbf{d}) = s'(\mathbf{d})$, we can use the Coincidence Lemma 4. Which expresses that it exists a state $f'$ such as $s' \xrightarrow{a} f'$ and

$$
f(\mathbf{d}) = f'(\mathbf{d}). \tag{4.7}
$$

This is illustrated in Figure 4.19.

From the bound lemma 3, we can conclude that $\forall x \notin d$, $s'(x) = f'(x)$. On particular, since all variables in $d'$ are not in $d$, we have $\forall i \in [1; n]$, $f'(d'_i) = s'(d'_i) = f(d'_i)$. Which we can rewrite as:

$$
f(\boldsymbol{d}') = f'(\boldsymbol{d}') \tag{4.8}
$$

From equation 4.7 and 4.8, we have $f'(\boldsymbol{d}) = f'(\boldsymbol{d}')$. Since $s' \xrightarrow{a} f'$ and $f'(\boldsymbol{d}) = f'(\boldsymbol{d}')$, we can now use the differential refinement lemma 2. It states that their is a state $f''$ such that $s' \xrightarrow{b} f''$ and $f''(\boldsymbol{d}) = f''(\boldsymbol{d}')$. This is summarised in Figure 4.20.

Thanks to the Coincidence Lemma 4, we can conclude, from $s' \xrightarrow{b} f''$ and $s'(\mathbf{d}) = s(\mathbf{d})$ by definition of $s'$, that their is a state $f'''$ such as $s \xrightarrow{b} f'''$ and $f'''(\mathbf{d}) = f''(\mathbf{d})$. This is illustrated in Figure 4.21.

We will now prove that $\forall x \in V, f'''(x) = f(x)$. First if $x \notin d$, from the bound effect lemma 3, $f'''(x) = s(x)$ and (from the same lemma) $s(x) = f(x)$, hence $f'''(x) = f(x)$. Then, we prove that $f'''(\mathbf{d}) = f(\mathbf{d})$. From the coincidence lemma, we have $f'''(\mathbf{d}) = f''(\mathbf{d})$. We also have $f''(\mathbf{d}) = f''(\mathbf{d}')$ and from bound effect, $f''(\mathbf{d}') = s'(\mathbf{d}')$. And from Equation 4.6 $s'(\mathbf{d}) = f(\mathbf{d})$. So $f'''(\mathbf{d}) = f''(\mathbf{d}') = s'(\mathbf{d}') = f(\mathbf{d})$ which finishes the proof. □
<figure><img src="image_31.png" /><figcaption>Figure 4.19: Definition of $f'$ with coincidence lemma</figcaption></figure>

<figure><img src="image_32.png" /><figcaption>Figure 4.20: Definition of $f''$ with differential refinement lemma</figcaption></figure>

<figure><img src="image_33.png" /><figcaption>Figure 4.21: Definition of $f'''$ with coincidence lemma</figcaption></figure>
## 4.5 Abstract Programs

In this section, we introduce abstract programs, a subset of hybrid programs specifically designed to define contracts. So far, we expressed three requirements for the definition of abstract programs, they must be:

* closed by conjunction, disjunction and negation,

* writable as hybrid programs, and

* expressive enough to specify of systems.

We also want to instantiate the type class described in Section 3.7, which we do in Section 4.6. The instantiation will give us contracts that are sufficient to specify the examples of Section 4.2, and are compatible with the components defined in Section 4.3.

### 4.5.1 Definition

Abstract programs consist in the disjunctive normal form of atoms. Atoms are hybrid formulas which denote either a precondition or a postcondition. An `atom` is made of two parts, the `atom_` with the formula which can be either a precondition or a postcondition, and `atom_in_alphabet` which is the proof that the alphabet of the formula is `d`.

Inductive
`atom_ :=`
| preF : Formula → `atom_`
| postF : Formula → `atom_`.

Definition `atom_in_alphabet` (`d`: `alphabet`) (`e`: `atom_`) : `Prop` :=
match `e` with
| preF `f` ⇒ `formula_in_alphabet` `d` `f`
| postF `f` ⇒ `formula_in_alphabet` `d` `f`
end.

Definition `atom` (`d`: `alphabet`) := `{e | `atom_in_alphabet` `d` `e}`.

The type `aProgram` is an abstract program, coded as a list of list of atoms. The sublists of atoms encode the conjunction of the atoms, and the global list is the disjunction of all sublists. An example of abstract program is represented on Figure 4.22.

Definition `aProgram` (`d`: `alphabet`) :=
list (list (`atom` `d`)).

### 4.5.2 Satisfaction Function

The satisfaction function works inductively on the structure of the abstract programs. It returns a proposition determining if a behavior satisfies an abstract program.
<figure><img src="image_34.png" /><figcaption>Figure 4.22: The structure of abstract programs</figcaption></figure>

**Satisfaction of Atoms** The satisfaction of an atom depends on the nature of the atom. If it is a "Pre" atom, we check that the initial state of the behavior satisfies the formula in differential dynamic logic. If it's a "Post" atom, we check that the final state of the behavior satisfies the formula. The `proj1 Sig e` unwraps the `atom` and returns the `atom_` inside it.

**Definition** `aProgramSatAtom` (`d`: alphabet) (`t`: behavior `d`) (`e`: atom `d`) : `Prop` :=
`let` (prestate, poststate) := `to_transition` `t` in
`match` `proj1 Sig e` `with`
| `preF` `f` ⇒ `dynamic Semantics formula I` `f` `prestate`
| `postF` `f` ⇒ `dynamic Semantics formula I` `f` `poststate`
end.

**Satisfaction of Abstract Programs** The satisfaction of an abstract program is structural: the function `aProgramSat_aux` takes a list of atoms and holds if the behavior satisfies all the atoms; `aProgramSat` holds if one of the lists of atoms is satisfied by the behavior.

**Fixpoint** `aProgramSat_aux` (`d`: alphabet) (`t`: behavior `d`) (`sp_and`: list (atom `d`)) : `Prop` :=
`match` `sp_and` `with`
| `nil` ⇒ `True`
| `h :: q` ⇒ `aProgramSat_atom` `d` `t` `h` ∧ `aProgramSat_aux` `d` `t` `q`
end.

**Fixpoint** `aProgramSat` (`d`: alphabet) (`s`: behavior `d`) (`sp`: `aProgram` `d`) : `Prop` :=
`match` `sp` `with`
| `nil` ⇒ `False`
| `h :: t` ⇒ `aProgramSat_aux` `d` `s` `h` ∨ `aProgramSat` `d` `s` `t`
end.

### 4.5.3 Construction Operators

In this section we define the usual operators defined for expressions.
**Disjunction** The disjunction operator is made by appending two `aProgram` as seen on Figure 4.23

**Definition** `aProgram_or` (d : alphabet) (a b : aProgram d) : aProgram d :=
`a` `++` `b`.

<figure><img src="image_35.png" /><figcaption>Figure 4.23: The `V` operator.</figcaption></figure>

**Conjunction** The conjunction operator needs a little more work. We first need to define `aProgram_and_aux` which, for a list of atom and a program, returns the conjunction of the lists of atoms and the program. The idea is to recursively make the conjunction of an atom `a` and a list of disjunction `l = h :: t` with the equality: `a ∧ (h ∨ t) = (a ∧ h) ∨ (a ∧ t)`. Then, the "and" operator needs to call this function on all sub-lists of the program. We give an example in Figure 4.24.

<figure><img src="image_36.png" /><figcaption>Figure 4.24: The `∧` operator</figcaption></figure>

**Fixpoint** `aProgram_and_aux` (d : alphabet) (l : list (atom d)) (prog : aProgram d) : aProgram d :=
`match prog with`
| `nil` ⇒ `nil`
| `h :: t ⇒ (l ++ h) :: aProgram_and_aux d l t`
end.
**Fixpoint** aProgram_and (d : alphabet) (a b : aProgram d) : aProgram d :=
match a with
| nil ⇒ []
| h :: t ⇒ aProgram_or d (aProgram_and_aux d h b) (aProgram_and d t b)
end.

**Negation** To define the negation of an abstract program, we first define the negation of an element `aProgram_not`, as shown on Figure 4.25. We define the negation of list of atom with `aProgram_not_aux`. With De Morgan's Law, the negation of a conjunction of atoms is the disjunction of their negation. Then, we use again the De Morgan's law to compute the negation of the whole abstract program with `aProgram_not`. An example is given in Figure 4.26.

<figure><img src="image_37.png" /><figcaption>Figure 4.25: The negation operator of an atom</figcaption></figure>

**Definition** aProgram_not_atom (d : alphabet) (e : atom d) : atom d :=
match e with
| exist (preF f) pf ⇒ exist _ (preF (KFnot f)) (KFnot_in_d d f pf)
| exist (postF f) pf ⇒ exist _ (postF (KFnot f)) (KFnot_in_d d f pf)
end.

**Fixpoint** aProgram_not_aux (d : alphabet) (l : list (atom d)) : aProgram d :=
match l with
| nil ⇒ []
| h :: t ⇒ ((aProgram_not_atom d h):nil) :: (aProgram_not_aux d t)
end.

**Fixpoint** aProgram_not (d : alphabet) (sp : aProgram d) : aProgram d :=
match sp with
| nil ⇒ nil :: nil
| h :: t ⇒ aProgram_and d (aProgram_not_aux d h) (aProgram_not d t)
end.

### 4.5.4 Transforming to Hybrid Programs

In this section, we explain how to transform an abstract program into a hybrid program. This is done inductively on the structure of `aProgram`. More precisely, there is a function that transforms list of atoms into programs. Then, these programs are joined with the choice operator.

**Translating of an atom** The translation of the two kind of atoms is described in Figure 4.27.
<figure><img src="image_38.png" /><figcaption>Figure 4.26: The negation using de Morgan's rule</figcaption></figure>

$$ \boxed{\text{Pre } \phi} \longrightarrow (\neg \phi ; d = * ; ?\top) $$

$$ \boxed{\text{Post } \psi} \longrightarrow (\neg\top ; d = * ; ?\psi) $$

<caption>Figure 4.27: Transforming an abstract atom into an hybrid program</caption>

**Undeterminate Assignation of Alphabet** We use $d = *$ which stands for the indeterminate assignment of all variables in alphabet $d$. This implies that the alphabet $d$ must be finite, we use the same axioms as in Section 4.4. To define this operator **AssignAny**, we define **assignAny_aux** which iterate over the identifiers of the alphabet and compose hybrid programs that assign any value to them.

Fixpoint assignAny_aux (l : list ident) : Program ::= match l with | nil ⇒ KPtest KFtrue | h :: t ⇒ KPcompose (KPassignAny h) (assignAny_aux t) end.

Definition assignAny (d : alphabet) (fd : Finite d) : Program ::= assignAny_aux (elements_of d fd).

**Aggregation of List of Atoms** To transform a list of atoms into an hybrid programs, we aggregate the atoms that are precondition and the atoms that are postconditions with `flatten_pre` and `flatten_post`. Then the function `to_program_aux` creates the program with the sequence of the precondititon, **assignAny d** and the postcondition. We give an example of the process in Figure `fg-list-hp`.
**Fixpoint** `flatten_pre` (d : alphabet) (l : list (atom d)) : Formula ::= match l with
| nil ⇒ KFtrue
| exist (preF f) _ :: t ⇒ KFand f (flatten_pre d t)
| exist (postF _ ) _ :: t ⇒ flatten_pre d t
end.

**Fixpoint** `flatten_post` (d : alphabet) (l : list (atom d)) : Formula ::= match l with
| nil ⇒ KFtrue
| exist (preF _ ) _ :: t ⇒ flatten_post d t
| exist (postF f) _ :: t ⇒ KFand f (flatten_post d t)
end.

**Definition** `to_program_aux` (d : alphabet) (fd : Finite d) (s : list (atom d)) : Program ::= KPcompose
(KPcompose
(KPtest (flatten_pre d s))
(assignAny d fd))
(KPtest (flatten_post d s))

<figure><img src="image_39.png" /></figure>

<figure><img src="image_40.png" /></figure>

<figure><img src="image_41.png" /><figcaption>Figure 4.28: Transforming a list of abstract atom into an hybrid program</figcaption></figure>

**Transforming an Abstract Program** To transform an abstract program to an hybrid program, we first transform each sublists to hybrid programs with `to_program_aux`. Then we join each program with the choice operator of differential dynamic logic with `to_program` as shown on Figure 4.29.
Fixpoint to_program (d : alphabet) (fd : Finite d) (s : aProgram d) : Program ::= match s with | nil ⇒ KPtest KFfalse | h :: t ⇒ KPchoice (to_program_aux d fd h) (to_program d fd t) end.

<figure><img src="image_42.png" /><figcaption>Figure 4.29: Transforming an abstract program into a hybrid program</figcaption></figure>

### 4.5.5 Proving the Transformation is Sound

We want to prove that `to_program` is correctly defined, to do that we prove that a behavior `t` satisfying an abstract program `sp aProgram.sat d t sp` also satisfies the translation of the abstract program `to_program d fd sp`.

**Proof of Correctness** We want to prove that the translation function is correct. The proof is done by induction on the abstract program. First we prove that `to_program_aux` is sound, then with induction we will prove `to_program` is sound. We need to prove that every behavior on `d` satisfy `assignAny d`. This is done by induction on the list of identifiers in the alphabet `d`.
**Theorem sat_to_program :**
∀ (d : alphabet) (fd : Finite d) (sp : aProgram d) (t : behavior d),
let (preS, postS) := to_transition t in
dynamic Semantics program I (to_program d fd sp) preS postS ↔ aProgram sat d t sp.

**Lemma sat_to_program S O U N D A X :**
∀ (d : alphabet) (fd : Finite d) (a : list (atom d)) (t : behavior d),
let (preS, postS) := to_transition t in
dynamic Semantics program I (to_program_aux d fd a) preS postS ↔
aProgram sat_aux d t a.

**Lemma assignAny_dsp :** ∀ (d : alphabet) (fd : Finite d) (t : behavior d),
let (preS, postS) := to_transition t in
dynamic Semantics program I (assignAny d fd) preS postS.

## 4.6 Contracts with Differential Dynamic Logic

This section instantiates the assumption/guarantee theory of contracts with abstract programs. We are going to instantiate the theory using the interface we defined in Section 3.7. Then, we focus on defining contracts using abstract programs. We show how to transform an implementation property into a hybrid formula to prove in $dL$. Finally we use the composition given by the instantiation to create a contract for the system, and use the contract as a validation of an hybrid program modeling the system.

### 4.6.1 Instantiating the Theory of Contract

**Using the Interface** We use the interface defined in Section 3.7, it is particularly fit for this purpose because abstract programs are alphabetized expressions. To be able to use hybrid programs and abstract programs in conjunction, we use the same types for the definition of behaviors, namely KAssignable for ident and (R * R) for value. The instantiation needs an expression type, operators, proof of correctness of operators and decidability of satisfaction function. The operators "and", "or", and "not" and the satisfaction function were developed in Section 4.5. We still need to prove their correctness and the decidability of the satisfaction function.

**Proof Operators are Correct** We prove that each operator respect its specification. For each operator, the proof is done by induction on sp1 and poses no real challenge.

**Lemma aProgram_or_correct :** $\forall$ (d : alphabet) (s : behavior d) (sp1 sp2 : aProgram d),
aProgram\_sat d s sp1 $\lor$ aProgram\_sat d s sp2 $\leftrightarrow$ aProgram\_sat d s (aProgram\_or d sp1 sp2).

**Lemma aProgram_and_correct :** $\forall$ (d : alphabet) (s : behavior d) (sp1 sp2 : aProgram d),
aProgram\_sat d s sp1 $\land$ aProgram\_sat d s sp2 $\leftrightarrow$ aProgram\_sat d s (aProgram\_and d sp1 sp2).
**Lemma** `aProgram_not correct`: **forall** (d : alphabet) (s : behavior d) (sp : aProgram d),
¬ aProgram.sat d s sp ↔ aProgram.sat d s (aProgram_not d sp).

**Decidability** We axiomatize the decidability of the satisfaction function, since proving it is outside of our scope of work.

**Axiom** `aProgram.sat_dec`: **forall** (d : alphabet) (s : behavior d) (sp : aProgram d),
`aProgram.sat d s sp` ∨ ¬`aProgram.sat d s sp`.

Now, we are ready to instantiate the type class `AlphabetizedExpression`

**Instance** `abstract_program`: `AlphabetizedExpression` `(R*R)` `KAssignable` `aProgram` := {
  `e_and` := `aProgram_and`;
  `e_or` := `aProgram_or`;
  `e_not` := `aProgram_not`;
  `sat` := `aProgram.sat`;
  `sat_e_not` := `aProgram_not_correct`;
  `sat_e_or` := `aProgram_or correct`;
  `sat_e_and` := `aProgram_and_correct`;
  `sat_dec` := `aProgram.sat_dec`;
}.

**Results** This instantiation gives us operators to define contracts. The function `contractF` constructs a contract given two abstract programs. The function `saturateF` computes the saturated version of a contract. The function `composeF` computes the composition of two contracts. For the example we define `aSaturate` and `aCompose`, to facilitate the use of the operators.

**Definition** `aSaturate` := `@saturateF _ _ _` (abstract_program I) d.

**Definition** `aCompose` := `@composeF _ _ _` (abstract_program I) d.

## 4.6.2 Example of Contracts

**Contract for the valve** The valve has no assumption, so we say its assumption holds for any behavior. We define `aTrue` as an abstract program that holds for any behavior. The guarantee has one atom with formula $h \ge H_{limit} \rightarrow v = 0$, which we reproduce in `atom_1_f`. After having proved that this formula's alphabet is in `d`, we create the guarantee. The contract is described in Figure 4.30.

**Definition** `caassume` := `aTrue d`.

**Definition** `atom_1_f`: `atom_` := `postF ((KFimply
(KFgreaterEqual (KTread h) HLimit)
(KFequal v (KTnumber (KTnreal 0))))).`
**Lemma** `atom_1_in_d`: `atom_in_alphabet d atom_1_f`. **Proof.** firstorder. **Qed.**

**Definition** `atom_1` := `exist _ atom_1_f atom_1_in_d`.

**Definition** `ca_guarantee`: `aProgram d := [[ atom_1 ]].`

**Definition** `ca_contract`: `contractF d := ContractF d caassume ca_guarantee.`
<figure><img src="image_43.png" /><figcaption>Figure 4.30: The contract of the valve $\alpha$</figcaption></figure>

**Contract of the Water Tank** We create the contract for the water tank. The tank assumes that the level of water $h$ starts below $H_{max}$ which we encode in `atom_2`. The assumption is the conjunction of `atom_2` and `atom_1` the guarantee of the valve. The water tank guarantee it doesn't overflow, we write this assertion as `atom_3`. We give Figure 4.31 a visual representation of the contract.

**Definition** `atom_2_f` := preF (KFlessEqual h HMax).

**Lemma** `atom_2_in_d` : `atom_in_alphabet d atom_2_f`.

**Proof.** firstorder. **Qed.**

**Definition** `atom_2` := exist _ `atom_2_f atom_2_in_d`.

**Definition** `cbassume` : `aProgram d` := [[ `atom_2` ; `atom_1` ]].

**Definition** `atom_3_f` := postF (KFlessEqual h HMax).

**Lemma** `atom_3_in_d` : `atom_in_alphabet d atom_3_f`.

**Proof.** firstorder. **Qed.**

**Definition** `atom_3` := exist _ `atom_3_f atom_3_in_d`.

**Definition** `cbguarantee` : `aProgram d` := [[ `atom_3` ]].

**Definition** `cb_contract` := `ContractF d cbassume cbguarantee`.

### 4.6.3 Implementation of a Contract by a Component

Thanks to the previous definitions, we can express the implementation of a contract by a component as a $d\mathcal{L}$ property. Indeed the assumption/guarantee theory of contract we can show that for a saturated contract $c = (A, G)$ and a component $\sigma$

$$ \sigma \vdash c \equiv \sigma \preceq G \qquad (4.9) $$

With the help the relation we proved in Section 4.4, we can express the refinement as a differential refinement which is provable as a property of differential dynamic logic. We also need to use the translations from abstract programs to
<figure><img src="image_44.png" /><figcaption>Figure 4.31: The contract of the water tank</figcaption></figure>

hybrid programs to transform the contract's guarantee into an hybrid program. This is proved in **Theorem proof_trans**.

**Theorem proof_trans** (d : alphabet) (fd : Finite d) 
(a : Program) (a_in_d : prog_in_d d a) (c : contractF d) : 
(forall preS : KState, 
(dynamic Semantics formula I 
(KRefine d fd a (to_program d fd (G d (saturateF d c)))) preS)) 
-> 
Implements d (to_component I a a_in_d) (contract_of d c).

**Example** Here we show how we would discharge the proof that the hybrid program modeling the valve is an implementation of the contract to a differential dynamic logic formula with proof_trans.

**Theorem ca_Implements_alpha:**
(forall preS, dynamic Semantics formula I
(KRefine d d finite alpha
(to_program d d finite (G d (aSaturate ca_abSTRACT_contract))))
preS)
-> Implements d alpha_component (to_contract ca_abSTRACT_contract).

**Proof.**

apply (proof_trans I d fd).

Qed.

4.6.4 Composition of Contracts

Thanks to the instantiation of the theory of assumption/guarantee contracts, the composition of contracts made with abstract program is already defined.

**Example** We build the contract for the system by composition of the contract of the valve and the water tank. Since the guarantee of the valve is the same as the assumption of the water tank, the assumption of the system reduce to a more simple abstract program. The mechanism of reduction is not automatised in our formalisation but we can prove this result by hand. We show in Figure 4.32 a representation of the contract.
<figure><img src="image_45.png" /><figcaption>Figure 4.32: The (reduced) contract of the system</figcaption></figure>

**Definition** `cg_contract`: `contractF d :=`
`aCompose ca_abSTRACT_contract cb_contract.`

**Lemma** `cg_contract_reduction`:
`aSaturate cg_contract =`
`aSaturate (ContractF d [[atom_2]] [[atom_1; atom_3]]).`

**System's Hybrid Program** The hybrid program modeling the system was written by hand. It is not the result of an operation between $\alpha$ and $\beta$. Because, to the best of our knowledge, the parallel composition of hybrid programs is not defined in differential dynamic logic. The proof obligation is now to verify that $\gamma$ implements the contract `cg_contract`. With `proof_trans`, we can discharge this proof into differential dynamic logic. This makes it possible to validate the component $\gamma$ as the correct composition of the valve and the water-tank.

$$ \gamma = ((\dot{h} = v \& h < H_{limit}) ; (?h < H_{limit} \lor v := 0))^* \quad (4.10) $$

**Definition** `gamma :=`
KPloop
(KPcompose
(KPchoice
(KPtest (KFlessEqual (KTread h) HMax))
(KPassign v (KTnumber (KTReal 0%R))))
)
(KPodeSystem
(ODEAtomic (ODEsing (KAssignDiff h) (KTread v)))
(KFless h HMax)
)
).
**Theorem gamma_implments_cg:**
(forall preS : KState,
  dynamic_semlotics_formula I
  (KFrefine d fd gamma (to_program d fd (G d (aSaturate cg_contract)))))
  preS)
$\rightarrow$
implies d gamma_component (to_contract cg_contract).

**Proof.**
apply (proof_trans I d fd).

Qed.

## 4.7 Conclusion

In this chapter, we showed two different instantiation of the assumption/guarantee theory of contracts. The first instantiation used the generic interface, simply by implementing the type class. The instantiation of the verified contract theory gives a natural definition of the refinement relation. Yet, a refinement relation was already defined for hybrid programs [LP16]. We proved that this refinement implies the refinement defined in the assume/guarantee contracts, which allow us to prove refinement relations by proving hybrid formulas using specialized tools such as Keymaera X. To define contracts in differential dynamic logic, we introduced abstract programs. We gave the algorithms to construct and manipulate abstract programs, and the function to decide the satisfaction of an abstract programs by behaviors. We also gave the translation function from abstract programs to hybrid programs. Finally, we proved this function to be correct, meaning a behavior satisfying the abstract programs also satisfies the translated hybrid programs and vice versa. Next, we showed how both instances work together. Specifically, we defined the implementation relation of a contract by a component. The contract being written with abstract programs, and the component being written with hybrid programs. We also gave the water tank system as an example of an use case for components and contracts. This example demonstrates the usefulness of modularity and abstraction in the process of verifying systems. The water tank system being a cyber-physical system, the example uses all the potentials of differential dynamic logic to model ordinary differential equation. This example showed how the mechanization of assumption/guarantee contracts can be useful to define contracts with different logics. The aim of this mechanization is to be a common base of definition of contracts. Since different logic have different features, their natives definition of components and contract are different. The Verified Contract Theory shows we can link theses definitions together.
<figure><img src="image_46.png" /></figure>
# Chapter 5

# Conclusion

## 5.1 Overview

We presented a formalization of the set-theoretical assumption/guarantee contracts in the proof assistant Coq. To the best of our knowledge, it is the first mechanized formalization of a theory of assumption/guarantee contracts for system design. The formalization gives us the assurance that the notion of assumption/guarantee contract is a correct instance of the meta-theory of contract. We also formalized the mechanism to extend the alphabet on which a contract is defined, as well as the abstraction of a contract by eliminating one its variable. Both mechanisms are validated regarding the meta-theory of contract. Finally, we introduce an interface made to facilitate to instantiation of the theory.

In the second part of our thesis, we instantiated the theory with differential dynamic logic. It is a practical demonstration of the use of the parametric assumption/guarantee contract theory. Firstly, we instantiated the theory to construct components from hybrid programs. We exhibit the relation between the refinement of hybrid program and the refinement of component define in the assumption/guarantee theory of contract. Secondly, we defined abstract programs, to instantiate the theory of contract with them. Abstract programs are a restriction of hybrid programs, though they are closed by conjunction and negation, thus we also gave the translation function from abstract programs to hybrid program. The instantiation of the theory of contract with abstract programs gave us contract defined with abstract programs as assumptions and guarantee. The contracts came with the operators defined in the theory, namely, conjunction, refinement and composition. The implementation of a contract component by a contract is also defined between the components defined as hybrid programs and the contracts defined with abstract programs. Finally, we introduced an example to apply all the definitions above, it gives a practical usage of the theory of contract to specify a system.
## 5.2 Perspectives

One of our interest would be to exhibit the links between the works done to define contracts and components for differential dynamic logic. Lunel defines components for differential dynamic logic with a particular form [Lun+19] whereby components are considered as the sequences of discrete computations followed by a continuous behaviour. This fixed form allows to define a commutative and associative composition operator. The operator is only defined if its arguments validate specific timing requirements. The operator defines the sequence of the discrete computations and the parallelization of the continuous behaviour. It would be interesting to formally establish the relation between this operator and the operator naturally defined from our instantiation mechanism.

Müller et al. define components and contracts for differential dynamic logic [Mül+18] in a similar manner as Lunel, yet without explicit timing constraints. Their model uses ports to manage inputs and outputs of the contracts, and their contracts are specifically made to specify those ports. Müller et al. also define different kinds of contracts to specify specific aspects of a component. The different contracts may be defined as different instances of the theory of contracts.

Another approach would be to instantiate the verified contract theory with another logic, for example duration calculus and hybrid Hoare logic [Liu+10; HC97] It is expressive enough to capture cyber-physical systems, and already has a formalisation in Isabelle [Che+17]. The formalisation in Coq has been investigated already, without complete success to date [CPM03]. Contracts have been defined for hybrid Hoare logic [WZG12], we are interested in the relation between the contracts defined by Wang and the contract that are defined from the contract theory.

We could also augment the mechanization, for example recent work have defined a quotient for the assumption/guarantee contract [Ínc+18]. The quotient is an important part of the meta theory of contract as it permits to exhibit the necessary contracts needed for a system to function. Yet, the quotient has no trivial definition, it is thus missing from our mechanization, we should add the definition of Incer to our formalization.

Nuzzo made some very interesting developments to the assumption/guarantee contracts [Nuz15]. In particular the heterogeneous refinement of contracts seems quite fitted to our mechanization. We could implement it to define refinement of contract from different instances of the theory.

We believe extending the work of our mechanization can help the community understanding the theory of contracts and creating better processes for the specification and validation of systems.
Bibliography

[Abr10] Jean-Raymond Abrial. *Modeling in Event-B: System and Software Engineering*. Cambridge University Press, May 13, 2010. 613 pp.
ISBN: 978-1-139-64397-9. Google Books: 23UgAwAAQBAJ.

[AK15] Abhishek Anand and Ross Knepper. "ROSCoq: Robots Powered by Constructive Reals". In: *Interactive Theorem Proving*. Ed. by Christian Urban and Xingyuan Zhang. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2015, pp. 34–50.
ISBN: 978-3-319-22102-1. DOI: 10.1007/978-3-319-22102-1_3.

[AL93] Martín Abadi and Leslie Lamport. "Composing Specifications". In: *ACM Transactions on Programming Languages and Systems* 15.1 (Jan. 1, 1993), pp. 73–132. ISSN: 0164-0925. DOI: 10.1145/151646.151649. URL: https://doi.org/10.1145/151646.151649 (visited on 03/17/2021).

[AL95] Martín Abadi and Leslie Lamport. "Conjoining Specifications". In: *ACM Transactions on Programming Languages and Systems* 17.3 (May 1995), pp. 507–535. ISSN: 0164-0925, 1558-4593. DOI: 10.1145/203095.201069. URL: https://dl.acm.org/doi/10.1145/203095.201069 (visited on 03/17/2021).

[Alu+93] Rajeev Alur et al. "Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems". In: *Hybrid Systems*. Ed. by Robert L. Grossman et al. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1993, pp. 209–229.
ISBN: 978-3-540-48060-0. DOI: 10.1007/3-540-57318-6_30.

[Bau+12] Sebastian S. Bauer et al. "Moving from Specifications to Contracts in Component-Based Design". In: *Fundamental Approaches to Software Engineering*. Ed. by Juan de Lara and Andrea Zisman. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2012, pp. 43–58. ISBN: 978-3-642-28872-2. DOI: 10.1007/978-3-642-28872-2_3.

[BC13] Yves Bertot and Pierre Castéran. *Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions*. Springer Science & Business Media, Mar. 14, 2013. 492 pp. ISBN: 978-3-662-07964-5. Google Books: Fek1BQAAQBAJ.
[Beh+99] Patrick Behm et al. "Météor: A Successful Application of B in a Large Project". In: *FM'99 — Formal Methods*. Ed. by Jeannette M. Wing, Jim Woodcock, and Jim Davies. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1999, pp. 369–387. ISBN: 978-3-540-48119-5. DOI: 10.1007/3-540-48119-2_22.

[Ben+08] Albert Benveniste et al. "Multiple Viewpoint Contract-Based Specification and Design". In: *Formal Methods for Components and Objects*. Ed. by Frank S. de Boer et al. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2008, pp. 200–225. ISBN: 978-3-540-92188-2. DOI: 10.1007/978-3-540-92188-2_9.

[Ben+15a] Albert Benveniste et al. *Contracts for Systems Design: Methodology and Application Cases*. report. July 2015. URL: https://hal.inria.fr/hal-01178469 (visited on 12/02/2019).

[Ben+15b] Albert Benveniste et al. *Contracts for Systems Design: Theory*. report. INRIA, July 2015. URL: https://hal.inria.fr/hal-01178467 (visited on 11/29/2019).

[BLM15] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. "Coquelicot: A User-Friendly Library of Real Analysis for Coq". In: *Mathematics in Computer Science* 9.1 (Mar. 1, 2015), pp. 41–62. ISSN: 1661-8289. DOI: 10.1007/s11786-014-0181-1. URL: https://doi.org/10.1007/s11786-014-0181-1 (visited on 03/03/2023).

[BNH14] Albert Benveniste, Dejan Nickovic, and Thomas Henzinger. *positional Contract Abstraction for System Design*. report. Jan. 29, 2014. URL: https://hal.inria.fr/hal-00938854 (visited on 10/29/2019).

[Boh+17] Brandon Bohrer et al. "Formally Verified Differential Dynamic Logic". In: *Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs* (Paris, France). CPP 2017. New York, NY, USA: ACM, 2017, pp. 208–221. ISBN: 978-1-4503-4705-1. DOI: 10.1145/3018610.3018616. URL: http://doi.acm.org/10.1145/3018610.3018616 (visited on 12/02/2019).

[Che+17] Mingshuai Chen et al. "MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems". In: *Provably Correct Systems*. Ed. by Mike Hinchey, Jonathan P. Bowen, and Ernst-Rüdiger Olderog. NASA Monographs in Systems and Software Engineering. Cham: Springer International Publishing, 2017, pp. 39–58. ISBN: 978-3-319-48628-4. URL: https://doi.org/10.1007/978-3-319-48628-4_3 (visited on 01/13/2020).

[CHR91] Zhou Chaochen, C. A. R. Hoare, and Anders P. Ravn. "A Calculus of Durations". In: *Information Processing Letters* 40.5 (Dec. 13, 1991), pp. 269–276. ISSN: 0020-0190. DOI: 10.1016/0020-0190(91)90122-X. URL: http://www.sciencedirect.com/science/article/pii/002001909190122X (visited on 12/23/2019).
[CJR96] Zhou Chaochen, Wang Ji, and Anders P. Ravn. "A Formal Description of Hybrid Systems". In: *Hybrid Systems III*. Ed. by Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1996, pp. 511-530. ISBN: 978-3-540-68334-6. DOI: 10.1007/BFb0020972.

[CM20] Zheng Cheng and Dominique Méry. *A Refinement Strategy for Hybrid System Design with Safety Constraints*. Research Report. Université de Lorraine ; INRIA ; CNRS, July 2020. URL: https://hal.inria.fr/hal-02895528.

[Cou+12] Denis Cousineau et al. "TLA + Proofs". In: *FM 2012: Formal Methods*. Ed. by Dimitra Giannakopoulou and Dominique Méry. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2012, pp. 147-154. ISBN: 978-3-642-32759-9. DOI: 10.1007/978-3-642-32759-9_14.

[CPM03] Samuel Colin, Vincent Poirriez, and Georges Mariano. "Thoughts about the Implementation of the Duration Calculus with Coq". In: *Fourth Workshop on the Implementation of Logics*. 2003, p. 33.

[dMB08] Leonardo de Moura and Nikolaj Bjørner. "Z3: An Efficient SMT Solver". In: *Tools and Algorithms for the Construction and Analysis of Systems*. Ed. by C. R. Ramakrishnan and Jakob Rehof. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2008, pp. 337-340. ISBN: 978-3-540-78800-3. DOI: 10.1007/978-3-540-78800-3_24.

[Dup+18] Guillaume Dupont et al. "Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B". In: *Abstract State Machines, Alloy, B, TLA, VDM, and Z*. Ed. by Michael Butler et al. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2018, pp. 155-170. ISBN: 978-3-319-91271-4. DOI: 10.1007/978-3-319-91271-4_11.

[FGH06] Peter H. Feiler, David P. Gluch, and John J. Hudak. *The Architecture Analysis & Design Language (AADL): An Introduction*. Carnegie-Mellon Univ Pittsburgh PA Software Engineering Inst, 2006.

[FMS14] Sanford Friedenthal, Alan Moore, and Rick Steiner. *A Practical Guide to SysML: The Systems Modeling Language*. Morgan Kaufmann, Oct. 23, 2014. 631 pp. ISBN: 978-0-12-800800-3. Google Books: Ze60AwAAQBAJ.

[Fos+20] Simon Foster et al. "Unifying Theories of Reactive Design Contracts". In: *Theoretical Computer Science* 802 (Jan. 8, 2020), pp. 105-140. ISSN: 0304-3975. DOI: 10.1016/j.tcs.2019.09.017. arXiv: 1712.10233. URL: https://www.sciencedirect.com/science/article/pii/S0304397519305614 (visited on 07/02/2021).
[Fre10] Patrick Christopher Frey. "A timing model for real-time control-systems and its application on simulation and monitoring of AUTOSAR systems". PhD thesis. University of Ulm, 2010. URL: http://vts.uni-ulm.de/docs/2011/7505/vts%5C_7505%5C_10701.pdf.

[Ful+15] Nathan Fulton et al. "KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems". In: Automated Deduction - CADE-25. Ed. by Amy P. Felty and Aart Middeldorp. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2015, pp. 527-538. ISBN: 978-3-319-21401-6. DOI: 10.1007/978-3-319-21401-6_36.

[FW17] Simon Foster and Jim Woodcock. "Towards Verification of Cyber-Physical Systems with UTP and Isabelle/HOL". In: Concurrency, Security, and Puzzles: Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday. Ed. by Thomas Gibson-Robinson, Philippa Hopcroft, and Ranko Lazić. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2017, pp. 39-64. ISBN: 978-3-319-51046-0. DOI: 10.1007/978-3-319-51046-0_3. URL: https://doi.org/10.1007/978-3-319-51046-0_3 (visited on 03/30/2020).

[FZW15] Simon Foster, Frank Zeyda, and Jim Woodcock. "Isabelle/UTP: A Mechanised Theory Engineering Framework". In: Unifying Theories of Programming. Ed. by David Naumann. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2015, pp. 21-41. ISBN: 978-3-319-14806-9. DOI: 10.1007/978-3-319-14806-9_2.

[GLB87] Thierry Gautier, Paul Le Guernic, and Loïc Besnard. "SIGNAL: A Declarative Language for Synchronous Programming of Real-Time Systems". In: Functional Programming Languages and Computer Architecture. Ed. by Gilles Kahn. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1987, pp. 257-277. ISBN: 978-3-540-47879-9. DOI: 10.1007/3-540-18317-5_15.

[Gra+18] Susanne Graf et al. "Building Correct Cyber-Physical Systems: Why We Need a Multiview Contract Theory". In: Formal Methods for Industrial Critical Systems. Ed. by Falk Howar and Jiří Barnat. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2018, pp. 19-31. ISBN: 978-3-030-00244-2. DOI: 10.1007/978-3-030-00244-2_2.

[Hal+91] N. Halbwachs et al. "The Synchronous Data Flow Programming Language LUSTRE". In: Proceedings of the IEEE 79.9 (Sept. 1991), pp. 1305-1320. ISSN: 0018-9219, 1558-2256. DOI: 10.1109/5.97300.
[HC97] Michael R. Hansen and Zhou Chaochen. "Duration Calculus: Logical Foundations". In: *Formal Aspects of Computing* 9.3 (May 1, 1997), pp. 283–330. ISSN: 1433-299X. DOI: 10.1007/BF01211086. URL: https://doi.org/10.1007/BF01211086 (visited on 10/13/2020).

[Hen00] Thomas A. Henzinger. "The Theory of Hybrid Automata". In: *Verification of Digital and Hybrid Systems*. Ed. by M. Kemal Inan and Robert P. Kurshan. NATO ASI Series. Berlin, Heidelberg: Springer, 2000, pp. 265–292. ISBN: 978-3-642-59615-5. DOI: 10.1007/978-3-642-59615-5_13. URL: https://doi.org/10.1007/978-3-642-59615-5_13 (visited on 12/02/2019).

[HJ98] Charles Antony Richard Hoare and He Jifeng. *Unifying Theories of Programming*. Vol. 14. Prentice Hall Englewood Cliffs, 1998.

[HP22] Jérôme Hugues and Sam Procter. "Contracts in System Development: From Multiconcern Analysis to Assurance With the Architecture Analysis and Design Language". In: *IEEE Software* 39.4 (July 2022), pp. 34–38. ISSN: 1937-4194. DOI: 10.1109/MS.2022.3167533.

[Hug+22] Jérôme Hugues et al. "Mechanization of a Large DSML: An Experiment with AADL and Coq". In: *2022 20th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)*. 2022 20th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). Oct. 2022, pp. 1–9. DOI: 10.1109/MEMOCODE.57689.2022.9954589.

[Ínc+18] Íñigo Íncer Romeo et al. "Quotient for Assume-Guarantee Contracts". In: *2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)*. 2018 16th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). Oct. 2018, pp. 1–11. DOI: 10.1109/MEMCOD.2018.8556872.

[Inc+22] Inigo Íncer et al. "Hypercontracts". In: *NASA Formal Methods*. Ed. by Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2022, pp. 674–692. ISBN: 978-3-031-06773-0. DOI: 10.1007/978-3-031-06773-0_36.

[Lam93] Leslie Lamport. "Hybrid Systems in TLA+". In: *Hybrid Systems*. Ed. by Robert L. Grossman et al. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 1993, pp. 77–102. ISBN: 978-3-540-48060-0. DOI: 10.1007/3-540-57318-6_25.

[LBT17] Simon Lunel, Benoît Boyer, and Jean-Pierre Talpin. "Compositional Proofs in Differential Dynamic Logic dL". In: *2017 17th International Conference on Application of Concurrency to System Design (ACSD)*. 2017 17th International Conference on Application of Concurrency to System Design (ACSD). June 2017, pp. 19–28. DOI: 10.1109/ACSD.2017.16.
[Liu+10] Jiang Liu et al. "A Calculus for Hybrid CSP". In: *Programming Languages and Systems*. Ed. by Kazunori Ueda. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2010, pp. 1-15. ISBN: 978-3-642-17164-2. DOI: 10.1007/978-3-642-17164-2_1.

[LP16] Sarah M. Loos and André Platzer. "Differential Refinement Logic". In: *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science*. LICS '16. New York, NY, USA: Association for Computing Machinery, July 5, 2016, pp. 505-514. ISBN: 978-1-4503-4391-6. DOI: 10.1145/2933575.2934555. URL: https://doi.org/10.1145/2933575.2934555 (visited on 10/12/2020).

[Lun+19] Simon Lunel et al. "Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic". In: *Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings*. Ed. by Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira. Vol. 11800. Lecture Notes in Computer Science. Springer, 2019, pp. 354-370. ISBN: 978-3-030-30941-1. DOI: 10.1007/978-3-030-30942-8_22.

[Lun19] Simon Lunel. "Parallelism and Modular Proof in Differential Dynamic Logic." PhD thesis. University of Rennes 1, France, 2019. URL: https://tel.archives-ouvertes.fr/tel-02102687.

[Mal+16] G. Malecha et al. "Towards Foundational Verification of Cyber-Physical Systems". In: *2016 Science of Security for Cyber-Physical Systems Workshop (SOSCYPS)*. 2016 Science of Security for Cyber-Physical Systems Workshop (SOSCYPS). Apr. 2016, pp. 1-5. DOI: 10.1109/SOSCYPS.2016.7580000.

[MAL22] Amel Mammar, Meryem Afendi, and Régine Laleau. "Modeling and proving hybrid programs with Event-B: An approach by generalization and instantiation". In: *Science of Computer Programming* 222 (2022), p. 102856. ISSN: 0167-6423. DOI: https://doi.org/10.1016/j.scico.2022.102856. URL: https://www.sciencedirect.com/science/article/pii/S0167642322000892.

[MEO98] Sven Erik Mattsson, Hilding Elmqvist, and Martin Otter. "Physical System Modeling with Modelica". In: *Control Engineering Practice* 6.4 (Apr. 1, 1998), pp. 501-510. ISSN: 0967-0661. DOI: 10.1016/S0967-0661(98)00047-1. URL: https://www.sciencedirect.com/science/article/pii/S0967066198000471 (visited on 02/21/2023).

[Mey92] B. Meyer. "Applying 'Design by Contract'". In: *Computer* 25.10 (Oct. 1992), pp. 40-51. ISSN: 1558-0814. DOI: 10.1109/2.161279.

[MN04] Oded Maler and Dejan Nickovic. "Monitoring Temporal Properties of Continuous Signals". In: *Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems*. Ed. by Yassine Lakhnech
and Sergio Yovine. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2004, pp. 152–166. ISBN: 978-3-540-30206-3. DOI: 10.1007/978-3-540-30206-3_12.

[Mül+16] Andreas Müller et al. “A Component-Based Approach to Hybrid Systems Safety Verification”. In: *Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings*. Ed. by Erika Ábrahám and Marieke Huisman. Vol. 9681. Lecture Notes in Computer Science. Springer, 2016, pp. 441–456. ISBN: 978-3-319-33692-3. DOI: 10.1007/978-3-319-33693-0_28.

[Mül+17] Andreas Müller et al. “Change and Delay Contracts for Hybrid System Component Verification”. In: *Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings*. Ed. by Marieke Huisman and Julia Rubin. Vol. 10202. Lecture Notes in Computer Science. Springer, 2017, pp. 134–151. ISBN: 978-3-662-54493-8. DOI: 10.1007/978-3-662-54494-5_8.

[Mül+18] Andreas Müller et al. “Tactical Contract Composition for Hybrid System Component Verification”. In: *International Journal on Software Tools for Technology Transfer* 20.6 (Nov. 1, 2018), pp. 615–643. ISSN: 1433-2787. DOI: 10.1007/s10009-018-0502-9. URL: https://doi.org/10.1007/s10009-018-0502-9 (visited on 02/04/2020).

[NPW02] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. *Isabelle/HOL: A Proof Assistant for Higher-Order Logic*. Lecture Notes in Computer Science, Lect.Notes Computer. Tutorial. Berlin Heidelberg: Springer-Verlag, 2002. ISBN: 978-3-540-43376-7. DOI: 10.1007/3-540-45949-9. URL: https://www.springer.com/gp/book/9783540433767 (visited on 07/02/2021).

[Nuz15] Pierluigi Nuzzo. “Compositional Design of Cyber-Physical Systems Using Contracts”. UC Berkeley, 2015. URL: https://escholarship.org/uc/item/5hk5w3bg (visited on 07/21/2020).

[Osb+05] Leon F. Osborne et al. *Clarus: Concept of Operations*. FHWA-JPO-05-072. Oct. 1, 2005. URL: https://rosap.ntl.bts.gov/view/dot/3710 (visited on 03/13/2023).

[Pla08] André Platzer. “Differential Dynamic Logic for Hybrid Systems”. In: *Journal of Automated Reasoning* 41.2 (Aug. 1, 2008), pp. 143–189. ISSN: 1573-0670. DOI: 10.1007/s10817-008-9103-8. URL: https://doi.org/10.1007/s10817-008-9103-8 (visited on 01/10/2020).
[Pla17] André Platzer. "A Complete Uniform Substitution Calculus for Differential Dynamic Logic". In: *Journal of Automated Reasoning* 59.2 (Aug. 1, 2017), pp. 219–265. ISSN: 1573-0670. DOI: 10.1007/s10817-016-9385-1. URL: https://doi.org/10.1007/s10817-016-9385-1 (visited on 09/17/2021).

[PQ08] André Platzer and Jan-David Quesel. "KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)". In: *Automated Reasoning*. Ed. by Alessandro Armando, Peter Baumgartner, and Gilles Dowek. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2008, pp. 171–178. ISBN: 978-3-540-71070-7. DOI: 10.1007/978-3-540-71070-7_15.

[Raj+10] Ragunathan Rajkumar et al. "Cyber-Physical Systems: The next Computing Revolution". In: *Design Automation Conference*. Design Automation Conference. June 2010, pp. 731–736. DOI: 10.1145/1837274.1837461.

[Ric+15] Daniel Ricketts et al. "Towards Verification of Hybrid Systems in a Foundational Proof Assistant". In: *2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)*. 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE). Austin, TX, USA: IEEE, Sept. 2015, pp. 248–257. ISBN: 978-1-5090-0237-5. DOI: 10.1109/MEMCOD.2015.7340492. URL: http://ieeexplore.ieee.org/document/7340492/ (visited on 09/17/2021).

[RST20] Adnan Rashid, Umair Siddique, and Sofiène Tahar. "Formal Verification of Cyber-Physical Systems Using Theorem Proving". In: *Formal Techniques for Safety-Critical Systems*. Ed. by Osman Hasan and Frédéric Mallet. Communications in Computer and Information Science. Cham: Springer International Publishing, 2020, pp. 3–18. ISBN: 978-3-030-46902-3. DOI: 10.1007/978-3-030-46902-3_1.

[SDP12] Alberto Sangiovanni-Vincentelli, Werner Damm, and Roberto Passerone. "Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems*". In: *European Journal of Control* 18.3 (Jan. 1, 2012), pp. 217–238. ISSN: 0947-3580. DOI: 10.3166/ejc.18.217-238. URL: http://www.sciencedirect.com/science/article/pii/S0947358012709433 (visited on 12/11/2019).

[SO08] Matthieu Sozeau and Nicolas Oury. "First-Class Type Classes". In: *Theorem Proving in Higher Order Logics*. Ed. by Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2008, pp. 278–293. ISBN: 978-3-540-71067-7. DOI: 10.1007/978-3-540-71067-7_23.

[Tea18] The Coq Development Team. *The Coq Proof Assistant, Version 8.7.2*. Zenodo, Feb. 16, 2018. DOI: 10.5281/zenodo.1174360. URL: https://zenodo.org/record/1174360#.YKJOf5MzZXQ (visited on 05/17/2021).
[WC04] Jim Woodcock and Ana Cavalcanti. "A Tutorial Introduction to Designs in Unifying Theories of Programming". In: *Integrated Formal Methods*. Ed. by Eerke A. Boiten, John Derrick, and Graeme Smith. Red. by Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen. Vol. 2999. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 40–66. ISBN: 978-3-540-21377-2. DOI: 10.1007/978-3-540-24756-2_4. URL: http://link.springer.com/10.1007/978-3-540-24756-2_4 (visited on 02/21/2023).

[WZG12] Shuling Wang, Naijun Zhan, and Dimitar Guelev. "An Assume/Guarantee Based Compositional Calculus for Hybrid CSP". In: *Theory and Applications of Models of Computation*. Ed. by Manindra Agrawal, S. Barry Cooper, and Angsheng Li. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2012, pp. 72–83. ISBN: 978-3-642-29952-0. DOI: 10.1007/978-3-642-29952-0_13.

[WZZ15] Shuling Wang, Naijun Zhan, and Liang Zou. "An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems". In: *Formal Methods and Software Engineering*. Ed. by Michael Butler, Sylvain Conchon, and Fatiha Zaïdi. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2015, pp. 382–399. ISBN: 978-3-319-25423-4. DOI: 10.1007/978-3-319-25423-4_25.

[Xu+23] Xiong Xu et al. "Semantics Foundation for Cyber-physical Systems Using Higher-order UTP". In: *ACM Transactions on Software Engineering and Methodology* 32.1 (Feb. 13, 2023), 9:1–9:48. ISSN: 1049-331X. DOI: 10.1145/3517192. URL: https://doi.org/10.1145/3517192 (visited on 02/17/2023).

[Yu+15] Huafeng Yu et al. "The challenge of interoperability: model-based integration for automotive control software". In: *Proceedings of the 52nd Annual Design Automation Conference, San Francisco, CA, USA, June 7-11, 2015*. ACM, 2015, 58:1–58:6. DOI: 10.1145/2744769.2747945. URL: https://doi.org/10.1145/2744769.2747945.

[Yua+16] Zhenghen Yuan et al. "Hybrid Lustre". In: *Perspectives of System Informatics*. Ed. by Manuel Mazzara and Andrei Voronkov. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2016, pp. 325–340. ISBN: 978-3-319-41579-6. DOI: 10.1007/978-3-319-41579-6_25.

[ZH10] Chaochen Zhou and Michael R. Hansen. *Duration Calculus: A Formal Approach to Real-Time Systems*. Softcover reprint of hardcover 1st ed. 2004 Edition. Berlin; London: Springer, Dec. 9, 2010. 260 pp. ISBN: 978-3-642-07404-2.
[Zou+14] Liang Zou et al. "Verifying Chinese Train Control System under a Combined Scenario by Theorem Proving". In: *Verified Software: Theories, Tools, Experiments*. Ed. by Ernie Cohen and Andrey Rybalchenko. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer, 2014, pp. 262–280. ISBN: 978-3-642-54108-7. DOI: 10.1007/978-3-642-54108-7_14.
**Titre** : Sur la vérification mécanisée de la méta-théorie des contrats et son instanciation à la logique dynamique différentielle

**Mots clés** : Méthodes formelles, conception par contrats, systèmes cyber-physiques

**Résumé** : L'augmentation de la complexité et de l'hétérogénéité des systèmes critiques pose un défi dans leur conception et leur assurance de sécurité. Les méthodes formelles sont utilisées pour valider les modèles de système, mais la difficulté réside dans la vérification de la sécurité du système global à partir des spécifications de composants validées. La théorie des contrats résout ce problème en utilisant les contrats d'assomption/garantie comme spécifications de composants. Les contrats sont validés en vérifiant que leurs hypothèses et garanties sur-approximent les pré- et post-conditions résultant des évaluations valides du modèle de composant. Les contrats individuels peuvent être combinés en faisant correspondre les hypothèses et garanties de

chaque composant. Le manuscrit définit une formalisation algébrique des contrats d'assomption/garantie implémenté dans le calcul de construction de l'assistant de preuve Coq. Cette formalisation est prouvée pour valider une méta-théorie des contrats de Benveniste et al. pour tous les opérateurs tels que la composition, la conjonction, l'abstraction, le raffinement ainsi que l'introduction et l'élimination de variables. Le cas d'utilisation pratique du modèle de contrat est illustré avec la logique différentielle dynamique et deux instances du modèle de contrats. La théorie est appliquée à une étude de cas pour illustrer sa puissance dans la modélisation de composants pour valider un système cyber-physique.

**Title** : On the mechanized verification of the meta-theory of contracts and its instantiation to differential dynamic logic

**Keywords** : Formal methods, contract-based design, cyber physical systems

**Abstract** : The increasing complexity and heterogeneity of safe-critical systems present a challenge in designing and ensuring their safety. Formal methods are employed to validate system models, but the difficulty lies in verifying the safety at the global level, starting from validated component specifications. Contract theory addresses this problem by using assume/guarantee contracts as component specifications. The theory is equipped with operators for combining contracts and incrementally building a verified specification from the low-level functional requirements up to system-level requirements. Concretely, a contracts abstract component interfaces as pairs of assumptions-guarantees, specifying

component-environment relations. This thesis introduces the mechanized formalization of an assume/guarantee contracts algebra in the calculus of construction of the proof assistant Coq. In the meantime, the formalization has been proven correct against the Benveniste et al.'s meta-theory formalized in Coq for all the necessary operators: composition, conjunction, abstraction, refinement, as well as the variable introduction and elimination. The practical use case of the contract model is demonstrated with differential dynamic logic and two instances of the contracts model. The theory is exercised on a case study to illustrate its power in modeling components and contractual abstractions.