Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic

TL;DR

This paper introduces a modular framework within differential dynamic logic for modeling and verifying computer-controlled hybrid systems, emphasizing parallel composition and timing guarantees to facilitate safety proofs.

Contribution

It develops a component-based approach in differential dynamic logic that enables modular modeling and automated safety verification of parallel, timing-critical hybrid systems.

Findings

Framework supports parallel component composition with timing guarantees

Automated safety proofs derived from modular component properties

Applicable to safety-critical computer-controlled systems

Abstract

Computer-Controlled Systems (CCS) are a subclass of hybrid systems where the periodic relation of control components to time is paramount. Since they additionally are at the heart of many safety-critical devices, it is of primary importance to correctly model such systems and to ensure they function correctly according to safety requirements. Differential dynamic logic $d\mathcal{L}$ is a powerful logic to model hybrid systems and to prove their correctness. We contribute a component-based modeling and reasoning framework to $d\mathcal{L}$ that separates models into components with timing guarantees, such as reactivity of controllers and controllability of continuous dynamics. Components operate in parallel, with coarse-grained interleaving, periodic execution and communication. We present techniques to automate system safety proofs from isolated, modular, and possibly mechanized proofs of component properties parameterized with timing characteristics.

Tables

Table 1. Table 1: Syntax and semantics of hybrid programs

Program	Semantics
$?\varphi$	Test whether formula $\varphi$ is true, abort if false: ${\rho }_{\nu }\left(?\phi \right)=\{\nu \mid \nu \vDash \phi \}$
$x:=\theta$	Assign value of term $\theta$ to variable $x$:
	${\rho }_{\nu }(x:=\theta )=\{\omega \mid \omega =\nu \text{ except that }{⟦x⟧}_{\omega }={⟦\theta ⟧}_{\nu }\}$
	Evolve ODE $x^{\prime }=\theta$ for any time $t\ge 0$
	with evolution domain constraint $H$ true throughout:
	$f\left(r\right)\vDash x^{\prime }=\theta \text{ and }f\left(r\right)\vDash H\}$
$\alpha ;\beta$	Run $\alpha$ followed by $\beta$ on resulting state(s): ${\rho }_{\nu }(\alpha ;\beta )={\bigcup }_{\omega \in {\rho }_{\nu }\left(\alpha \right)}{\rho }_{\omega }\left(\beta \right)$
$\alpha \cup \beta$	Run either $\alpha$ or $\beta$ non-deterministically: ${\rho }_{\nu }\left(\alpha \cup \beta \right)={\rho }_{\nu }\left(\alpha \right)\cup {\rho }_{\nu }\left(\beta \right)$
${\alpha }^{\ast }$	Repeat $\alpha$ $n$ times, for any $n\in \mathbb{N}$:
	$\rho \left({\alpha }^{\ast }\right)={\bigcup }_{n\in \mathbb{N}}\rho \left({\alpha }^n\right)\text{with}{\alpha }^0=?\top \text{ and }{\alpha }^{n+1}={\alpha }^n;\alpha$

Table 2. Table 2: Semantic of formulas

Equations

$$\phi,\psi::=\phi\land\psi\ |\ \phi\lor\psi\ |\ \phi\rightarrow\psi\ |\ \neg\phi\ |\ \theta_{1}\sim\theta_{2}|\ \forall{x}{~{}\phi}\ |\ \exists{x}{~{}\phi}\ |\ [\alpha]\phi\$$

$$C_1\otimes C_2={({\text{disc}}_1\cup {\text{disc}}_2\cup \{x_1^{\prime }={\theta }_1,x_2^{\prime }={\theta }_2\&H_1\wedge H_2\})}^{\ast }$$

$$\text{RCtrl}(\text{ctrl},\delta )\doteq (?t\le \tau +\delta ;\text{ctrl};\tau :=t)$$

$$\textit{wlctrl}\doteq wlm\mathrel{{:}{=}}wl;\big{(}{(?wlm\geq 6.5;\mathit{fin}\mathrel{{:}{=}}0)}\cup{(?wlm\leq 3.5;\mathit{fin}\mathrel{{:}{=}}1)}\big{)}$$

$$\{w{l}^{\prime }=fin-fout,t^{\prime }=1\&t\ge 0\wedge wl\ge 0\wedge t\le {\Delta }_{\text{wl}}\}$$

$$\textbf{CCS}\doteq{\big{(}\{x^{\prime}=\theta\ \mathbin{\&}\ H\wedge\underbrace{t\leq\tau+\delta}_{\delta\leq\Delta}\}\cup\textbf{RCtrl}(\textit{ctrl},\delta)\big{)}}^{*}$$

$$\left(\begin{array}[]{l}\ \ \ \{wl^{\prime}=\mathit{fin}-\mathit{fout},t^{\prime}=1\ \mathbin{\&}\ t\geq 0\wedge wl\geq 0\wedge t\leq\tau+\delta_{\textit{wlctrl}}\}\\ \cup\ (?t\leq\tau+\delta_{\textit{wlctrl}};\textit{wlctrl};\tau\mathrel{{:}{=}}t)\end{array}\right)^{\ast}$$

$$\left\{\begin{array}[]{c l}A_{\textit{wlctrl}}:&G_{\textit{wl}}\\ G_{\textit{wlctrl}}:&wlm\leq 3.5\rightarrow\mathit{fin}=1\\ &6.5\leq wlm\rightarrow\mathit{fin}=0\\ &(3.5\leq wlm\leq 6.5)\rightarrow(\mathit{fin}=0\vee\mathit{fin}=1)\end{array}\right.$$

$$\left\{\begin{array}[]{c l}A_{\textit{wl}}:&G_{\textit{wlctrl}}\\ G_{\textit{wl}}:&3\leq wl\leq 7\end{array}\right.$$

$$\text{MRCtrl}\left(\bigcup _{1\le i\le n}{\text{ctrl}}_i,\delta \right)\doteq \left(\bigcup _{1\le i\le n}\text{RCtrl}({\text{ctrl}}_i,\delta )\right).$$

$$\text{MRCtrl}\left(\bigcup _{1\le i\le n_{\alpha }}{\alpha }_i\cup \bigcup _{1\le j\le n_{\beta }}{\beta }_j,\mathcal{C}({\delta }_{\alpha },{\delta }_{\beta })\right).$$

$$\begin{array}[]{l l}&\textbf{MRCtrl}\left(\textit{wlctrl}_{1}\cup\textit{wlctrl}_{2},\delta_{\textit{wlctrl}_{1}}+\delta_{\textit{wlctrl}_{2}}\enspace\right)\\ =&\textbf{RCtrl}(\textit{wlctrl}_{1},\delta_{\textit{wlctrl}_{1}}+\delta_{\textit{wlctrl}_{2}})\cup\textbf{RCtrl}(\textit{wlctrl}_{2},\delta_{\textit{wlctrl}_{1}}+\delta_{\textit{wlctrl}_{2}})\\ =&\phantom{\cup}(?t\leq\tau_{1}+\delta_{\textit{wlctrl}_{1}}+\delta_{\textit{wlctrl}_{2}};~{}\textit{wlctrl}_{1};~{}\tau_{1}\mathrel{{:}{=}}t)\\ &\cup(?t\leq\tau_{2}+\delta_{\textit{wlctrl}_{1}}+\delta_{\textit{wlctrl}_{2}};~{}\textit{wlctrl}_{2};~{}\tau_{2}\mathrel{{:}{=}}t)\end{array}$$

$$\begin{array}[]{l c l r}\alpha\ \otimes\ \beta&=&\beta\ \otimes\ \alpha&\mbox{ (Commutativity)}\\ (\alpha\ \otimes\ \beta)\ \otimes\ \gamma&=&\alpha\ \otimes\ (\beta\ \otimes\ \gamma)&\mbox{ (Associativity)}\end{array}$$

$$\begin{array}[]{l l r}&\alpha\ \otimes\ \beta&\\ \doteq&\textbf{MRCtrl}\left(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i}\cup\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\enspace\right)&\mbox{(Unfolding definition)}\\ \doteq&\textbf{MRCtrl}\left(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j}\cup\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\enspace\right)&\mbox{(Commutativity of $\cup$ )}\\ \doteq&\textbf{MRCtrl}\left(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j}\cup\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\beta},\delta_{\alpha})\enspace\right)&\mbox{(Commutativity of $S$)}\\ \doteq&\beta\ \otimes\ \alpha&\mbox{(Folding definition)}\end{array}$$

$$\begin{array}[]{l l}&(\alpha\ \otimes\ \beta)\ \otimes\ \gamma\\ \doteq&\textbf{MRCtrl}\left((\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i}\cup\bigcup_{1\leq j\leq n_{\beta}}\beta_{j})\cup\bigcup_{1\leq k\leq n_{\gamma}}\gamma_{k},{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\enspace\right)\\ &\mbox{(Unfolding definition)}\\ \doteq&\textbf{MRCtrl}\left(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i}\cup(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j}\cup\bigcup_{1\leq k\leq n_{\gamma}}\gamma_{k}),{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\enspace\right)\\ &\mbox{(Associativity of $\cup$)}\\ \doteq&\textbf{MRCtrl}\left((\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i}\cup\bigcup_{1\leq j\leq n_{\beta}}\beta_{j})\cup\bigcup_{1\leq k\leq n_{\gamma}}\gamma_{k},{\mathcal{C}}(\delta_{\alpha},{\mathcal{C}}(\delta_{\beta},\delta_{\gamma}))\enspace\right)\\ &\mbox{(Associativity of $S$)}\\ \doteq&\alpha\ \otimes\ (\beta\ \otimes\ \gamma)\\ &\mbox{(Folding definition)}\end{array}$$

$$\left\{\begin{array}[]{c l}A_{\textit{wlctrl}_{2}}:&\top\\ G_{\textit{wlctrl}_{2}}:&wlm_{2}\leq 2.3\rightarrow\mathit{fout}_{2}=0\\ &9.7\leq wlm_{2}\rightarrow\mathit{fout}_{2}=1\\ &(2.3\leq wlm_{2}\leq 9.7)\rightarrow(\mathit{fout}_{2}=0\vee\mathit{fout}_{2}=1)\end{array}\right.$$

$$\begin{gathered} \{w{l}_1^{\prime }=fin-{fout}_1,w{l}_2^{\prime }={fout}_1-{fout}_2,t^{\prime }=1 \\ \&{\text{wl}}_1\ge 0\wedge {\text{wl}}_2\ge 0\wedge t\le min({\Delta }_{{\text{wl}}_1},{\Delta }_{{\text{wl}}_2})\} \end{gathered}$$

$$\begin{array}[]{l c l r}\alpha\ \otimes\ \beta&=&\beta\ \otimes\ \alpha&\mbox{ (Commutativity)}\\ (\alpha\ \otimes\ \beta)\ \otimes\ \gamma&=&\alpha\ \otimes\ (\beta\ \otimes\ \gamma)&\mbox{ (Associativity)}\end{array}$$

$$\begin{array}[]{l l r}&\alpha\ \otimes\ \beta&\\ \doteq&\textbf{CPlant}\big{(}\{x^{\prime}=\theta_{x},y^{\prime}=\theta_{y}\ \mathbin{\&}\ H_{x}\wedge H_{y}\},min(\Delta_{\alpha},\Delta_{\beta})\big{)}&\mbox{(Unfolding definition)}\\ \doteq&\textbf{CPlant}\big{(}\{y^{\prime}=\theta_{y},x^{\prime}=\theta_{x}\ \mathbin{\&}\ H_{x}\wedge H_{y}\},min(\Delta_{\alpha},\Delta_{\beta})\big{)}&\mbox{(Commutativity of ``,'')}\\ \doteq&\textbf{CPlant}\big{(}\{y^{\prime}=\theta_{y},x^{\prime}=\theta_{x}\ \mathbin{\&}\ H_{y}\wedge H_{x}\},min(\Delta_{\alpha},\Delta_{\beta})\big{)}&\mbox{(Commutativity of $\wedge$)}\\ \doteq&\textbf{CPlant}\big{(}\{y^{\prime}=\theta_{y},x^{\prime}=\theta_{x}\ \mathbin{\&}\ H_{y}\wedge H_{x}\},min(\Delta_{\beta},\Delta_{\alpha})\big{)}&\mbox{(Commutativity of $min(\cdot,\cdot)$)}\\ \doteq&\beta\ \otimes\ \alpha&\mbox{(Folding definition)}\end{array}$$

$$\begin{array}[]{l l}&(\alpha\ \otimes\ \beta)\ \otimes\ \gamma\\ \doteq&\textbf{CPlant}\big{(}\{(x^{\prime}=\theta_{x},y^{\prime}=\theta_{y}),z^{\prime}=\theta_{z}\ \mathbin{\&}\ (H_{x}\wedge H_{y})\wedge H_{z}\},min(min(\Delta_{\alpha},\Delta_{\beta}),\Delta_{\gamma})\big{)}\\ &\mbox{(Unfolding definition)}\\ \doteq&\textbf{CPlant}\big{(}\{x^{\prime}=\theta_{x},(y^{\prime}=\theta_{y},z^{\prime}=\theta_{z})\ \mathbin{\&}\ (H_{x}\wedge H_{y})\wedge H_{z}\},min(min(\Delta_{\alpha},\Delta_{\beta}),\Delta_{\gamma})\big{)}\\ &\mbox{(Associativity of ``,'')}\\ \doteq&\textbf{CPlant}\big{(}\{x^{\prime}=\theta_{x},(y^{\prime}=\theta_{y},z^{\prime}=\theta_{z})\ \mathbin{\&}\ H_{x}\wedge(H_{y}\wedge H_{z})\},min(min(\Delta_{\alpha},\Delta_{\beta}),\Delta_{\gamma})\big{)}\\ &\mbox{(Associativity of $\wedge$)}\\ \doteq&\textbf{CPlant}\big{(}\{x^{\prime}=\theta_{x},(y^{\prime}=\theta_{y},z^{\prime}=\theta_{z})\ \mathbin{\&}\ H_{x}\wedge(H_{y}\wedge H_{z})\},min(\Delta_{\alpha},min(\Delta_{\beta},\Delta_{\gamma}))\big{)}\\ &\mbox{(Associativity of $min(\cdot,\cdot)$)}\\ \doteq&\alpha\ \otimes\ (\beta\ \otimes\ \gamma)\\ &\mbox{(Folding definition)}\end{array}$$

$$DG[\{x^{\prime }=f(x)\&H_x\}]p(x)\leftrightarrow \exists y[\{x^{\prime }=f(x),y^{\prime }=a(x)y+b(x)\&H_x\}]p(x)$$

$$\left\{\begin{array}[]{c l}A_{\textit{wl}_{2}}:&G_{\textit{wlctrl}_{2}}\\ G_{\textit{wl}_{2}}:&2\leq\textit{wl}_{2}\leq 10\end{array}\right.$$

$$\begin{array}[]{l}{\bigg{(}\{y^{\prime}=\theta,t^{\prime}=1\ \mathbin{\&}\ H\wedge\underbrace{\bigwedge_{1\leq i\leq n}t\leq\tau_{i}+\delta}_{\delta\leq\Delta}\}\cup\textbf{MRCtrl}\left(\bigcup_{1\leq i\leq n}ctrl_{i},\delta\right)\bigg{)}}^{*}\end{array}$$

$$\left(\begin{array}[]{l}\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\big{)}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq m}\beta_{j},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\big{)}\\ \cup\{x^{\prime}=\theta,y^{\prime}=\eta,t^{\prime}=1\ \mathbin{\&}\ H\wedge Q\\ \qquad\qquad\wedge\underbrace{\bigwedge_{1\leq i\leq n}t\leq\tau_{i}+{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})~{}\wedge\bigwedge_{1\leq j\leq m}t\leq\tau_{j}+{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})}_{{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\leq min(\Delta_{\alpha},\Delta_{\beta})}\}\end{array}\right)^{\ast}$$

$$\begin{array}[]{l}\bigg{(}\{x^{\prime}=\theta_{x},t^{\prime}=1\ \mathbin{\&}\ H_{x}\wedge\bigwedge_{1\leq i\leq n_{\alpha}}t\leq\tau_{i}+\delta_{\alpha}\}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},\delta_{\alpha}\big{)}\bigg{)}^{\ast}\\ \bigg{(}\{y^{\prime}=\theta_{y},t^{\prime}=1\ \mathbin{\&}\ H_{y}\wedge\bigwedge_{1\leq j\leq n_{\beta}}t\leq\tau_{j}+\delta_{\beta}\}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},\delta_{\beta}\big{)}\bigg{)}^{\ast}\\ \bigg{(}\{z^{\prime}=\theta_{z},t^{\prime}=1\ \mathbin{\&}\ H_{z}\wedge\bigwedge_{1\leq k\leq n_{\gamma}}t\leq\tau_{k}+\delta^{\gamma}\}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq k\leq n_{\gamma}}\gamma_{k},\delta^{\gamma}\big{)}\bigg{)}^{\ast}.\end{array}$$

$$\begin{array}[]{l c l r}\alpha\ \otimes\ \beta&=&\beta\ \otimes\ \alpha&\mbox{ (Commutativity)}\\ (\alpha\ \otimes\ \beta)\ \otimes\ \gamma&=&\alpha\ \otimes\ (\beta\ \otimes\ \gamma)&\mbox{ (Associativity)}\end{array}$$

$$\begin{array}[]{ll}&\alpha\ \otimes\ \beta\\ \doteq\bigg{(}&\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\big{)}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\big{)}\\ &\cup\{x^{\prime}=\theta_{x},y^{\prime}=\theta_{y},t^{\prime}=1\ \mathbin{\&}\ H_{x}\wedge H_{y}\\ &\wedge\bigwedge_{1\leq i\leq n_{\alpha}}t\leq\tau_{i}+{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\wedge\bigwedge_{1\leq j\leq n_{\beta}}t\leq\tau_{j}+{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\}\bigg{)}^{\ast}\\ &\mbox{(Unfolding definition)}\\ \doteq\bigg{(}&\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}(\delta_{\beta},\delta_{\alpha})\big{)}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\beta},\delta_{\alpha})\big{)}\\ &\cup\{x^{\prime}=\theta_{x},y^{\prime}=\theta_{y},t^{\prime}=1\ \mathbin{\&}\ H_{x}\wedge H_{y}\\ &\wedge\bigwedge_{1\leq i\leq n_{\alpha}}t\leq\tau_{i}+{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\wedge\bigwedge_{1\leq j\leq n_{\beta}}t\leq\tau_{j}+{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\}\bigg{)}^{\ast}\\ &\mbox{(Proposition~{}\ref{prop:AlgCompoDisc})}\\ \doteq\bigg{(}&\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}(\delta_{\beta},\delta_{\alpha})\big{)}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\beta},\delta_{\alpha})\big{)}\\ &\cup\{y^{\prime}=\theta_{y},x^{\prime}=\theta_{x},t^{\prime}=1\ \mathbin{\&}\ H_{y}\wedge H_{x}\\ &\wedge\bigwedge_{1\leq j\leq n_{\beta}}t\leq\tau_{j}+{\mathcal{C}}(\delta_{\beta},\delta_{\alpha})\wedge\bigwedge_{1\leq i\leq n_{\alpha}}t\leq\tau_{i}+{\mathcal{C}}(\delta_{\beta},\delta_{\alpha})\}\bigg{)}^{\ast}\\ &\mbox{(Proposition~{}\ref{prop:AlgCompoCont})}\\ \doteq&\beta\ \otimes\ \alpha\\ &\mbox{(Folding definition)}\end{array}$$

$$\begin{array}[]{ll}&(\alpha\ \otimes\ \beta)\ \otimes\ \gamma\\ \doteq\Bigg{(}&\bigg{(}\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\big{)}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\big{)}\bigg{)}\\ &\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq k\leq n_{\gamma}}\gamma_{k},{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\big{)}\\ &\cup\{x^{\prime}=\theta_{x},y^{\prime}=\theta_{y},z^{\prime}=\theta_{z},t^{\prime}=1\ \mathbin{\&}\ (H_{x}\wedge H_{y})\wedge H_{z}\\ &\wedge\big{(}\bigwedge_{1\leq i\leq n_{\alpha}}t\leq\tau_{i}+{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\wedge\bigwedge_{1\leq j\leq n_{\beta}}t\leq\tau_{j}+{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\big{)}\\ &\wedge\bigwedge_{1\leq k\leq n_{\gamma}}t\leq\tau_{k}+{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\}\Bigg{)}^{\ast}\\ &\mbox{(Unfolding definition)}\\ \doteq\Bigg{(}&\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},{\mathcal{C}}(\delta_{\beta},\delta_{\gamma}))\big{)}\cup\bigg{(}\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}(\delta_{\alpha},{\mathcal{C}}(\delta_{\beta},\delta_{\gamma}))\big{)}\\ &\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq k\leq n_{\gamma}}\gamma_{k},{\mathcal{C}}(\delta_{\alpha},{\mathcal{C}}(\delta_{\beta},\delta_{\gamma}))\big{)}\bigg{)}\\ &\cup\{x^{\prime}=\theta_{x},y^{\prime}=\theta_{y},z^{\prime}=\theta_{z},t^{\prime}=1\ \mathbin{\&}\ (H_{x}\wedge H_{y})\wedge H_{z}\\ &\wedge\big{(}\bigwedge_{1\leq i\leq n_{\alpha}}t\leq\tau_{i}+{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\wedge\bigwedge_{1\leq j\leq n_{\beta}}t\leq\tau_{j}+{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\big{)}\\ &\wedge\bigwedge_{1\leq k\leq n_{\gamma}}t\leq\tau_{k}+{\mathcal{C}}({\mathcal{C}}(\delta_{\alpha},\delta_{\beta}),\delta_{\gamma})\}\Bigg{)}^{\ast}\\ &\mbox{(Proposition~{}\ref{prop:AlgCompoDisc})}\\ \doteq\Bigg{(}&\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},{\mathcal{C}}(\delta_{\beta},\delta_{\gamma}))\big{)}\cup\bigg{(}\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}(\delta_{\alpha},{\mathcal{C}}(\delta_{\beta},\delta_{\gamma}))\big{)}\\ &\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq k\leq n_{\gamma}}\gamma_{k},{\mathcal{C}}(\delta_{\alpha},{\mathcal{C}}(\delta_{\beta},\delta_{\gamma}))\big{)}\bigg{)}\\ &\cup\{x^{\prime}=\theta_{x},y^{\prime}=\theta_{y},z^{\prime}=\theta_{z},t^{\prime}=1\ \mathbin{\&}\ H_{x}\wedge(H_{y}\wedge H_{z})\\ &\wedge\bigwedge_{1\leq i\leq n_{\alpha}}t\leq\tau_{i}+{\mathcal{C}}(\delta_{\alpha},{\mathcal{C}}(\delta_{\beta},\delta_{\gamma}))\wedge\big{(}\bigwedge_{1\leq j\leq n_{\beta}}t\leq\tau_{j}+{\mathcal{C}}(\delta_{\alpha},{\mathcal{C}}(\delta_{\beta},\delta_{\gamma}))\\ &\wedge\bigwedge_{1\leq k\leq n_{\gamma}}t\leq\tau_{k}+{\mathcal{C}}(\delta_{\alpha},{\mathcal{C}}(\delta_{\beta},\delta_{\gamma}))\big{)}\}\Bigg{)}^{\ast}\\ &\mbox{(Proposition~{}\ref{prop:AlgCompoCont})}\\ \doteq&\alpha\ \otimes\ (\beta\ \otimes\ \gamma)\\ &\mbox{(Folding definition)}\end{array}$$

$$\left(\begin{array}[]{l}\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\big{)}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq m}\beta_{j},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\big{)}\\ \cup\{x^{\prime}=\theta_{x},y^{\prime}=\theta_{y},t^{\prime}=1\ \mathbin{\&}\ H_{x}\wedge H_{y}\\ \wedge\bigwedge_{1\leq i\leq n}t\leq\tau_{i}+{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\wedge\bigwedge_{1\leq j\leq m}t\leq\tau_{j}+{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\}\end{array}\right)^{\ast}$$

$$\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\big{)}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq m}\beta_{j},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\big{)}$$

Full text

1 Introduction

A computer-controlled system (CCS) is a hybrid system with discrete hardware-software components that control a specific physical phenomenon, *e.g. *the water level of a tank in a water-recycling plant. CCSs are widely used in industry to monitor time-critical and safety-critical processes. While CCS defines a large class of hybrid systems, systems mixing physical phenomena and natural discrete interactions (e.g. a bouncing-ball) are neither CCSs nor the focus of this work, although most could easily be given verification models in $d\mathcal{L}$. Tools to model, verify, and design CCSs need to capture mixed discrete and continuous dynamics, as well as mixed logical, discretized real-time and continuous time in, resp., computer programs, electronics, and physics models.

CCSs are difficult to model since they subsume the problem of designing a software controller and its real-timed hardware. Our aim is to develop a component-based approach to engineer such systems in a modular manner while accounting for time domain boundaries across components. In component-based design, a system is constructed from smaller elements that are modeled and individually verified, then assembled and checked for consistency to form larger components and subsystems. The CCS components typically execute in parallel, and concurrency must be accounted for in the envisioned verification framework.

In this paper, we contribute a component-based verification technique that aims at the definition of a bottom-up and modular verification methodology through a correct-by-construction system design methodology, in which component contracts formalize the domain, timing, and invariants of components. The proof of a system model is built by assembling the contracts of its components through formally defined composition mechanisms. Contracts-based approaches have been successfully implemented for several paradigms such as programming languages [15] or automata [2], because contracts are very efficient to make proofs easier scalable. Following the component-based design widely used for CCS, contracts provide a natural way to get modularity and abstraction in proofs.

To meet the specific time-criticality requirements of CCSs, we start from earlier compositionality results in $d\mathcal{L}$ [7] to elaborate a timed model of parallel composition that forms the foundation of our modeling and verification framework. In Sec. 3, we detail the modeling part and the verification part of our framework on a simple system where only one reactive controller monitors a plant. In Sec. 4, we generalize it step-by-step to systems where multiple controllers monitor multiple parallel plants; we show how to compose: multiple reactive controllers into a component called Multi-Choice Reactive Controllers (MRCtrl, see Sec. 4.1); multiple controllable plants together (see Sec. 4.2); MRCtrl with controllable plants to form Multi Computer-Controlled Systems (MCCS, see Sec. 4.3); and finally how MCCS compose (see Sec. 4.4).

2 Differential Dynamic Logic

This section briefly recalls differential dynamic logic ($d\mathcal{L}$ [12]) and its proof system, which is implemented in the theorem prover KeYmaera X [3].

In $d\mathcal{L}$, hybrid programs are used as a programming language for expressing the combined discrete and continuous dynamics of hybrid systems (the programs operate over mathematical reals). The syntax and semantics of hybrid programs is summarized in Tab. 1. The set of reachable states from state $\nu$ by hybrid program $\alpha$ is noted $\rho_{\nu}(\alpha)$, and $\ldbrack x\rdbrack_{\nu}$ denotes the value of $x$ at state $\nu$.

Hybrid programs include discrete assignment $x\mathrel{{:}{=}}\theta$ and tests $?\phi$, as well as combinators for non-deterministic choice ($\alpha\cup\beta$), sequential composition ($\alpha;\beta$), and non-deterministic repetition (${\alpha}^{*}$). The notation $\{x^{\prime}=\theta\ \mathbin{\&}\ H\}$ denotes an ordinary differential equation (ODE) system (derivatives with respect to time) of the form $x^{\prime}_{1}=\theta_{1}$, …, $x^{\prime}_{n}=\theta_{n}$ within evolution domain $H$. For example, the ODE $\{t^{\prime}=1\ \mathbin{\&}\ t\geq 0\}$ describes that variable $t$ evolves with constant slope $1$, where $t\geq 0$ discards any negative values. Formulas of $d\mathcal{L}$ formalize properties:

Definition 1 ($d\mathcal{L}$ formulas)

The formulas $\phi,\psi$ of $d\mathcal{L}$ relevant in this paper consist of the following operators:

[TABLE]

Connectives $\phi\land\psi$, $\phi\lor\psi$, $\phi\rightarrow\psi$,$\neg\phi$, $\forall{x}{~{}\phi}$, and $\exists{x}{~{}\phi}$ are according to classical first-order logic. Formula $\theta_{1}\sim\theta_{2}$ are any comparison operator $\sim\mathop{\in}\{\leq,<,=,\neq,>,\geq\}$ and $\theta_{i}$ are real-valued terms in operators $\{+,-,\cdot,/\}$. The modal operator $[\alpha]\phi$ is true iff $\phi$ holds in all states reachable by program $\alpha$.

The notion of free and bound variables is defined in the static semantics of $d\mathcal{L}$ [12] and useful to characterize the interaction of a program $\alpha$ with its context. It is computed from the syntactic structure of programs: the bound variables $\text{BV}(\alpha)$ can be updated by assignments (e.g. $x\mathrel{{:}{=}}10$) or ODEs (e.g. $x^{\prime}=3$) in $\alpha$, whereas free variables $\text{FV}(\alpha)$ are those that the program depends on. For example, in program $\alpha\equiv({v\mathrel{{:}{=}}a}\cup{v\mathrel{{:}{=}}2});\{x^{\prime}=v\ \mathbin{\&}\ x\leq 5\}$ the free variables are $\text{FV}(\alpha)=\{a,x\}$ (the variable $v$ is not free, because it is bound on all paths of $\alpha$ and so the result of $\alpha$ does not depend on the initial value of $v$; even though also modified, variable $x$ is free because the result of $\alpha$ depends on the initial value of $x$) and the bound variables are $\text{BV}(\alpha)=\{v,x\}$ (variable $a$ is not bound because it is not modified anywhere in the program). We use $\text{V}(\alpha)$ to denote $\text{BV}(\alpha)\cup\text{FV}(\alpha)$.

In [7], a component model $C_{i}={({\textbf{disc}_{i}}\cup{\textbf{cont}_{i}})}^{*}$ is evaluated as the non-deterministic interleaving of its discrete specifications $\textbf{disc}_{i}$ and the ODE $\textbf{cont}_{i}=\{x_{i}^{\prime}=\theta_{i}\ \mathbin{\&}\ H_{i}\}$. For $i\in\{1,2\}$, the parallel composition of $C_{1}$ and $C_{2}$ builds a component of the same structure, i.e. the dicrete parts $\textbf{disc}_{1}$ and $\textbf{disc}_{2}$ are non-deterministically interleaved within the evolution of the ODE obtained from the mathematical composition of $\textbf{cont}_{1}$ and $\textbf{cont}_{2}$. In $d\mathcal{L}$, it is defined

[TABLE]

The logic $d\mathcal{L}$ further enjoys a proof calculus [11, 12, 13] based on uniform substitution from axioms. Its base axioms are those of a classical first-order sequent calculus. A second set of axioms is dedicated to goals of the form $[\alpha]\phi$, supporting syntactical deconstruction of hybrid programs $\alpha$. The last set of axioms is dedicated to iteration and ODEs [14].

3 Computer-Controlled Systems

We present a component-based approach to model and verify Computer Controlled Systems (CCS) based on the parallel composition pattern proposed in [7]. We construct the proof of a CCS from the isolated sub-proofs of its components by syntactically decomposing the CCS using the axioms of $d\mathcal{L}$, so that the theorems presented here can be implemented as tactics in the theorem prover KeYmaera X. This enables automation to reduce the proof complexity of analyzing a CCS to that of modularly analyzing its components.

In this section, we introduce the necessary concepts to adapt the framework of [7] to systematically model CCSs modularly. We achieve modularity by limiting the ways in which the free and bound variables of different components may overlap, and by taking into account the timing constraints of CCSs. The idea is to analyze the controllability of the plant, *i.e. *the period of time it can evolve safely without intervention of a controller, and the reactivity of the controller, *i.e. *the execution period of the controller. These concepts satisfy the associativity property of parallel composition and the ability to retain contracts from [7].

3.1 Modeling CCS

A CCS is classically composed of a controller and a plant. The controller measures the state of the plant through sensing and regulates the behavior of the plant through actuation. For example, the controller in the water tank regulates the water level by opening or closing a faucet. The key trait of a CCS is the periodic execution of the controller to regulate the plant. We associate periodic values $\delta$ and $\Delta$ with the controller and the plant, respectively: Control reactivity $\delta$ models the period in which control is guaranteed to happen. Plant controllability $\Delta$ models how long a plant can evolve safely without control intervention.

3.1.1 Time.

To make timed reasoning available to any component, we use the ODE $\textbf{Time}(t)\doteq\{t^{\prime}=1\ \mathbin{\&}\ t\geq 0\}$. The hence defined global variable $t$ represents time passing with constant slope $1$, initialized to [math].

3.1.2 Controller.

The functional behavior of a controller is provided as a discrete program ctrl and the associated reactivity $\delta$. The controller acts at least every $\delta$ units of time, see Def. 2.

Definition 2 (Reactive Controller)

A reactive controller $\textbf{RCtrl}(\textit{ctrl},\delta)$ with reactivity boundary $\delta$ and fresh timestamp $\tau$ has the program shape

[TABLE]

Execution periodicity is ensured by a fresh variable $\tau$ time stamping ($\tau\mathrel{{:}{=}}t$) the last execution of ctrl. The prefixing guard $?t\leq\tau+\delta$ forces ctrl to be executed within $\delta$ time since its last execution $\tau$. This pattern models control frequency, since all runs not satisfying a test are aborted, see Sec. 2.

Example 1 (Water-level Controller)

We consider the water level controller in a water plant. When the level reaches a maximum (resp. minimum) threshold, we close the inlet faucet $\mathit{fin}$ (resp. we open the inlet faucet). The resulting controller has the program shape $\textbf{RCtrl}(\textit{wlctrl},\delta_{\textit{wlctrl}})$ i.e. $(?t\leq\tau+\delta_{\textit{wlctrl}};~{}\textit{wlctrl};~{}\tau\mathrel{{:}{=}}t)$, where $\delta_{\textit{wlctrl}}=0.05s$ ensures a control frequency of at least 20Hz. The controller:

[TABLE]

measures the water level using $wlm\mathrel{{:}{=}}wl$ and then sets $\mathit{fin}$ depending on whether the water level exceeds the minimum threshold $3.5$ or the maximum threshold $6.5$. This controller makes implicit assumptions on the maximum inflow and outflow of the water tank through the relation between its reactivity $\delta_{\textit{wlctrl}}$ and the thresholds on $wlm$.

3.1.3 Plant.

The functional behavior of the plant is provided as an ODE system $\{x^{\prime}=\theta\ \mathbin{\&}\ H\}$ with $t\not\in\text{V}(x^{\prime}=\theta)$ and the controllability bound $\Delta$. Controllability is implemented by adding the formula $t\leq\Delta$ to the evolution domain, see Def. 3.

Definition 3 (Controllable Plant)

A controllable plant $\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta)$ with controllability bound $\Delta$ is an ODE system of the shape $\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta)\doteq\{x^{\prime}=\theta\ \mathbin{\&}\ H\wedge t\leq\Delta\}$, combined with time defined by $\textbf{Time}(t)$.

Example 2 (Water-level)

The evolution of the water level $wl$ in the tank is determined by the difference between the inlet flow $\mathit{fin}$ and the outlet flow $\mathit{fout}$. The water level is always non-negative ($H\doteq wl\geq 0$), and so the controllable water level is the ODE with controllability $\Delta_{\textit{wl}}=0.2s$:

[TABLE]

We compose the plant with the controller to a full system with repeated interaction between the plant and the controller.

3.1.4 Full system.

The full system is obtained by applying parallel composition as defined in (1) to the plant and the controller, but with one important change: the formula $t\leq\Delta$ is replaced by the formula $t\leq\tau+\delta$ to ensure that the plant suspends when the controller is expected to run, see Def. 4.

Definition 4 (Computer-Controlled System)

A computer-controlled system CCS is a parallel composition of a reactive controller $\textbf{RCtrl}(\textit{ctrl},\delta)$ and a controllable plant $\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta)$ with $\delta\leq\Delta$ and the resulting hybrid program shape, assuming $\textbf{Time}(t)$ and, initially, $\tau=t$:

[TABLE]

Execution between the controller and the plant switches based on the variable $\tau$. At the beginning of each loop iteration, we have $t\geq\tau$. The difference $t-\tau$ grows according to the evolution of time until the point $t-\tau=\delta$. At the latest, then, the controller must act before the plant can continue. Safety requires $\delta\leq\Delta$, *i.e. *the reactivity of the controller is at most the controllability of the plant. Otherwise, there may be runs of the whole system where the controller executes too late for the plant to stay safe.

Example 3 (Water-tank)

We compose the water level with its controller to obtain the water tank system with the following behavior:

[TABLE]

The composition is possible because the reactivity of the controller ($\delta_{\textit{wlctrl}}=0.05s$) does not exceed the controllability of the plant ($\Delta_{\textit{wl}}=0.2s$).

3.2 Modular Verification of a CCS

Based on the modular modeling capabilities offered by the concepts of Sec. 3.1 and through [7, Thm. 2], we provide techniques to verify the safety of a complete system from safety proofs of its components (which can be reactive controllers, controllable plants, or subsystems built from those following the computer-controlled systems composition). The proofs of our theorems are syntactic using the axioms of $d\mathcal{L}$ (as opposed to the semantic proofs in [7]) and are, thus, implementable as tactics in the theorem prover KeYmaera X [3].

3.2.1 Environment.

A description of the global system environment $\mathcal{E}$ characterizing constants (either as exact values or through their relevant characteristics) is necessary. We require that $\text{FV}(\mathcal{E})\cap\text{BV}(\alpha)=\emptyset$ for all system components $\alpha$ to ensure that the environment variables are constants: these constants are not controlled, but can be read by all components. (*e.g. *, gravity constant $g$).

Example 4 (Water tank environment)

In the water tank example, the environment $\mathcal{E}_{wt}\doteq\mathit{fout}=0.75\wedge\delta_{\textit{wlctrl}}=0.05\wedge\Delta_{\textit{wl}}=0.2$ is the outlet flow $\mathit{fout}$ of $0.75$, plant controllability $\Delta_{\textit{wl}}$ of $0.2s$, and controller reactivity $\delta_{\textit{wlctrl}}$ of $0.05s$.

3.2.2 Contracts.

A designer specifies the assumptions $A_{\textit{ctrl}}$ and guarantees $G_{\textit{ctrl}}$ of the controller as well as the assumption $A_{\textit{plant}}$ and guarantees $G_{\textit{plant}}$ of the plant. In order to be compositional, the guarantees of the controller must not refer to outputs of the plant and inversely ($\text{FV}(G_{\textit{ctrl}})\cap\text{BV}(\textit{plant})=\emptyset$ and $\text{FV}(G_{\textit{plant}})\cap\text{BV}(\textit{ctrl})=\emptyset$). A component $\alpha$ satisfies its contract $(A_{\alpha},G_{\alpha})$ in environment $\mathcal{E}$ under starting conditions $Init_{\alpha}$ if formula $(\mathcal{E}\wedge A_{\alpha}\wedge Init_{\alpha})\rightarrow[{\alpha}^{*}]G_{\alpha}$ is valid (*e.g. *, proved using the $d\mathcal{L}$ proof calculus). Unlike the environment $\mathcal{E}$, the initial conditions $Init_{\alpha}$ and assumptions $A_{\alpha}$ of a component $\alpha$ can mention assumptions about the state of other components.

Example 5 (Water tank contracts)

The water-level controller assumes that the actual water level in the tank ranges over the interval $[3,7]$ (as guaranteed by the tank), and itself guarantees to drain the tank when the measured water level approaches the upper threshold $6.5$, and fill the tank when below the lower threshold $3.5$. The tank contract assumes that the tank is instructed correctly to drain or fill, and then guarantees to keep the water level in the limits $[3,7]$.

[TABLE]

[TABLE]

These contracts assume that the measured water level is correct, *i.e. *it corresponds to the true water level in the tank, so $Init_{\textit{ctrl}}\equiv wl=wlm$ and also $Init_{\textit{plant}}\equiv wl=wlm$. As we compose the controller and plant components to a full system, where the plant evolves for some time between controller runs (and thus measurements), we will need to find a condition that describes how the true water level evolves in relationship to the measured water level.

3.2.3 Full system.

The contract $(A_{\textit{ctrl}}\wedge A_{\textit{plant}},G_{\textit{ctrl}}\wedge G_{\textit{plant}})$ for the full system is the conjunction of the assumptions and of the guarantees.

Composition invariant.

In the full system, the controller and the plant will run in a quasi-parallel fashion, so time passes between controller runs and thus in turn between measurements of the true plant values. With a composition invariant $J_{\text{cmp}}$ we describe the relationship between the true values of the plant and the measured values in the controller. The formula $J_{\text{cmp}}$ is a composition invariant for two components $\alpha$ and $\beta$ if the formulas $J_{\text{cmp}}\rightarrow[\alpha]J_{\text{cmp}}$ and $J_{\text{cmp}}\rightarrow[\beta]J_{\text{cmp}}$ are valid (components maintain the composition invariant), and $Init_{\alpha}\land Init_{\beta}\rightarrow J_{\text{cmp}}$ is valid (composition invariant is initially satisfied).

Each component is responsible for satisfying its own guarantees and can assume that others will satisfy its assumptions. We also require that other components do not interfere with a component’s guarantees. This notion of non-interference ensures that contracts focus on the behavior of their own component (but nothing else), as intuitively expected.

Definition 5 (Non-interfering Controller and Plant)

A controller ctrl and plant $\{x^{\prime}=\theta\&H\}$ are non-interfering if they do not influence the guarantees of the respective other component, so $\text{FV}(G_{\textit{ctrl}})\cap\text{BV}(\{x^{\prime}=\theta\&H\})=\emptyset$ and $\text{FV}(G_{\textit{plant}})\cap\text{BV}(\textit{ctrl})=\emptyset$, and if they do not share the same outputs, so $\text{BV}(\textit{ctrl})\cap\text{BV}(\{x^{\prime}=\theta\&H\})=\emptyset$.

For composition it is important that contracts are compatible, meaning that they mutually satisfy their assumptions from their respective guarantees.

Definition 6 (Compatible Contracts)

Contracts $(A_{\alpha},G_{\alpha})$ and $(A_{\beta},G_{\beta})$ of components $\alpha$ and $\beta$ with composition invariant $J_{\text{cmp}}$ are compatible if the formulas $A_{\alpha}\rightarrow[\beta](G_{\beta}\land J_{\text{cmp}}\rightarrow A_{\alpha})$ and $A_{\beta}\rightarrow[\alpha](G_{\alpha}\land J_{\text{cmp}}\rightarrow A_{\beta})$ are valid.

Theorem 3.1 (Safe composition of controller and plant)

Let $\textbf{RCtrl}(\textit{ctrl},\delta)$ be a reactive controller satisfying its contract $(A_{\textit{ctrl}},G_{\textit{ctrl}})$ and $\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta)$ be a controllable plant satisfying its contract $(A_{\textit{plant}},G_{\textit{plant}})$. Further let the components $\textbf{RCtrl}(\textit{ctrl},\delta)$ and $\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta)$ be non-interfering, the contracts $(A_{\textit{ctrl}},G_{\textit{ctrl}})$ and $(A_{\textit{plant}},G_{\textit{plant}})$ be compatible, and $J_{\text{cmp}}$ be a composition invariant. Then, the parallel composition CCS is safe, i.e., $(\mathcal{E}\land A_{\textit{ctrl}}\land Init_{\textit{ctrl}}\land A_{\textit{plant}}\land Init_{\textit{plant}})\rightarrow[\textbf{CCS}](G_{\textit{ctrl}}\land G_{\textit{plant}})$ is valid.

Proof

Adapts [7, Thm. 2] to a syntactic $d\mathcal{L}$ proof with loop invariant $A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}$ with differential refinement to replace $\delta$ with $\Delta$. Prove with loop invariant $A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}$:

Base Case

$\mathcal{E}\land Init_{\textit{ctrl}}\land Init_{\textit{plant}}\land A_{\textit{ctrl}}\land A_{\textit{plant}}\rightarrow G_{\textit{ctrl}}\land G_{\textit{plant}}\land J_{\text{cmp}}$: follows from base cases of the component induction proofs $\mathcal{E}\land Init_{\textit{ctrl}}\land A_{\textit{ctrl}}\rightarrow A_{\textit{ctrl}}\land G_{\textit{ctrl}}$ and $\mathcal{E}\land Init_{\textit{plant}}\land A_{\textit{plant}}\rightarrow A_{\textit{plant}}\land G_{\textit{plant}}$, as well as initially satisfied composition invariant $Init_{\textit{ctrl}}\land Init_{\textit{plant}}\rightarrow J_{\text{cmp}}$.

Use Case

$A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}\rightarrow G_{\textit{ctrl}}\land G_{\textit{plant}}$: trivial.

Induction Step

The induction step unfolds into the following cases (unfolding the non-deterministic choice and the conjuncts of the loop invariant):

1. 1.

$A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}\rightarrow[\textbf{RCtrl}(\textit{ctrl},\delta)](A_{\textit{ctrl}}\land G_{\textit{ctrl}})$: follows from induction step of component proof $G_{\textit{ctrl}}\rightarrow[\textit{ctrl}]G_{\textit{ctrl}}$. 2. 2.

$A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}\rightarrow[\textbf{RCtrl}(\textit{ctrl},\delta)]J_{\text{cmp}}$: follows from composition invariant proof $J_{\text{cmp}}\rightarrow[\textit{ctrl}]J_{\text{cmp}}$. 3. 3.

$A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}\rightarrow[\textbf{RCtrl}(\textit{ctrl},\delta)]G_{\textit{plant}}$: follows from $\text{FV}(G_{\textit{plant}})\cap\text{BV}(\textit{ctrl})=\emptyset$. 4. 4.

$A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}\rightarrow[\textbf{RCtrl}(\textit{ctrl},\delta)]A_{\textit{plant}}$: follows from Case 1+2 with compatibility. 5. 5.

$A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}\rightarrow[\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\delta)]G_{\textit{ctrl}}$: follows from $\text{FV}(G_{\textit{ctrl}})\cap\text{BV}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\})=\emptyset$. 6. 6.

$A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}\rightarrow[\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\delta)](A_{\textit{plant}}\land G_{\textit{plant}})$: follows from differential refinement ($\delta\leq\Delta$) with induction step of component proof $A_{\textit{plant}}\land G_{\textit{plant}}\rightarrow[\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta)](A_{\textit{plant}}\land G_{\textit{plant}})$. 7. 7.

$A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}\rightarrow[\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\delta)]J_{\text{cmp}}$: follows from differential refinement ($\delta\leq\Delta$) with composition invariant proof $J_{\text{cmp}}\rightarrow[\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta)]J_{\text{cmp}}$. 8. 8.

$A_{\textit{ctrl}}\land G_{\textit{ctrl}}\land A_{\textit{plant}}\land G_{\textit{plant}}\land J_{\text{cmp}}\rightarrow[\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\delta)]A_{\textit{ctrl}}$: follows from Case 6+7 with compatibility.

∎

Example 6 (Water-tank contract)

The controller and the water-level are non-interfering, their contracts compatible, and the controller is fast enough to keep the plant safe ($\delta_{\textit{wlctrl}}\leq\Delta_{\textit{wl}}$). We apply Thm. 3.1 with the composition invariant $J_{\text{cmp}}\doteq wl=(\mathit{fin}-\mathit{fout})(t-\tau)+wlm$ to obtain that the composition is safe, *i.e. *formula $\mathcal{E}\land Init_{\textit{wl}}\land Init_{\textit{wlctrl}}\land A_{\textit{wl}}\land A_{\textit{wlctrl}}\rightarrow[\textbf{Water-tank}](G_{\textit{wl}}\land G_{\textit{wlctrl}})$ is valid. The composition invariant says how the true value wl deviates from the last measured value $wlm$ according to the flow $\mathit{fin}-\mathit{fout}$ as time $t-\tau$ passes.

Outlook

We adapted parallel composition of [7] to model and prove computer-controlled systems composed of two components, a reactive controller and a controllable plant. Next, we extend this concept to arbitrarily nested combinations of controllers and plants with a systematic integration of timed constraints.

4 Parallel Composition

We want to extend the integration of temporal considerations for every component in a timed framework. The previous section shows the importance of temporal considerations in CCS. Industrial systems combine CCS in parallel and it is necessary to have a framework to handle temporal properties.

In order to reason about parallel execution of control software sharing computation resources, models of different costs (controllability, performance, latency, etc) become important. For example, when two programs execute quasi-parallel on a single CPU core, their computation resources are shared and execution may mutually preempt. As a result, the worst-case execution times of the programs sum up to the total worst-case execution time of the composed system. This requires designing plants with sufficiently longer controllability periods, and controllers that react further in advance.

Based on the parallel composition pattern in [7] and the concepts of reactive controller and controllable plant introduced above, here we present parallel compositions of component hierarchies, including composition of multiple reactive controllers, multiple controllable plants, and mixed compositions. We retain the algebraic properties of [7], commutativity and associativity, and present theorems guaranteeing that the conjunction of contracts is preserved through composition.

Controllable plants are already hierarchically compositional per Def. 3. The particular structure to enclose control programs with temporal guards in reactive controllers, however, makes it necessary to extend the definition of reactive controller (Def. 2) to a multi-choice reactive controller that combines choices of each of its constituting atomic reactive controllers non-deterministically. We associate a fresh variable $\tau_{i}$ with each atomic reactive controller $\textit{ctrl}_{i}$. It is used to specify the time stamp of the controller in an execution cycle.

Definition 7 (Multi-Choice Reactive Controller)

A multi-choice reactive controller $\textbf{MRCtrl}\left(\bigcup_{1\leq i\leq n}\textit{ctrl}_{i},\delta\right)$ with $n$ control choices and overall reactivity bound $\delta$ has the program shape

[TABLE]

The parallel composition follows cases for purely discrete components, purely continuous components or a mix of both, which we detail in the subsections below. We illustrate each case with an example with two connected water-tanks, one where the inlet flow of one is the outlet flow of the other, with respective reactive controllers to ensure that they remain within a pre-defined range. The first controller actuates on the inlet flow of the first tank, whereas the second actuates on the outlet valve of the second tank.

4.1 Parallel Composition of Multi-Choice Reactive Controllers

We refine the parallel composition operator for multi-choice reactive controllers to considering the controllability and reactivity bounds $\Delta$ and $\delta$ of its components. By definition, the controllability bound of composed components $\alpha$ and $\beta$ is always $\min(\Delta_{\alpha},\Delta_{\beta})$ of their individual bounds $\Delta_{\alpha}$, $\Delta_{\beta}$. The reactivity bound depends on the physical architecture that composes $\alpha$ and $\beta$. It is overapproximated by a max+ cost function ${\mathcal{C}}:\mathbb{R}^{2}\rightarrow\mathbb{R}$ such that ${\mathcal{C}}(\delta_{\alpha},\delta_{\beta})=\max(\delta_{\alpha},\delta_{\beta})$ if $\alpha$ and $\beta$ have controllers running independently (e.g. two ECUs or PLCs), or else $\delta_{\alpha}+\delta_{\beta}$, if both controllers execute on one resource. Notice that such a definition is associative and commutative with respect to composition.

Modeling.

We first define the parallel composition of discrete components, which are multi-choice reactive controllers $\textbf{MRCtrl}(\bigcup_{1\leq i\leq n}\textit{ctrl}_{i},\delta)$. To the definition in [7], we add the cost model ${\mathcal{C}}$ to combine individual bounds $\delta$ as that of the composed system. The parallel composition is the non-deterministic choice between all control choices in multi-choice reactive controllers $\textbf{MRCtrl}(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},\delta_{\alpha})$ and $\textbf{MRCtrl}(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},\delta_{\beta})$, but with the individual $\delta_{\alpha}$ and $\delta_{\beta}$ replaced by the cost model ${\mathcal{C}}(\delta_{\alpha},\delta_{\beta})$. Interleaving of controller executions occurs through embedding the non-deterministic choice in the loop of a full system, see Thm. 4.1.

Definition 8 (Parallel Composition of Multi-Choice Reactive

Controllers)

Let $\alpha$ and $\beta$ be multi-choice reactive controllers with respective program shapes $\textbf{MRCtrl}(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},\delta_{\alpha})$ and $\textbf{MRCtrl}(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},\delta_{\beta})$. The parallel composition $\alpha\ \otimes\ \beta$ has the program shape:

[TABLE]

Example 7 (Composition of two water-level controllers)

We compose two reactive water-level controllers $\textit{wlctrl}_{1}$ (reactivity $\delta_{\textit{wlctrl}_{1}}=0.05$s) and $\textit{wlctrl}_{2}$ (reactivity $\delta_{wlctrl_{2}}=0.02$s) on one CPU. The multi-choice reactive controller resulting from cost model ${\mathcal{C}}(\delta_{\textit{wlctrl}_{1}},\delta_{\textit{wlctrl}_{2}})=\delta_{\textit{wlctrl}_{1}}+\delta_{\textit{wlctrl}_{2}}$ is:

[TABLE]

where $\textit{wlctrl}_{1}$ follows Example 1 and

\textit{wlctrl}_{2}\doteq wlm_{2}\mathrel{{:}{=}}wl;\big{(}{(?wlm_{2}\geq 9.7;\mathit{fout}_{2}\mathrel{{:}{=}}1)}\cup{(?wlm_{2}\leq 2.3;\mathit{fout}_{2}\mathrel{{:}{=}}0)}.

Algebraic properties.

We retain commutativity and associativity of the parallel composition operator defined in [7]. Commutativity implies that we are able to decompose a system and associativity ensures that we can build it step-by-step. The proof relies on the commutativity and associativity of both non-deterministic choice and cost model ${\mathcal{C}}$.

Proposition 1 (Commutativity and Associativity for Parallel Composition of Multi-Choice Reactive Controllers)

Let $\alpha$, $\beta$ and $\gamma$ be multi-choices reactive controllers with respective program shape $\textbf{MRCtrl}\left(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},\delta_{\alpha}\enspace\right)$, $\textbf{MRCtrl}\left(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},\delta_{\beta}\enspace\right)$ and $\textbf{MRCtrl}\left(\bigcup_{1\leq k\leq n_{\gamma}}\gamma_{k},\delta_{\gamma}\enspace\right)$. Assume that the max+ cost function ${\mathcal{C}}$ is commutative and associative. Then:

[TABLE]

Proof

We unfold the definitions and use the commutativity (resp. associativity) property of the non-deterministic choice operator and of the max+ cost function${\mathcal{C}}$.

Commutativity

[TABLE]

Associativity

[TABLE]

∎

Modular verification.

We adapt [7, Thm. 2] by adding the condition that the individual reactivity bound $\delta_{\alpha}$ of a controller $\alpha$ must neither occur in its functional behavior $\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i}$ nor in its guarantees. Failing to do so may prevent to re-use a component proof.

Definition 9 (Non-interfering Controllers)

Two controllers $\alpha$ and $\beta$ are non-interfering if they do not modify the same variables, *i.e. *the outputs are separated ($\text{BV}(\alpha)\cap\text{BV}(\beta)=\emptyset$), and if they do not influence the guarantees of the other component ($\text{FV}(G_{\alpha})\cap\text{BV}(\alpha)=\emptyset$ and $\text{FV}(G_{\beta})\cap\text{BV}(\beta)=\emptyset$).

Theorem 4.1 (Safe composition of Multi-Choice Reactive Controllers)

Let $\alpha$ and $\beta$ be non-interfering multi-choice reactive controllers with program shape $\textbf{MRCtrl}(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},\delta_{\alpha})$ and $\textbf{MRCtrl}(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},\delta_{\beta})$ satisfying their compatible contracts $(A_{\alpha},G_{\alpha})$ and $(A_{\beta},G_{\beta})$ and let $J_{\text{cmp}}$ be a composition invariant. Then the parallel composition $\alpha\ \otimes\ \beta$ is safe, i.e., $(\mathcal{E}\land A_{\alpha}\land Init_{\alpha}\land A_{\beta}\land Init_{\beta})\rightarrow[{(\alpha\ \otimes\ \beta)}^{*}](G_{\alpha}\land G_{\beta})$ is valid.

Proof

Similar to Thm. 3.1 using the additional condition that $\delta_{\alpha}$ (resp. $\delta_{\beta}$) does not appear in the functional behavior $\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i}$ (resp. $\bigcup_{1\leq j\leq n_{\beta}}\beta_{j}$) of the controller, nor in its guarantee $G_{\alpha}$ (resp. $G_{\beta}$). The loop invariant $A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}$. The base case and use case are the same as for Theorem 3.1. The induction step unfolds in the following case:

$A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta}))](A_{\alpha}\land G_{\alpha})$: follows from the condition that $\delta_{\alpha}$ does not occur in the functional behavior $\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i}$, nor in the guarantee $G_{\alpha}$, with induction step of component proof $A_{\alpha}\land G_{\alpha}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},\delta_{\alpha})](A_{\alpha}\land G_{\alpha})$. 2. 2.

$A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta}))]J_{\text{cmp}}$: follows from the condition that $\delta_{\alpha}$ does not occur in the functional behavior $\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i}$, nor in the formula $J_{\text{cmp}}$, with composition invariant proof $J_{\text{cmp}}\rightarrow[\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i}]J_{\text{cmp}}$. 3. 3.

$A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta}))]G_{\beta}$: follows from $\text{FV}(G_{\beta})\cap\text{BV}(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i})=\emptyset$. 4. 4.

$A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq i\leq n_{\alpha}}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta}))]A_{\beta}$: follows from Case 1+2 with compatibility. 5. 5.

$A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta}))]G_{\alpha}$: follows from $\text{FV}(G_{\alpha})\cap\text{BV}(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j})=\emptyset$. 6. 6.

$A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta}))](A_{\beta}\land G_{\beta})$: follows from the condition that $\delta_{\beta}$ does not occur in the functional behavior $\bigcup_{1\leq j\leq n_{\beta}}\beta_{j}$, nor in the guarantee $G_{\beta}$ with induction step of component proof $A_{\beta}\land G_{\beta}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},\delta_{\beta})](A_{\beta}\land G_{\beta})$. 7. 7.

$A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta}))]J_{\text{cmp}}$: follows from the condition that $\delta_{\beta}$ does not occur in the functional behavior $\bigcup_{1\leq j\leq n_{\beta}}\beta_{j}$, nor in the formula $J_{\text{cmp}}$, with composition invariant proof $J_{\text{cmp}}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},\delta_{\beta})]J_{\text{cmp}}$. 8. 8.

$A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}\rightarrow[\textbf{MRCtrl}(\bigcup_{1\leq j\leq n_{\beta}}\beta_{j},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta}))]A_{\alpha}$: follows from Case 6+7 with compatibility.

∎

Non-interference of controllers and compatibility of contracts are standard requirements when modeling a system compositionally and safely.

Example 8 (Safe composition of two water-level controllers)

The contract of the first reactive controller $\textit{wlctrl}_{1}$ is the same as in Example 5 with necessary changes. The contract for the second controller is :

[TABLE]

The controller actuates the outlet valve of the system ($\mathit{fout}_{2}$). It opens it when the real water-level of the second tank is too close to the maximum threshold ($10$ here) to drain the tank and close it to fill the tank if too close to the minimum threshold ($2$). The two controllers are non-interfering, the contracts are compatible and they both satisfy their contracts (verified using the proof calculus of $d\mathcal{L}$). Hence, Thm. 4.1 guarantees that the parallel composition is safe, *i.e. *that the contract $(A_{\textit{wlctrl}_{1}}\land A_{\textit{wlctrl}_{2}},G_{\textit{wlctrl}_{1}}\land G_{\textit{wlctrl}_{2}})$ is valid.

4.2 Parallel Composition of Controllable Plants

When composing two continuous components in parallel, the controllability of the resulting system is the minimum of their individual controllability bounds (which is obvious from the semantics of ODEs listed in Tab. 1: safety proofs hold for any non-negative duration, so also for smaller durations).

Modeling

Non-interference of controllable plants ensures that their combined continuous dynamics stays true to the isolated dynamics, and that they do not interfere with the guarantees of the respective other component.

Definition 10 (Non-interfering Plants)

Two controllable plants $\alpha$ and $\beta$ with $\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta_{\alpha})$ and $\textbf{CPlant}(\{y^{\prime}=\eta\ \mathbin{\&}\ Q\},\Delta_{\beta})$ and contracts $(A_{\alpha},G_{\alpha})$ and $(A_{\beta},G_{\beta})$ are non-interfering if $\text{BV}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\})\cap\text{FV}(\eta)=\emptyset$ and $\text{BV}(\{y^{\prime}=\eta\ \mathbin{\&}\ Q\})\cap\text{FV}(\theta)=\emptyset$, and if $\text{BV}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\})\cap\text{FV}(G_{\beta})=\emptyset$ and $\text{BV}(\{y^{\prime}=\eta\ \mathbin{\&}\ Q\})\cap\text{FV}(G_{\alpha})=\emptyset$.

Note that non-interference implies $\text{BV}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\})\cap\text{BV}(\{y^{\prime}=\eta\ \mathbin{\&}\ Q\})=\emptyset$.

Definition 11 (Parallel Composition of Controllable Plants)

Let $\alpha$ and $\beta$ be non-interfering controllable plants $\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta_{\alpha})$ and$\textbf{CPlant}(\{y^{\prime}=\eta\ \mathbin{\&}\ Q\},\Delta_{\beta})$. The parallel composition $\alpha\ \otimes\ \beta$ is an ODE system of the shape \begin{array}[]{l}\textbf{CPlant}(\{x^{\prime}=\theta,y^{\prime}=\eta\ \mathbin{\&}\ H\wedge Q\},min(\Delta_{\alpha},\Delta_{\beta}))\enspace.\end{array}

Example 9 (Composition of two water-level)

Here, we compose the water level dynamics of two tanks ($\{wl_{1}^{\prime}=\mathit{fin}-\mathit{fout}_{1},t^{\prime}=1\ \mathbin{\&}\ \textit{wl}_{1}\geq 0\wedge t\leq\Delta_{\textit{wl}_{1}}\}$ and $\{wl_{2}^{\prime}=\mathit{fout}_{1}-\mathit{fout}_{2},t^{\prime}=1\ \mathbin{\&}\ \textit{wl}_{2}\geq 0\wedge\Delta_{\textit{wl}_{2}}\}$) to obtain a controllable plant modeling the evolution of both water levels simultaneously. Their respective controllability bounds are $\Delta_{\textit{wl}_{1}}=0.2s$ and $\Delta_{\textit{wl}_{2}}=0.15s$. The controllable plant resulting from the parallel composition expands to

[TABLE]

Algebraic properties.

Commutativity and associativity of the parallel composition pattern defined in [7] are preserved. The proof follows from commutativity and associativity of “,” in ODEs and of operator $\min$.

Proposition 2 (Commutativity and Associativity for Parallel Composition of Controllable Plants)

Let $\alpha$, $\beta$ and $\gamma$ non-interfering controllable plants $\textbf{CPlant}(\{x^{\prime}=\theta_{x}\ \mathbin{\&}\ H_{x}\},\Delta_{\alpha})$, $\textbf{CPlant}(\{y^{\prime}=\theta_{y}\ \mathbin{\&}\ H_{y}\},\Delta_{\beta})$ and $\textbf{CPlant}(\{z^{\prime}=\theta_{z}\ \mathbin{\&}\ H_{z}\},\Delta_{\gamma})$. Then:

[TABLE]

Proof

We unfold the definitions, use the commutativity (resp. associativity) property of the minimum operator $min(\cdot,\cdot)$, of the conjunction $\wedge$ (for the evolution domain formulas) and of “,” in ODEs.

Commutativity

[TABLE]

Associativity

[TABLE]

∎

Modular verification.

The conjunction of contracts is retained for parallel composition of continuous components, similar to parallel composition of controllers.

Theorem 4.2 (Safe Composition of Controllable Plants)

Let $\alpha$ and $\beta$ be two non-interfering controllable plants $\textbf{CPlant}(\{x^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta_{\alpha})$ and $\textbf{CPlant}(\{y^{\prime}=\eta\ \mathbin{\&}\ Q\},\Delta_{\beta})$ satisfying their respective compatible contracts $(A_{\alpha},G_{\alpha})$ and $(A_{\beta},G_{\beta})$, and let $J_{\text{cmp}}$ be a composition invariant. Then the parallel composition $\alpha\ \otimes\ \beta$ is safe, i.e., $(\mathcal{E}\land A_{\alpha}\land Init_{\alpha}\land A_{\beta}\land Init_{\beta})\rightarrow[{(\alpha\ \otimes\ \beta)}^{*}](G_{\alpha}\land G_{\beta})$ is valid.

Proof

Similar to Theorem 3.1 after separating the non-interfering plants using the right-to-left direction of the differential ghost axiom (DG) [12].

[TABLE]

$A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}\rightarrow[\textbf{CPlant}(\{x^{\prime}=\theta_{x},y^{\prime}=\theta_{y}\ \mathbin{\&}\ H_{x}\wedge H_{y}\},min(\Delta_{\alpha},\Delta_{\beta})](A_{\alpha}\land G_{\alpha})$: follows from component’s proof $A_{\alpha}\land G_{\alpha}\land A_{\beta}\land G_{\beta}\land J_{\text{cmp}}\rightarrow[\textbf{CPlant}(\{x^{\prime}=\theta_{x}\ \mathbin{\&}\ H_{x}\wedge H_{y}\},min(\Delta_{\alpha},\Delta_{\beta})](A_{\alpha}\land G_{\alpha})$ using the the differential ghost axiom right-to-left since the plants are non-interfering. ∎

Example 10 (Safe composition of two water-level)

The contract for the first water level is the same as in Example 5 with necessary changes. We guarantee that the water level of the second tank is within $2$ and $10$, provided that there is a controller which reacts appropriately. Its contract is:

[TABLE]

We apply Thm. 4.2 to guarantee that the controllable plant modeling the evolution of water levels in distinct connected tanks is safe, *i.e. *it satisfies the contract $(A{\textit{wl}_{1}}\land A_{\textit{wl}_{2}},G_{\textit{wl}_{1}}\land G_{\textit{wl}_{2}})$.

4.3 Parallel Composition of Multi-Choice Reactive Controllers and Controllable Plants

We present the composition of a multi-choice reactive controller with a controllable plant that may result from the composition of several atomic controllable plants. We lift the definition of CCS (Sec. 3) to a general integration of controllability and reactivity.

Modeling

We define a multi computer-controlled system MCCS as the parallel composition of a multi-choice reactive controller with a controllable plant.

Definition 12 (Multi Computer-Controlled System)

A multi computer-controlled system is a parallel composition of a multi-choice reactive controller $\textbf{MRCtrl}(\bigcup_{1\leq i\leq n}\textit{ctrl}_{i},\delta)$ and a controllable plant $\textbf{CPlant}(\{y^{\prime}=\theta\ \mathbin{\&}\ H\},\Delta)$. The parallel composition MCCS has the hybrid program shape:

[TABLE]

The formula $\bigwedge_{1\leq i\leq n}t\leq\tau_{i}+\delta$ is the conjunction of the reactivity bounds of all the $n$ sub-controllers $\textit{ctrl}_{i}$.

Modular verification

Cor. 1 lifts Thm. 3.1 (for a single controller and a single plant) to multi computer-controlled systems of possibly many controllers with a controllable plant representing multiple simultaneous evolutions.

Corollary 1 (Safe Composition of Multi-Choice Reactive Controller and Controllable Plant)

Let $\textbf{MRCtrl}(\bigcup_{1\leq i\leq n}\textit{ctrl}_{i},\delta)$ be a multi-choice reactive controller non-interfering with the controllable plant $\textbf{CPlant}(\{y^{\prime}=\theta_{y}\ \mathbin{\&}\ H_{y}\},\Delta)$ satisfying their compatible contracts $(A_{\textit{ctrl}},G_{\textit{ctrl}})$ and $(A_{\textit{plant}},G_{\textit{plant}})$. Further let $J_{\text{cmp}}$ be a composition invariant. Then, MCCS is safe, i.e., $(\mathcal{E}\land A_{\textit{ctrl}}\land Init_{\textit{ctrl}}\land A_{\textit{plant}}\land Init_{\textit{plant}})\rightarrow[\textbf{MCCS}](G_{\textit{ctrl}}\land G_{\textit{plant}})$ is valid.

Proof

Similar to the proof of Thm. 3.1, but with multi-choice reactive controller instead of a single reactive controller. ∎

4.4 Parallel Composition of Multi Computer-Controlled Systems

When composing multi computer-controlled systems, the combined reactivity of all controllers must not exceed the combined (minimum) controllability bounds of the plants. Otherwise, safety cannot be guaranteed, as elaborated next.

Modeling

The parallel composition of two multi computer-controlled systems is similar to the composition of a multi-choice reactive controller with a controllable plant to obtain a multi computer-controlled system MCCS, but with extra care for the combined reactivity bounds obtained from the physical cost model ${\mathcal{C}}$.

Definition 13 (Parallel Composition of Multi Computer-Controlled

Systems)

Let $\alpha$ and $\beta$ be two multi computer-controlled systems with shapes \alpha\doteq\big{(}\{x^{\prime}=\theta,t^{\prime}=1\ \mathbin{\&}\ H\wedge\bigwedge_{1\leq i\leq n}t\leq\tau_{i}+\delta_{\alpha}\}\cup\textbf{MRCtrl}(\bigcup_{1\leq i\leq n}\alpha_{i},\delta_{\alpha})\big{)}^{\ast}, \beta\doteq\big{(}\{y^{\prime}=\eta,t^{\prime}=1\ \mathbin{\&}\ Q\wedge\bigwedge_{1\leq j\leq m}t\leq\tau_{j}+\delta_{\beta}\}\cup\textbf{MRCtrl}(\bigcup_{1\leq j\leq m}\beta_{j},\delta_{\beta})\big{)}^{\ast}. The parallel composition $\alpha\ \otimes\ \beta$ has the hybrid program shape:

[TABLE]

Algebraic properties

We retain the commutativity and associativity properties (under the condition that the provided max+ cost function ${\mathcal{C}}$ is commutative and associative), essential for a modular component-based approach.

Proposition 3 (Commutativity and Associativity for Parallel Composition of Multi Computer-Controlled Systems)

Let $\alpha$, $\beta$ and $\gamma$ be multi computer-controlled systems with respective hybrid program shape

[TABLE]

*Then: *

[TABLE]

Proof

We unfold definitions and apply Propositions 1 and 2 to inner multi-choice reactive controllers and controllable plants.

Commutativity

[TABLE]

Associativity

[TABLE]

∎

Modular verification

We retain also the respective contracts through the parallel composition. We assume that the individual reactivity bound $\delta_{\alpha}$ of the controller must not occur in its functional behavior, nor in its guarantees.

Theorem 4.3 (Safe composition of Multi Computer-Controlled Systems)

Let $\alpha$ and $\beta$ be non-interfering multi computer-controlled systems (with program shape $\textbf{MCCS}_{\alpha}$ and $\textbf{MCCS}_{\beta}$) satisfying their respective compatible contracts $(A_{\alpha},G_{\alpha})$ and $(A_{\beta},G_{\beta})$, and let $J_{\text{cmp}}$ be a composition invariant. Then the parallel composition $\alpha\ \otimes\ \beta$ is safe, i.e., $(\mathcal{E}\land A_{\alpha}\land Init_{\alpha}\land A_{\beta}\land Init_{\beta})\rightarrow[\alpha\ \otimes\ \beta](G_{\alpha}\land G_{\beta})$ is valid.

Proof

The parallel composition of two multi computer-controlled systems $\alpha$ and $\beta$ with hybrid program shape \textbf{MCCS}_{\alpha}\doteq\{x^{\prime}=\theta_{x},t^{\prime}=1\ \mathbin{\&}\ H_{x}\wedge\bigwedge_{1\leq i\leq n}t\leq\tau_{i}+\delta_{\alpha}\}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n}\alpha_{i},\delta_{\alpha}\big{)} and \textbf{MCCS}_{\beta}\doteq\{y^{\prime}=\theta_{y},t^{\prime}=1\ \mathbin{\&}\ H_{y}\wedge\bigwedge_{1\leq j\leq m}t\leq\tau_{j}+\delta_{\beta}\}\cup\textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq m}\beta_{j},\delta_{\beta}\big{)} has the hybrid program shape:

[TABLE]

The parallel composition of respective inner multi-choice reactive controllers \textbf{MRCtrl}\big{(}\bigcup_{1\leq i\leq n}\alpha_{i},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\big{)} and \textbf{MRCtrl}\big{(}\bigcup_{1\leq j\leq m}\beta_{j},{\mathcal{C}}(\delta_{\alpha},\delta_{\beta})\big{)} results in the multi-choice reactive controller:

[TABLE]

The parallel composition of inner controllable plants results in the controllable plant:

[TABLE]

Composing the multi-choice reactive controller with the controllable plant following Def. 12 yields:

[TABLE]

We successively apply Theorem 4.1 to the group of inner controllers, Theorem 4.2 to the global controllable plant and Cor. 1 to the composition of both to conclude. ∎

Outlook

In this section, we have presented how to extend our previous component-based approach to take into account the timing constraints inherent to the design of a Computer-Controlled System. We have proved that we retain the commutativity and associativity, essential to scale up to realistic systems. Finally, we state and prove theorems to retain contracts through the parallel composition. Theses results give us confidence in the ability of our approach to be adapted to new challenges that will arise when applied to realistic industrial systems.

5 Related Work

Recent component-based verification techniques [9, 10] proposed a composition operator in $d\mathcal{L}$ based on the modeling pattern ${(\textit{ctrl};\textit{plant})}^{*}$ to split verification of systems into more manageable pieces. It focus on separating self-contained components (a controller monitoring its own plant) instead of separating discrete and continuous fragments. Morevoer, our approach integrates a max+ cost function which handles timing relations upon composition.

Hybrid automata [1] are a popular formalism to model hybrid systems, but composition of automata results in an exponential product automaton which is intractable to analyze in practice. I/O hybrid automata [8] is an extension of hybrid automata with explicit inputs and outputs. Assume-guarantee reasoning [4] on such automata tackles composability to prevent state-space explosion. Yet, use is in practice restricted to linear hybrid automata. Differential Dynamic Logic is practically used for systems with ODEs (and not just linear ODEs), thus our approach is more expressive.

Hybrid Communicating Sequential Processes (HCSP) [5] is a hybrid extension of the CSP framework. It features a native parallel composition operator and communicating primitives in addition to standard constructs for hybrid systems (sequences, loops, ODEs) and a proof calculus has been proposed in [6]. In contrast, our parallel composition operator is not native and relies on usual constructs of $d\mathcal{L}$. The benefit is that we do not have to extend $d\mathcal{L}$ and check the soundness of such extension, but it requires additional effort to mechanize it into the theorem prover KeYmaera X. Also, our approach provide engineering support for timing aspects and modular verification principles.

This paper is an extension of our previous work, with specific features to handle temporal properties of the parallel composition of CCS and syntactic proofs that facilitate implementation of the proposed techniques as tactics in the theorem prover KeYmaera X.

6 Conclusion

We presented a component-based verification technique to modularly design and verify computer-controlled systems with special focus on timing constraints (reactivity and controllability) and modular verification. Our concepts enable systematic modeling of CCS in a modular way while maintaining algebraic properties of composition operators and preserving contract proofs through composition. We additionally support reasoning on non-functional properties (reactivity, controllability) through multiple compositions of reactive controllers and plants. This paves the way to ultimately model complex cyber-physical systems (several controllers running in parallel according to a generic max+ cost function that monitor different plants) from only simple, atomic components. Verification of safety properties for the global system reduces to component safety proofs with only mild assumptions on the reactivity of controllers (does not exceed the controllability of plants) and compatibility between contracts.

As future work, we intend to allow more aggressive compositions to lift restrictions of the techniques presented here: allow some interference in the parallel composition of controllable plants and reactive controllers with additional compatibility proofs (lift non-interference restriction of Cor. 1); allow time and reactivity in the predictions and guarantees of controllers with refactoring techniques to strengthen control choices upon composition (lift restriction of Thm. 4.3 that controllers are not allowed to exploit their reactivity bounds $\delta$ for control decisions); and support fine-grained communication going beyond shared variables with communication channels as in Hybrid Communicating Sequential Processes. For proof automation, we intend to implement the theorems of this paper as tactics in the KeYmaera X theorem prover.