## Formal Analysis of Linear Control Systems using Theorem Proving
Adnan Rashid and Osman Hasan
School of Electrical Engineering and Computer Science (SEECS) National University of Sciences and Technology (NUST) Islamabad, Pakistan
{adnan.rashid,osman.hasan}@seecs.nust.edu.pk
Abstract. Control systems are an integral part of almost every engineering and physical system and thus their accurate analysis is of utmost importance. Traditionally, control systems are analyzed using paper-andpencil proof and computer simulation methods, however, both of these methods cannot provide accurate analysis due to their inherent limitations. Model checking has been widely used to analyze control systems but the continuous nature of their environment and physical components cannot be truly captured by a state-transition system in this technique. To overcome these limitations, we propose to use higher-order-logic theorem proving for analyzing linear control systems based on a formalized theory of the Laplace transform method. For this purpose, we have formalized the foundations of linear control system analysis in higherorder logic so that a linear control system can be readily modeled and analyzed. The paper presents a new formalization of the Laplace transform and the formal verification of its properties that are frequently used in the transfer function based analysis to judge the frequency response, gain margin and phase margin, and stability of a linear control system. We also formalize the active realizations of various controllers, like Proportional-Integral-Derivative (PID), Proportional-Integral (PI), Proportional-Derivative (PD), and various active and passive compensators, like lead, lag and lag-lead. For illustration, we present a formal analysis of an unmanned free-swimming submersible vehicle using the HOL Light theorem prover.
Keywords: Control Systems, Higher-order Logic, Theorem Proving
## 1 Introduction
Linear control systems are widely used to regulate the behavior of many safetycritical applications, such as process control, aerospace, robotics and transportation. The first step in the analysis of a linear control system is the construction of its equivalent mathematical model by using the physical and engineering laws. For example, in the case of electrical systems, we need to model the currents and voltages passing through the electrical components and their interactions in the
## 2 A. Rashid and O. Hasan
corresponding electrical circuit using the system governing laws, such as Kirchhoff's current law (KCL) and Kirchhoff's voltage law (KVL). The mathematical model is then used to derive differential equations describing the relationship between the inputs and outputs of the underlying system. The next step in the analysis of a linear control system is to solve these equations to obtain a transfer function, which is in turn used to assess many interesting control system characteristics, such as frequency response, phase margin and gain margin. However, solving these equations in the time domain is not so straightforward as they usually involve the integral and differential operators. The Laplace transform, which is an integral based transform method, is thus often used to convert these differential equations to their equivalent algebraic equations in s -domain by converting the differential and integral operations into multiplication and division operators, respectively. This algebraic equation can be quite easily solved to obtain the corresponding transfer function, frequency response, gain margin and the phase margin and perform the stability analysis of the given control system.
Traditionally, the linear control system analysis is performed using paperand-pencil proof methods. However, these methods are human-error prone and cannot be relied upon for the analysis of safety-critical applications. Moreover, there is always a risk of misusing an existing mathematical result as this manual analysis method does not provide the assurance that a mathematical law would be used only if all of its required assumptions are valid. Computer simulation and numerical methods are also frequently used to analyze linear control systems. However, they also compromise the accuracy of the results due to the involvement of computer arithmetic and the associated round-off errors. Computer algebra systems (CAS), such as Mathematica [14], are also used for the Laplace transform based analysis of linear control systems. However, CAS are primarily based on unverified symbolic algorithms and thus there is no formal proof to ascertain the accuracy of their analysis results. Given the inaccurate nature of all the abovementioned analysis techniques, they are not very suitable to analyze control systems used in safety-critical domains, where even a slight error in analysis may lead to disastrous consequences, including the loss of human lives.
To overcome the above-mentioned limitations, model checking [11] has been also used to analyze control systems [12,22] but the continuous nature of their environment and physical components cannot be truly captured by a statetransition system in this technique. Similarly, a Hoare logic based framework [6] and the KeYmaera tool [2] have been used for the formal frequency domain analysis and verification of the safety properties of control systems with sampled-time controllers, respectively. However, the former is limited to the analysis of systems that can be expressed using a block diagram with a tree structure, whereas in the later, the continuous nature of the models is abstracted in the formal modeling process and hence the completeness of the analysis is compromised in both cases.
Recently, the HOL Light theorem prover has been used for the formal analysis of control systems. Hasan et al. presented a formalization of the block diagrams in HOL Light and used it to reason about the transfer function and the steady-
state error analysis of a feedback control system [10]. Ahmed et al. used this formalization of block diagrams to verify the steady-state error of a unity feedback control system [1]. Similarly, Beillahi et al. formalized the signal flow graphs in HOL Light, which can be used to formally verify transfer functions of linear control systems [5]. However, all these existing works focus on the verification of the transfer functions for a control system and, to the best of our knowledge, no prior work dealing with the formal analysis of dynamics of a linear control system exists in the literature of higher-order-logic theorem proving.
In this paper, we present a framework to conduct the formal analysis of dynamical characteristics of a linear control system using higher-order-logic theorem proving. The main idea behind the proposed framework, depicted in Fig. 1, is to formalize all the foundational components of a linear control system to facilitate formal modeling and reasoning about linear control systems within the sound core of a theorem prover. For this purpose, we built upon the higherorder-logic formalizations of Multivariable calculus [9] and a library of analog components, like resistor, capacitor and inductor [21]. We present a new formalization of Laplace transform , which includes the formal verification of some of its frequently used properties in reasoning about the transfer function of an n -order system. We also formalized some widely used characteristics of linear control systems , such as frequency response, gain margin and phase margin, which can be used for the stability analysis of a linear control system. Moreover, we formalize the active realizations of various controllers , such as ProportionalIntegral-Derivative (PID), Proportional-Integral (PI), Proportional-Derivative (PD), Proportional (P), Integral (I) and Derivative (D) and various active and passive compensators , such as lag, lead and lag-lead.
The proposed framework, depicted in Fig. 1, allows us to build a formal model of the given linear control system, based on the active realizations of its
Fig. 1: Proposed Framework
<details>
<summary>Image 1 Details</summary>
### Visual Description
\n
## Diagram: Control Systems and Higher-order Logic Relationship
### Overview
The image is a diagram illustrating the relationship between Control Systems and Higher-order Logic. It depicts a flow of information and dependencies between various components within these two domains, culminating in a formal verification process using the HOL Light Theorem Prover. The diagram is structured with a header representing Control Systems, a central block representing the core of Control Systems, and a left-side block representing Higher-order Logic. Arrows indicate the flow of information and dependencies.
### Components/Axes
The diagram consists of the following components:
* **Header (Gray):** "Control Systems" with sub-components: "Controllers", "Compensators", "Properties", "Differential Equation", "Transfer Function".
* **Higher-order Logic (Light Blue):** "Higher-order Logic" with sub-components: "Analog Library", "Multivariate Calculus", "Laplace Transform".
* **Central Control Systems Block (Light Green):** "Control Systems" with sub-components: "PID, PD, PI, P, I, D", "Lag, Lead, Lag-lead", "Gain Margin, Phase Margin, Frequency Response".
* **Formal Model (Purple):** "Formal Model".
* **HOL Light Theorem Prover (Dark Green):** "HOL Light Theorem Prover".
Arrows connect these components, indicating dependencies and information flow.
### Detailed Analysis or Content Details
The diagram shows the following connections:
1. **Header to Central Block:**
* "Controllers" connects to "PID, PD, PI, P, I, D".
* "Compensators" connects to "Lag, Lead, Lag-lead".
* "Properties" connects to "Gain Margin, Phase Margin, Frequency Response" and "Properties" (in the lower right).
* "Differential Equation" connects to "Differential Equation" (in the lower right).
* "Transfer Function" connects to "Transfer Function" (in the lower right).
2. **Higher-order Logic to Central Block:**
* "Analog Library" connects to "PID, PD, PI, P, I, D".
* "Multivariate Calculus" connects to "Gain Margin, Phase Margin, Frequency Response".
* "Laplace Transform" connects to "Transfer Function".
3. **Central Block to Formal Model:**
* "PID, PD, PI, P, I, D" connects to "Formal Model".
* "Gain Margin, Phase Margin, Frequency Response" connects to "Formal Model".
* "Differential Equation" connects to "Formal Model".
* "Transfer Function" connects to "Formal Model".
* "Properties" connects to "Formal Model".
4. **Formal Model to HOL Light Theorem Prover:**
* "Formal Model" connects to "HOL Light Theorem Prover".
5. **Higher-order Logic to HOL Light Theorem Prover:**
* "Analog Library" connects to "HOL Light Theorem Prover".
* "Multivariate Calculus" connects to "HOL Light Theorem Prover".
* "Laplace Transform" connects to "HOL Light Theorem Prover".
### Key Observations
The diagram highlights the integration of mathematical and analytical tools (Higher-order Logic) with practical control system design elements. The "Formal Model" acts as a bridge between the Control Systems components and the rigorous verification provided by the "HOL Light Theorem Prover". The diagram suggests a workflow where control system properties and designs are formally modeled and then verified for correctness and robustness.
### Interpretation
This diagram illustrates a methodology for formally verifying control systems. It demonstrates how concepts from higher-order logic, such as analog libraries, multivariate calculus, and Laplace transforms, are used to create a formal model of the control system. This formal model, encompassing elements like PID controllers, transfer functions, and properties like gain and phase margins, is then subjected to rigorous verification using the HOL Light Theorem Prover.
The diagram suggests a shift towards more reliable and trustworthy control systems by employing formal methods. The use of the HOL Light Theorem Prover implies a desire for mathematical proof of correctness, rather than relying solely on simulation and testing. This approach is particularly valuable in safety-critical applications where failures can have severe consequences. The diagram emphasizes the importance of a solid mathematical foundation for control system design and implementation. The connections between the higher-order logic components and the control system components suggest that the mathematical tools are used to analyze and model the behavior of the control system.
</details>
controllers and compensators, the passive realizations of compensators and differential equations. Moreover, it also allows to formalize the behavior of the
given linear control system in terms of its differential equation, transfer function specification and its properties, such as phase margin, frequency response and gain margin. We can then use these formalized models and properties to verify an implication relationship between them, i.e., model implies its specification. In order to demonstrate the effectiveness of our proposed formalization, we formalize the control system of an unmanned free-swimming submersible vehicle [15]. We have used the HOL Light theorem prover [8] for the proposed formalization in order to build upon its multivariable calculus theories. We have also developed a tactic that can be used to automatically verify the transfer function of any control system up to 20 th order . This tactic was found to be very handy in the formal analysis of the unmanned submersible vehicle.
## 2 Multivariable Calculus Theories in HOL Light
An N-dimensional vector is formalized in the multivariable theory of HOL Light as a R N column matrix of real numbers [9]. All of the multivariable calculus theorems are verified for functions with an arbitrary data-type R N β R M .
A complex number is defined as a 2-dimensional vector, i.e., a R 2 matrix.
```
Definition 1. |- \a. Cx a = complex (a, &0)
|- ii = complex (&0, &1)
```
Cx : R β R 2 is a type casting function that accepts a real number and returns its corresponding complex number with the imaginary part equal to zero, where the & operator type casts a natural number to its corresponding real number. Similarly, ii (iota) represents a complex number having the real part equal to zero and the magnitude of the imaginary part equal to 1.
```
Definition 2. |- \z. Re z = z$1
```
The function Re accepts a complex number (2-dimensional vector) and returns its real part. Here, the notation z $ i represents the i th component of vector z . Similarly, Im takes a complex number and returns its imaginary part. The function lift accepts a variable of type R and maps it to a 1-dimensional vector with the input variable as its single component. Similarly, drop takes a 1-dimensional vector and returns its single element as a real number.
```
Definition 3. |- \x. exp x = Re (cexp (Cx x))
```
The complex exponential and real exponentials are represented as cexp : R 2 β R 2 and exp : R β R in HOL Light, respectively.
```
Definition 4. - \forall f i. integral i f = (@y. (f has integral y) i)
\verbatim
\f a f i. real integral i f = (@y. (f has real integral y) i)
```
The function integral represents the vector integral and is defined using the Hilbert choice operator @ in the functional form. It takes the integrand function f , having an arbitrary type R N β R M , and a vector-space i : R N β B , which defines the region of convergence as B represents the boolean data type, and returns a vector R M , which is the integral of f on i . The function has integral represents the same relationship in the relational form. Similarly, the function real integral accepts the integrand function f : R β R and a set of real numbers i : R β B and returns the real-valued integral of function f over i . The region of integration, for both of the above integrals can be defined to be bounded by a vector interval [ a, b ] or real interval [ a, b ] using the HOL Light functions interval [ a , b ] and real interval [ a , b ], respectively.
## Definition 5.
β f net. vector derivative f net = (@f'.(f has vector derivative f') net)
The function vector derivative takes a function f : R 1 β R M and a net : R 1 β B , which defines the point at which f has to be differentiated, and returns a vector of data-type R M , which represents the differential of f at net . The function has vector derivative defines this relationship in the relational form.
$$D e f n i t i o n 6 . \, \vdash \forall f \, n e t . \, l i m \, n e t \, f = ( \mathbb { O } _ { 1 } . \, ( f \to 1 ) \, n e t )$$
The function lim accepts a net with elements of arbitrary data-type A and a function f : A β R M and returns l of data-type R M , i.e., the value to which f converges at the given net .
## 3 Formalization of Laplace Transform
Mathematically, Laplace transform is defined for a function f : R 1 β C as [4]:
$$\mathcal { L } [ f ( t ) ] = F ( s ) = \int _ { 0 } ^ { \infty } f ( t ) e ^ { - s t } d t , \, s \epsilon \, \mathbb { C } & & ( 1 )$$
We formalize Equation 1 in HOL Light as follows:
$$\text {Definition 7.} \, \vdash \forall s f . l a p l a c e t r a n s t o r f i s = \\ \text {integral } \{ t | \& 0 \leq d r o p \} ( \lambda t . c x p \left ( - ( s * C x \, ( d r o p \, t ) ) \right ) * f \, t )$$
The function laplace transform accepts a complex-valued function f : R 1 β R 2 and a complex number s and returns the Laplace transform of f as represented by Equation 1. In the above definition, we used the complex exponential function cexp : R 2 β R 2 because the return data-type of the function f is R 2 . Here, the data-type of t is R 1 and to multiply it with the complex number s , it is first converted into a real number by using drop and then it is converted to data-type R 2 using Cx . Next, we use the vector function integral (Definition 4) to integrate the expression f ( t ) e -iΟt over the positive real line since the datatype of this expression is R 2 . The region of integration is { t | &0 <= drop t } , which represents the positive real line. Laplace transform was earlier formalized using a limiting process as [20]:
```
|- \s f. laplace f s = lim at posinfinity (\b. integral
(interval [lift (&0), lift b]) (\t. cexp (--(s * Cx (drop t))) * f t))
```
However, the HOL Light definition of the integral function implicitly encompasses infinite limits of integration. So, our definition covers the region of integration, i.e., [0 , β ), as { t | &0 <= drop t } and is equivalent to the definition given in [20]. However, our definition considerably simplifies the reasoning process in the verification of Laplace transform properties since it does not involve the notion of limit.
The Laplace transform of a function f exists, if f is piecewise smooth and is of exponential order on the positive real line [4,19]. A function is said to be piecewise smooth on an interval if it is piecewise differentiable on that interval.
```
Definition 8. + \s f. laplace exists f s <=>
( \b . f piecewise differentiable on interval [lift (&0),lift b] ) ^
( \m a. Re s > drop a \^ exp order cond f M a)
```
The function exp order cond in the above definition represents the exponential order condition necessary for the existence of the Laplace transform [20,4]:
```
Definition 9. |- \f M a. exp order f M a <=> &0 < M ^ { * } \\ ( \forall t . &0 <= t \Rightarrow n o r m ( f ( l i f t ) ) \leq M * \exp ( d r o p a * t ) )
```
We used Definitions 7, 8 and 9 to formally verify some of the classical properties of Laplace transform, given in Table 1. The properties namely linearity, frequency shifting, differentiation and integration were already verified using the formal definition of the Laplace transform [20]. We formally verified these using our new definition of the Laplace transform. Moreover, we formally verified some new properties, such as, time shifting, time scaling, cosine and sine-based modulations and the Laplace transform of a n -order differential equation. The assumptions of these theorems describe the existence of the corresponding Laplace transforms. For example, the predicate laplace exists higher deriv in the theorem corresponding to the n -order differential equation ensures that the La-
Table 1: Properties of Laplace Transform
| Property | Formalized Form |
|---------------------------------------------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| Integrability e - st f ( t ) integrable on [0 , β ) | β f s. laplace exists f s β ( Ξ» t. cexp (--(s β Cx (drop t))) β f t) integrable on { t | &0 <= drop t } |
| Linearity L [ Ξ±f ( t )+ Ξ²g ( t )] = Ξ±F ( s )+ Ξ²G ( s ) | β f g s a b. laplace exists f s β§ laplace exists g s β laplace transform ( Ξ» t. a β f t + b β g t) s a β laplace transform f s + b β laplace transform g s |
| Frequency Shifting L [ e s 0 t f ( t )] = F ( s - s 0 ) | β f s s0. laplace exists f s β laplace transform ( Ξ» t. cexp (s0 β Cx (drop t)) β f t) s = laplace transform f (s - s0) |
<details>
<summary>Image 2 Details</summary>
### Visual Description
\n
## Mathematical Formulas: Laplace Transforms and Differentiation/Integration
### Overview
The image presents a collection of mathematical formulas related to Laplace transforms, differentiation, integration, time shifting, time scaling, cosine-based modulation, and sinusoidal modulation. The formulas demonstrate how these operations in the time domain translate to the Laplace domain (s-domain). The formulas are written in a symbolic mathematical notation, likely using LaTeX or a similar typesetting language.
### Components/Axes
There are no axes or traditional chart components. The image consists entirely of mathematical equations. Each equation is a self-contained statement. The equations are arranged vertically, with each representing a different transformation or property.
### Detailed Analysis or Content Details
Here's a transcription of each formula, along with a breakdown of its components:
1. **First-order Differentiation in Time Domain:**
`L{d/dt f(t)} = sF(s) - f(0)`
This formula states that the Laplace transform of the first derivative of a function f(t) is equal to s times the Laplace transform of f(t) minus the initial value of f(t).
2. **Higher-order Differentiation in Time Domain:**
`L{d^n/dt^n f(t)} = s^n F(s) - Ξ£(k=1 to n-1) sk-1 f^(n-k)(0)`
This formula generalizes the first-order differentiation to higher orders. It states that the Laplace transform of the nth derivative of f(t) is equal to s^n times the Laplace transform of f(t) minus a summation term involving the lower-order derivatives of f(t) evaluated at t=0.
3. **Integration in Time Domain:**
`L{β«f(t) dt} = 1/s F(s)`
This formula states that the Laplace transform of the integral of f(t) is equal to the Laplace transform of f(t) divided by s.
4. **Time Shifting:**
`L{f(t-to)u(t-to)} = e^(-sto)F(s)`
This formula describes the effect of a time shift on the Laplace transform. `u(t-to)` is the unit step function.
5. **Time Scaling:**
`L{f(ct)} = 1/c F(s/c), 0 < c`
This formula describes the effect of time scaling on the Laplace transform.
6. **Cosine Based Modulation:**
`L{f(t)cos(Οt)} = (1/2)[F(s+jΟ) + F(s-jΟ)]`
This formula states the Laplace transform of a function f(t) multiplied by a cosine wave.
7. **Sinusoidal Modulation:**
`L{f(t)sin(Οt)} = (j/2)[F(s+jΟ) - F(s-jΟ)]`
This formula states the Laplace transform of a function f(t) multiplied by a sine wave.
**Symbolic Notation:**
* `L{}`: Represents the Laplace transform operator.
* `f(t)`: Represents a function of time.
* `F(s)`: Represents the Laplace transform of f(t).
* `s`: Represents the complex frequency variable in the Laplace domain.
* `t`: Represents time.
* `to`: Represents a time shift.
* `c`: Represents a scaling factor.
* `Ο`: Represents angular frequency.
* `j`: Represents the imaginary unit (β-1).
* `u(t)`: Represents the unit step function.
* `β«`: Represents the integral operator.
* `d/dt`: Represents the derivative operator.
* `d^n/dt^n`: Represents the nth derivative operator.
* `Ξ£`: Represents summation.
### Key Observations
The formulas are presented in a consistent format, clearly showing the relationship between the time-domain function and its Laplace transform. The use of symbolic notation is standard in mathematical literature. The formulas build upon each other, starting with basic differentiation and integration and progressing to more complex operations like modulation.
### Interpretation
The image provides a concise reference for fundamental Laplace transform properties. These properties are crucial for solving differential equations, analyzing linear time-invariant systems, and designing control systems. The formulas demonstrate how operations in the time domain are transformed into algebraic operations in the s-domain, which often simplifies the analysis and solution process. The inclusion of initial conditions (f(0), f^(n-k)(0)) in the differentiation formulas highlights the importance of these conditions when using Laplace transforms to solve initial value problems. The modulation formulas are essential for analyzing signals that are amplitude-modulated or frequency-modulated. The formulas are presented in a formal mathematical style, suggesting they are intended for an audience with a strong mathematical background.
</details>
| First-order Differ- entiation in Time Domain L [ d dt f ( t ) ] = sF ( s ) - f (0) | β f s. laplace exists f s β§ ( β t. f differentiable at t) β§ laplace exists ( Ξ» t. vector derivative f (at t)) s β laplace transform ( Ξ» t. vector derivative f (at t)) s = |
|------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| Higher-order Diffe- rentiation in Time Domain L [ d n n f ( t )] = s n F ( s ) | s β laplace transform f s - f (lift (&0)) β f s n. laplace exists higher deriv n f s β§ ( β t. differentiable higher derivative n f t) |
| dt - β n k =1 s k - 1 d n - k f (0) dx n - k | β laplace transform ( Ξ» t. higher vector derivative n f t) s = s pow n β laplace transform f s - vsum (1..n) ( Ξ» x. s pow (x - 1) β higher vector derivative (n - x) f (lift (&0))) |
| Integration in Time Domain L [ β« t 0 f ( Ο ) dΟ ] = 1 s F ( s ) | β f s. &0 < Re s β§ laplace exists f s β§ laplace exists ( Ξ» x. integral (interval [lift (&0),x]) f) s β§ ( β x. f continuous on interval [lift (&0),x]) β laplace transform ( Ξ» x. integral (interval [lift (&0),x]) f) s = Cx (& 1 ) β laplace transform f s |
| Time Shifting L [ f ( t - t 0 ) u ( t - t 0 )] = e - t 0 s F ( s ) | s β f s t0. &0 < drop t0 β§ laplace exists f s β laplace transform (shifted fun f t0) s = cexp (--(s β Cx (drop t0))) β laplace transform f s |
| Time Scaling L [ f ( ct )] = 1 c F ( s c ) , 0 < c | β f s c. &0 < c β§ laplace exists f s β§ laplace exists f ( s Cx c ) β laplace transform ( Ξ» t. f(c % t)) s = Cx (& 1 ) Cx c β laplace transform f ( s Cx c ) |
| Cosine Based Modulation L [ f ( t ) cos ( Ο 0 t )] = F ( s - jΟ 0 ) 2 + F ( s + jΟ 0 ) 2 | β f s w0. laplace exists f s β laplace transform ( Ξ» t. ccos (Cx w0 β Cx (drop t)) β f t) s = laplace transform f ( s - ii β Cx w0 ) Cx (& 2 ) + laplace transform f ( s + ii β Cx w0 ) Cx (& 2 ) |
| Sine Based Modulation L [ f ( t ) cos ( Ο 0 t )] = F ( s - jΟ 0 ) 2 j - F ( s + jΟ 0 ) | β f s w0. laplace exists f s β laplace transform ( Ξ» t. csin (Cx w0 β Cx (drop t)) β f t) s = laplace transform f ( s - ii β Cx w0 ) Cx (& 2 ) β ii - laplace transform f ( s + ii β Cx w0 ) |
| n -order Differ- ential Equation L ( β n k =0 Ξ± k d k y dt k ) = F ( s ) β n k =0 Ξ± k s k - β n k =0 β k i =1 s i - 1 d k - i f (0) dt k - i | β f lst s n. laplace exists higher deriv n f s β§ ( β t. differentiable higher derivative n f t) β laplace transform ( Ξ» t. diff eq n order n lst f t) s = laplace transform f s β vsum (0..n) ( Ξ» k. EL k lst β s pow k) - vsum (0..n) ( Ξ» k. EL k lst β vsum (1..k) ( Ξ» i. s pow (i - 1) β higher vector derivative (k - i) f (lift (&0)))) |
|------------------------------------------------------------------------------------------------------------------------------------------------|---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
place of all the derivatives up to the n th order of the function f exist. Similarly, the predicate differentiable higher derivative provides the differentiability of the function f and its higher derivatives up to the n th order. The verification of these properties not only ensures the correctness of our definitions but also plays a vital role in minimizing the user effort in reasoning about Laplace transform based analysis of systems, as will be depicted in Sections 4 and 5 of this paper.
The generalized linear differential equation describes the input-output relationship for a generic n -order linear control system [15]:
$$\sum _ { k = 0 } ^ { n } \alpha _ { k } \frac { d ^ { k } } { d t ^ { k } } y ( t ) = \sum _ { k = 0 } ^ { m } \beta _ { k } \frac { d ^ { k } } { d t ^ { k } } x ( t ) , \quad m \leq n \quad ( 2 )$$
where y ( t ) is the output and x ( t ) is the input to the system. The constants Ξ± k and Ξ² k are the coefficients of the output and input differentials with order k , respectively. The greatest index n of the non-zero coefficient Ξ± n determines the order of the underlying system. The corresponding transfer function is obtained by setting the initial conditions equal to zero [15]:
$$\frac { Y ( s ) } { X ( s ) } = \frac { \sum _ { k = 0 } ^ { m } \beta _ { k } s ^ { k } } { \sum _ { k = 0 } ^ { n } \alpha _ { k } s ^ { k } } \quad ( 3 )$$
We verified the transfer function, given in Equation 3, for the generic n-order linear control system as the following HOL Light theorem.
## Theorem 1. β y x m n inlst outlst s.
```
Theorem 1. + \y x m n inlst outlst s.
( \forall t. differentiable higher deriv m n x y t) ^
laplace exists of higher deriv m n x y s ^ zero init conditions m n x y ^
diff eq n order sys m n inlst outlst x y ^
~(laplace transform x s = Cx (&0)) ^
~(vsum (0..n) ( \lambda. t. EL t outlst * s pow t) = Cx (&0))
=> laplace transform y s = vsum (0..m) ( \lambda.t. EL t inlst * s pow t)
:= laplace transform x s = vsum (0..n) ( \lambda.t. EL t outlst * s pow t)
```
The first assumption ensures that the functions y and x are differentiable up to the n th and m th order, respectively. The next assumption represents the Laplace transform existence condition up to the n th order derivative of function y and m th order derivative of the function x . The next assumption models the zero initial conditions for both of the functions y and x , respectively. The next assumption represents the formalization of Equation 2 and the last two assumptions provide
the conditions for the design of a reliable linear control system. Finally, the conclusion of the above theorem represents the transfer function given by Equation 3. The verification of this theorem is very useful as it allows to automate the verification of the transfer function of any linear control system as described in Sections 4 and 5 of the paper. The formalization, described in this section, took around 2000 lines of HOL Light code [17] and around 130 man-hours.
## 4 Formalization of Linear Control Systems Foundations
A general closed-loop control system is depicted in Fig. 2a. Here, X ( s ) and Y ( s ) represent the Laplace transforms of the time domain input x ( t ) and the output y ( t ), respectively. G ( s ) and H ( s ) represent the forward path and the feedback path transfer functions, respectively. Similarly, G ( s ) H ( s ) is the open loop transfer function of the system and Y ( s ) /X ( s ) is the closed loop transfer function [7]. Table 2 presents the formalization of the frequency response, phase margin and gain margin of this control system. These properties are used to study the dynamics of a linear control system in the frequency domain and to perform its stability analysis.
The frequency response is used to analyze the dynamics of the system by studying the impact of different frequency components on the intended behaviour of the given linear control system. We also formally verified the frequency response of a generic n -order system based on assumptions that are very similar to the ones used for Theorem 1.
Table 2: Properties of Linear Control Systems
| Property | Formalized Form |
|------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
| Frequency Response M ( jΟ ) = M ( s ) | ( jΟ ) = Y ( s ) X ( s ) β£ β£ β£ β£ β£ ( jΟ ) = Y ( jΟ ) X ( jΟ ) | β y x w. frequency response x y w = laplace transform y ( ii β Cx w ) laplace transform x ( ii β Cx w ) |
| Frequency Response of an n -order System Y ( jΟ ) X ( jΟ ) = β m k =0 Ξ² k ( jΟ ) k β n k =0 Ξ± k ( jΟ ) k | β y x m n inlst outlst s. ( β t. differentiable higher deriv m n x y t) β§ laplace exists of higher deriv m n x y w β§ zero init conditions m n x y β§ diff eq n order sys m n inlst outlst y x β§ non zero denom cond n x w outlst β frequency response x y w = vsum ( 0 .. m ) ( Ξ» t . EL t inlst β ( ii β Cx w ) pow t ) vsum ( 0 .. n ) ( Ξ» t . EL t outlst β ( ii β Cx w ) pow t ) |
| Phase Margin [ β G ( jΟ ) H ( jΟ )] Ο = Ο gc + 180 o | β g h wgc. phase margin g h wgc = pi + Arg (g (ii β Cx wgc) β h (ii β Cx wgc)) |
| Gain Margin [ 20 log 10 β£ β£ β£ G ( jΟ ) H ( jΟ ) β£ β£ β£ Ο = Ο pc ] dB | β g h wpc. gain margin db g h wpc = &20 β log ( norm ( g ( ii β Cx wpc ) β h ( ii β Cx wpc ))) log (& 10 ) |
Phase margin and gain margin provide useful information about controlling the stability of the system [7]. Phase margin represents 180 o shifted phase angle of the open loop transfer function evaluated at the gain crossover frequency ( Ο gc ), which is the frequency at which the magnitude of the open loop transfer function is equal to 0 dB. The gain margin represents the magnitude of the open loop transfer function evaluated at the phase crossover frequency ( Ο pc ), which is the frequency at which the resultant phase curve of the open loop gain has a phase of 180 o . In our formal definitions of these notions, the function Arg(z) represents the argument of a complex number z .
Fig. 2: Control Systems Foundations (a) Closed Loop Control System (b) Generic Active Realization of Controller (c) PID Configuration (d) Lag/lead Compensator Configuration (e) Generic Passive Realization of Compensator (f) Lag-lead Compensator Configuration
<details>
<summary>Image 3 Details</summary>
### Visual Description
\n
## Diagram: Transconductance Amplifier Circuit Stages
### Overview
The image presents a series of diagrams illustrating the stages of a transconductance amplifier circuit. It begins with a block diagram of a feedback system and progresses through circuit representations involving operational amplifiers, capacitors, and resistors. The diagrams appear to demonstrate the equivalent circuits at different points in the signal processing chain.
### Components/Axes
The diagrams utilize the following components:
* **X(s):** Input signal.
* **Y(s):** Output signal.
* **G(s):** Transfer function of the forward path.
* **H(s):** Transfer function of the feedback path.
* **v<sub>i</sub>(t):** Input voltage.
* **v<sub>o</sub>(t):** Output voltage.
* **i<sub>C</sub>(t):** Collector current.
* **i<sub>CB</sub>(t):** Base current.
* **C<sub>1</sub>, C<sub>2</sub>:** Capacitors.
* **R<sub>1</sub>, R<sub>2</sub>:** Resistors.
* **C<sub>A</sub>, C<sub>B</sub>:** Capacitors.
* Operational Amplifier (triangle symbol).
* Ground symbol.
### Detailed Analysis or Content Details
**(a) Block Diagram:**
A block diagram showing a closed-loop system. The input signal X(s) is fed into a block representing the forward transfer function G(s). The output Y(s) is fed back to the input through a block representing the feedback transfer function H(s). A summation point (circle with a cross) combines the input signal and the feedback signal.
**(b) Operational Amplifier Circuit:**
An operational amplifier circuit with input voltage v<sub>i</sub>(t), collector current i<sub>C</sub>(t), base current i<sub>CB</sub>(t), and output voltage v<sub>o</sub>(t). The operational amplifier has a positive input connected to ground and a negative input connected to v<sub>i</sub>(t). The output is connected to a capacitor C<sub>B</sub>.
**(c) Equivalent Circuit 1:**
An equivalent circuit consisting of a capacitor C<sub>1</sub> in series with a resistor R<sub>1</sub>, connected to capacitor C<sub>A</sub>. This is in parallel with a resistor R<sub>2</sub> in series with a capacitor C<sub>B</sub>.
**(d) Equivalent Circuit 2:**
A circuit with C<sub>1</sub> and R<sub>1</sub> enclosed in a dashed box, and C<sub>2</sub> and R<sub>2</sub> enclosed in a dashed box. The two boxes are connected in series.
**(e) Simplified Circuit:**
A simplified circuit showing capacitors C<sub>A</sub> and C<sub>B</sub> connected in series between the input voltage v<sub>i</sub>(t) and the output voltage v<sub>o</sub>(t). A horizontal line is drawn beneath the capacitors.
**(f) Equivalent Circuit 3:**
An equivalent circuit consisting of a capacitor C<sub>1</sub> in series with a resistor R<sub>1</sub>, connected to capacitor C<sub>A</sub>. This is in parallel with a resistor R<sub>2</sub> in series with a capacitor C<sub>2</sub>, connected to capacitor C<sub>B</sub>. The output voltage v<sub>o</sub>(t) is taken across the parallel combination.
### Key Observations
The diagrams progressively simplify the circuit, moving from a block diagram to equivalent circuits. The presence of capacitors and resistors suggests frequency-dependent behavior. The operational amplifier in diagram (b) indicates a gain stage. The dashed boxes in diagram (d) may represent simplified models of specific circuit sections.
### Interpretation
The series of diagrams likely illustrates the derivation of an equivalent circuit model for a transconductance amplifier. The initial block diagram (a) establishes the overall system architecture. Diagram (b) shows the basic operational amplifier configuration. Diagrams (c), (d), (e), and (f) then present increasingly simplified equivalent circuits, likely obtained through circuit analysis techniques such as impedance transformation or approximation. The goal is to represent the amplifier's behavior with a manageable circuit model that can be used for further analysis and design. The simplification process suggests that certain circuit elements or effects are being neglected to achieve a more concise representation. The presence of capacitors indicates that the amplifier's performance is frequency-dependent, and the equivalent circuits are likely valid only within a specific frequency range. The diagrams demonstrate a systematic approach to circuit modeling, starting from a detailed representation and progressively simplifying it to obtain a more abstract but useful model.
</details>
The controllers form the most vital part of any control system as they are mainly responsible for the correct operation of every component of the underlying system. Controllers are modeled using their active realizations based on an electrical circuit, which comprises of an inverting operational amplifier (op-amp) with unity gain, and two components, i.e., C A and C B , which are shown as rectangular boxes in Fig. 2b. The boxes C A and C B contain different configurations of the passive components, i.e., resistors and capacitors [16]. By making an appropriate choice of these passive components, we obtain various controllers, such as P, I, D, PI, PD, PID [15]. For the analysis of these controllers, we first need to formalize them in higher-order logic. This step requires a formal library of analog components [21,17], describing the voltage-current relationships of resistor, capacitors and inductors, and the KCL and KVL, which model the currents and voltages in an electrical circuit.
The PID controller, depicted in Fig. 2c, can be formalized as follows:
```
Definition 10. |- \C1 R1 Vi R2 C2 Vo Vb Va.
pid controller implem Vi Vo Va Vb C1 C2 R1 R2 <>
( \t. &0 < drop t => kcl [\t. capacitor current C1 (\t. Vi t - Va t) t;
\t. resistor current R1 (\t. Vi t - Va t) t;
\t. resistor current R2 (\t. Vb t - Va t) t] ^
( \t. &0 < drop t => kcl [\t. resistor current R2 (\t. Va t - Vb t) t;
\t. capacitor current C2 (\t. Vo t - Vb t) t] ^
( \t. &0 < drop t => Va t = Cx (&0))
```
where Vi and Vo are the input and the output voltages, respectively, having data type R 1 β C , and Va and Vb are the voltages at nodes a and b , respectively. The functions resistor current and capcitor current are the currents across the resistor and capacitor, respectively. The function kcl accepts a list of currents across the components of the circuit and a time variable t and returns the predicate that guarantees that the sum of all the currents leaving a particular node at time t is zero. The first conjunct of the above definition represents the application of KCL across node a . Similarly, the second conjunct models the KCL at node b , whereas the last conjunct provides the voltage across the non-inverting input of the op-amp using the virtual ground condition, as shown in Fig. 2b. We also develop a simplification tactic KCL SIMP TAC , which simplifies the implementations of the PID controller as well as other controllers and compensators. The details can be found in [17].
Next, we model the dynamical behaviour of the PID controller using the n -order differential equation:
```
Definition 11. ! R1 R2 C1 C2. inlst pid contr R1 R2 C1 C2 =
[--Cx (&1); --Cx (R2 * C2 + R1 * C1); --Cx (R1 * R2 * C1 * C2)]
! ! R1 C2. outlst pid contr R1 C2 = [Cx (&0); Cx (R1 * C2)]
! ! Vo R1 R2 C1 C2 Vi t. pid controller behav spec R1 R2 C1 C2 Vi Vo t <>
diff eq n order 1 (outlst pid contr R1 C2) Vo t =
diff eq n order 2 (inlst pid contr R1 R2 C1 C2) Vi t
```
We verified the behavioural specification based on the implementation of the PID controller as the following theorem:
```
Theorem 2. - β R1 R2 C1 C2 Vi Va Vb Vo t. &0 < R1 β§ &0 < R2 β§
&0 < C1 β§ &0 < C2 β§ (βt. differentiable higher derivative Vi Vo Vb t) β§
pid controller implem Vi Vo Va Vb C1 C2 R1 R2
β (&0 < drop t β pid controller behav spec R1 R2 C1 C2 Vi Vo t)
```
The first four assumptions model the design requirement for the underlying system. The next assumption provides the differentiability of the higher-order derivatives of Vi , Vo and Vb up to the order 1, 2 and 2, respectively. The last assumption presents the implementation for the PID controller. Finally, the conclusion presents its behavioral specification. We also develop a simplification tactic DIFF SIMP TAC , which simplifies the behavioural specifications of the PID controller as well as the other controllers and compensators [17].
Next, we verified the transfer function of the PID controller as follows:
```
Theorem 3. β’ \ R1 R2 C1 C2 Vi Vo s t. &0 < R1 ^ \& 0 < R2 ^ \& 0 < C1 ^
~(laplace transform Vi s = Cx (&0)) ^ \sim (Cx R1 * Cx C2 * s = Cx (&0)) ^
&0 < C2 ^ \wedge ( \forall t. differentiable higher derivative Vi Vo t) ^
laplace exists higher deriv Vi Vo s ^ zero initial conditions Vi Vo ^
( \forall t. pid controller behav spec R1 R2 C1 C2 Vi Vo t)
=> laplace transform Vo s =
laplace transform Vi s
--(Cx(R1 * C1 * R2 * C2) * s pow 2 + (Cx(R2 * C2) + Cx(C1 * R1)) * s + Cx(&1))
```
Cx ( R1 β C2 ) β s
The first six assumptions present the design requirements for the underlying system. The next two assumptions provide the differentiability and the Laplace existence condition for the higher-order derivatives of Vi and Vo up to the order 2 and 1, respectively. The next assumption models the zero initial conditions for the voltage functions Vi and Vo . The last assumption presents the behavioural specification of the PID controller. Finally, the conclusion of Theorem 3 presents its required transfer function. By judicious selection of the configuration of passive components, we obtain various controllers, such as P, I, D, PI, PD and perform the above-mentioned analysis for all of them.
Compensators are widely used in control systems, to improve their frequency response, steady-state error and the stability and hence, act as a fundamental block of a control system. Like controllers, the compensators are also modeled using their active realizations. A compensator uses the same analog circuit, which is used for the controllers, presented in Fig. 2b, by making an appropriate choice of the passive components C A and C B , as shown in Fig. 2d. It acts as a lag-compensator under the condition R 2 C 2 > R 1 C 1 , whereas for the case of R 1 C 1 > R 2 C 2 , it acts as a lead-compensator. The configurations of the passive components for the controllers and compensators, and their formalization is presented in [17].
Compensators are also modeled using their passive realizations based on an electrical circuit, which comprises of two components, i.e., C A and C B , which are shown as rectangular boxes in Fig. 2e. The boxes C A and C B contain different configurations of the passive components, i.e., resistors and capacitors. By making an appropriate choice of these passive components, we obtain various compensators, such as lag, lead and lag-lead [15]. The configuration of the lag-lead compensator is shown in Fig. 2f. Moreover, the configurations of the passive components for the compensators and their formalization in HOL Light is presented in [17].
The formalization of this section took around 300 lines of HOL Light code and around 14 man-hours. This clearly illustrates the effectiveness of our foundational formalization, presented in the previous section.
## 5 Unmanned Free-Swimming Submersible Vehicle
Unmanned Free-Swimming Submersible (UFSS) vehicles are a kind of autonomous underwater vehicles (AUVs) that are used to perform different tasks and operations in the submerged areas of the water. These vehicles have their own power
and control systems, which are autonomously operated and controlled by the onboard computer system without any involvement of human assistance as it is difficult for humans to work in an underwater environment. UFSS vehicles are used in many safety-critical domains to perform different tasks, such as underwater navigation and object detection [13], performing deep sea rescue and salvage operations [23], searching for sea mines [24] and securing sea harbour [24]. Due to their wider usage in the above-mentioned safety-critical applications, an accurate analysis of their control system is of utmost importance.
We present a formal analysis of the pitch control system of a UFSS vehicle. The pitch control system is responsible for the uninterrupted operation and functionality of the UFSS vehicle by manipulating different parameters, such as, elevator surface, pitch angle [15]. Fig. 3 depicts its block diagram.
Fig. 3: Pitch Control Model for Unmanned Free-swimming Submersible Vehicle
<details>
<summary>Image 4 Details</summary>
### Visual Description
\n
## Block Diagram: Pitch Control System
### Overview
The image depicts a block diagram representing a pitch control system for a vehicle. It illustrates the flow of signals from a pitch command through various components β gain, actuator, vehicle dynamics, and feedback β to ultimately control the pitch angle. The diagram uses standard block diagram notation to represent mathematical relationships and signal flow.
### Components/Axes
The diagram consists of the following components:
* **Pitch Command:** Input signal denoted as ΞΈ<sub>d</sub>(s).
* **Pitch Gain:** Block labeled -K<sub>1</sub>.
* **Summing Junctions:** Represented by circles with "+" and "-" signs, indicating addition and subtraction of signals.
* **Commanded Elevator Deflection:** Signal denoted as Ξ΄<sub>c</sub>(s).
* **Elevator Actuator:** Block with transfer function 2/(s+2).
* **Elevator Deflection:** Signal denoted as Ξ΄<sub>e</sub>(s).
* **Vehicle Dynamics:** Block with transfer function -0.125(s+0.435) / ((s+1.23)(s<sup>2</sup>+0.226s+0.0169)).
* **Pitch:** Output signal denoted as ΞΈ(s).
* **Pitch Rate Sensor:** Block labeled -K<sub>2</sub>s.
* **Feedback Loop:** A line connecting the pitch output ΞΈ(s) to a summing junction, representing feedback.
### Detailed Analysis
The system operates as follows:
1. **Pitch Command:** The system receives a desired pitch angle command, ΞΈ<sub>d</sub>(s).
2. **Pitch Gain:** This command is multiplied by a gain -K<sub>1</sub>.
3. **Commanded Elevator Deflection:** The output of the pitch gain is added to the feedback signal (from the pitch rate sensor) at a summing junction to produce the commanded elevator deflection, Ξ΄<sub>c</sub>(s).
4. **Elevator Actuator:** The commanded elevator deflection signal is passed through an elevator actuator with a transfer function of 2/(s+2), resulting in the actual elevator deflection, Ξ΄<sub>e</sub>(s).
5. **Vehicle Dynamics:** The elevator deflection affects the vehicle dynamics, modeled by the transfer function -0.125(s+0.435) / ((s+1.23)(s<sup>2</sup>+0.226s+0.0169)), producing the pitch angle output, ΞΈ(s).
6. **Pitch Rate Sensor:** The pitch angle is measured by a pitch rate sensor, which outputs a signal proportional to the pitch rate, -K<sub>2</sub>s.
7. **Feedback:** This signal is fed back to the summing junction, completing the control loop.
The transfer functions are:
* Pitch Gain: -K<sub>1</sub>
* Elevator Actuator: 2/(s+2)
* Vehicle Dynamics: -0.125(s+0.435) / ((s+1.23)(s<sup>2</sup>+0.226s+0.0169))
* Pitch Rate Sensor: -K<sub>2</sub>s
### Key Observations
The system employs a closed-loop control scheme with negative feedback. The negative signs in the gains (-K<sub>1</sub> and -K<sub>2</sub>) and the vehicle dynamics transfer function indicate that the system is designed to counteract disturbances and maintain the desired pitch angle. The actuator has a first-order response (2/(s+2)), while the vehicle dynamics are modeled as a more complex third-order system.
### Interpretation
This block diagram represents a simplified model of a pitch control system, commonly found in aircraft or other vehicles with pitch control surfaces. The negative feedback loop is crucial for stability and accurate tracking of the desired pitch angle. The gains K<sub>1</sub> and K<sub>2</sub> are tuning parameters that can be adjusted to optimize the system's performance (e.g., response time, overshoot, stability). The transfer functions represent the dynamic behavior of the individual components. The complexity of the vehicle dynamics transfer function suggests that the vehicle's response to elevator deflection is not simple and may involve multiple modes of oscillation or damping. The diagram provides a high-level overview of the system's structure and allows for analysis of its stability and performance characteristics using control theory techniques.
</details>
The dynamics of the UFSS vehicle are represented by its corresponding differential equation, which presents the relationship between the pitch command angle ΞΈ e ( t ) and the pitch angle ΞΈ ( t ), and is given as follows:
$$\begin{array} { r l r } & { \frac { d ^ { 4 } \theta } { d t ^ { 4 } } + 3 . 4 5 6 \frac { d ^ { 3 } \theta } { d t ^ { 3 } } + ( 3 . 2 0 7 + 0 . 2 5 K _ { 2 } ) \frac { d ^ { 2 } \theta } { d t ^ { 2 } } + ( 0 . 6 1 6 + 0 . 1 0 8 8 K _ { 2 } + 0 . 2 5 K _ { 1 } ) \frac { d \theta } { d t } + } \\ & { ( 0 . 1 0 8 8 K _ { 1 } + 0 . 0 4 1 6 ) = 0 . 2 5 K _ { 1 } \frac { d \theta _ { e } } { d t } + 0 . 1 0 8 8 K _ { 1 } } \end{array} ( 4 )$$
We formalize the above differential equation as follows [18]:
```
Definition 12. 1+ \ K1. inlst ufsv K1 = [Cx(#0.1088) * Cx K1;Cx (#0.25) * Cx K1]
\[Cx(#0.1088) * Cx K1 + Cx(#0.0416);Cx(#0.25) * Cx K1 + Cx(#0.1088) * Cx K2
+ Cx(#0.6106);Cx(#0.25) * Cx K2 + Cx(#3.207);Cx(#3.456);Cx (&1)]
\[ diff eq ufsv inlst ufsv outlst ufsv theta thetae K1 K2 <=>
(\/t. diff eq n order 4 (outlst ufsv K1 K2) theta t =
diff eq n order 1 (inlst ufsv K1) thetae t)
```
where thetae and theta represent the input and the output of the pitch control system and K1 and K2 are the pitch gain and pitch rate sensor gain, respectively. The symbol # is used to represent a decimal number of data type R in HOL Light and is same as symbol & for the integer literal of data type R .
The transfer function of the pitch control of the UFSS vehicle is as follows:
$$\frac { \theta ( s ) } { \theta _ { e } ( s ) } = \frac { 0 . 2 5 K _ { 1 } s + 0 . 1 0 8 8 K _ { 1 } } { s ^ { 4 } + 3 . 4 5 6 s ^ { 3 } + ( 3 . 2 0 7 + 0 . 2 5 K _ { 2 } ) s ^ { 2 } + ( 0 . 6 1 0 6 + 0 . 1 0 8 8 K _ { 2 } + } \quad ( 5 )$$
We verified the above transfer function as the following HOL Light theorem:
```
We verified the above transfer function as the following HOL Light theorem:
Theorem 4. 1 9 thetae theta s K1 K2.
( \forall t . differentiable higher deriv thetae t) ^
laplace exists of higher deriv theta e theta s ^
zero init conditions thetae theta ^
diff eq ufsv inlst ufsv outlst ufsv thetae theta K1 K2 ^
non zero denominator condition theta s
\laplace transform theta s
= laplace transform theta e s
(Cx(#0.25) * Cx K1) * s + Cx(#0.1088) * Cx K1
```
The first two assumptions present the differentiability and the Laplace existence condition of the higher-order derivatives of thetae and theta up to order 1 and 4, respectively. The next assumption provides the zero initial conditions for thetae and theta . The next assumption presents the differential equation specification for the pitch control system of UFSS vehicle. The final assumption models the non-negativity of the denominator of the transfer function presented in the conclusion of the above theorem. We also verified the open loop transfer function ΞΈ ( s ) /Ξ΄ e ( s ), frequency response (open and closed loop) and gain margin, for the UFSS vehicle and the details can be found in [17].
The distinguishing feature of Theorem 4 and the other properties, compared to traditional analysis methods is their generic nature, i.e., all of the variables and functions are universally quantified and can thus be specialized in order to obtain the results for some given values. Moreover, all of the required assumptions are guaranteed to be explicitly mentioned along with the theorems due to the inherent soundness of the theorem proving approach. The high expressiveness of the higher-order logic enables us to model the differential equation and the corresponding transfer function in their true continuous form, whereas, in model checking they are mostly discretized and modeled using a state-transition system, which compromises the accuracy of the analysis.
To facilitate control engineers in using our formalization, we developed an automatic tactic TRANSFER FUN TAC , which automatically verifies the transfer function of the systems up to 20 th -order. This tactic was successfully used for the automatic verification of the transfer functions of the controllers, compensators and the pitch control system of the UFSS vehicle. This automatic verification tactic only requires the differential equation and the transfer function of the
underlying system and automatically verifies the transfer function. Thus, the formal analysis of the UFSS vehicle took only 25 lines of code and about half an hour, thanks to our automatic tactic and the foundational formalization of Section 3.
## 6 Conclusion
This paper presented a higher-order-logic theorem proving based approach for the formal analysis of the dynamical aspects of linear control systems using theorem proving. The main idea behind the proposed framework is to use a formalization of Laplace transform theory in higher-order logic to formally analyze the dynamic aspects of linear control systems. For this purpose, we develop a new formalization of Laplace transform theory, which includes its formal definition and verification of its properties, such as linearity, frequency shifting, differentiation and integration in time domain, time shifting, time scaling, cosine and sinebased modulation and the Laplace transform of an n -order differential equation, which are used for the verification of the transfer function of a generic n -order linear control system. Moreover, the paper also presents the formal verification of some widely used linear control system characteristics, such as frequency response, phase margin and the gain margin, using the verified transfer function, which can be used for the stability analysis of a linear control system. We also formalize the active realization of various controllers, such as PID, PD, PI, P, I, D, and various compensators, such as lag and lead. Finally, we formalize the passive realization of the various compensators, such as lag, lead and lag-lead and verified the corresponding behavioral (differential equation) and the transfer function specifications. To facilitate the usage of these formalizations in analyzing real-world linear control systems, we developed some simplification and automatic verification tactics, in particular the tactic TRANSFER FUN TAC , which automatically verifies the transfer function of any real-world linear control system based on its differential equation. These foundations can be used to analyze a wide range of linear control systems and for illustration purposes, the paper presents the formal analysis of an unmanned free-swimming submersible vehicle.
In future, we plan to link the proposed formalization with Simulink so that the users can provide the system model as a block diagram. This diagram can be used to extract the corresponding transfer function [3], which can in turn be formally verified, almost automatically, to be equivalent to the corresponding block diagram based on the reported formalization and reasoning support.
## Acknowledgements
This work was supported by the National Research Program for Universities grant (number 1543) of Higher Education Commission (HEC), Pakistan.
## References
1. Ahmad, M., Hasan, O.: Formal Verification of Steady-State Errors in UnityFeedback Control Systems. In: Formal Methods for Industrial Critical Systems. pp. 1-15. Springer (2014)
2. ArΒ΄ echiga, N., Loos, S.M., Platzer, A., Krogh, B.H.: Using Theorem Provers to Guarantee Closed-loop System Properties. In: American Control Conference (ACC), 2012. pp. 3573-3580. IEEE (2012)
3. Babuska, R., Stramigioli, S.: Matlab and Simulink for Modeling and Control. Delft University of Technology (1999)
4. Beerends, R.J., Morsche, H.G., Van den Berg, J.C., Van de Vrie, E.M.: Fourier and Laplace Transforms. Cambridge University Press, Cambridge (2003)
5. Beillahi, S.M., Siddique, U., Tahar, S.: Formal Analysis of Power Electronic Systems. In: Formal Engineering Methods. pp. 270-286. Springer (2015)
6. Boulton, R.J., Hardy, R., Martin, U.: A Hoare Logic for Single-input Single-output Continuous-time Control Systems. In: International Workshop on Hybrid Systems: Computation and Control. pp. 113-125. Springer (2003)
7. Ghosh, S.: Control Systems, vol. 1000. Pearson Education (2010)
8. Harrison, J.: HOL Light: A Tutorial Introduction. In: Formal Methods in Computer-Aided Design. LNCS, vol. 1166, pp. 265-269. Springer (1996)
9. Harrison, J.: The HOL Light Theory of Euclidean Space. Journal of Automated Reasoning 50(2), 173-190 (2013)
10. Hasan, O., Ahmad, M.: Formal Analysis of Steady State Errors in Feedback Control Systems using HOL-Light. In: Design, Automation and Test in Europe. pp. 14231426 (2013)
11. Hasan, O., Tahar, S.: Formal verification methods. Encyclopedia of Information Science and Technology, IGI Global Pub pp. 7162-7170 (2015)
12. Johnson, M.E.: Model Checking Safety Properties of Servo-loop Control Systems. In: Dependable Systems and Networks. pp. 45-50. IEEE (2002)
13. Kondo, H., Ura, T.: Navigation of an AUV for Investigation of Underwater Structures. Control Engineering Practice 12(12), 1551-1559 (2004)
14. Lutovac, M., ToΛ siΒ΄ c, D.: Symbolic Analysis and Design of Control Systems using Mathematica. International Journal of Control 79(11), 1368-1381 (2006)
15. Nise, N.S.: Control Systems Engineering. John Wiley & Sons (2007)
16. Ogata, K., Yang, Y.: Modern Control Engineering (1970)
17. Rashid, A.: Formal Analysis of Linear Control Systems using Theorem Proving. http://save.seecs.nust.edu.pk/projects/falcstp (2017)
18. Rashid, A., Hasan, O.: On the Formalization of Fourier Transform in Higher-order Logic. In: International Conference on Interactive Theorem Proving. LNCS, vol. 9807, pp. 483-490. Springer (2016)
19. Rashid, A., Hasan, O.: Formalization of Transform Methods using HOL Light. In: Conference on Intelligent Computer Mathematics. LNAI, vol. 10383, pp. 319-332. Springer (2017)
20. Taqdees, S.H., Hasan, O.: Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light. In: Logic for Programming, Artificial Intelligence, and Reasoning. pp. 744-758. Springer (2013)
21. Taqdees, S.H., Hasan, O.: Formally Verifying Transfer Functions of Linear Analog Circuits. IEEE Design & Test, http://save.seecs.nust.edu.pk/pubs/2017/ DTnA\_2017.pdf (2017)
22. Tiwari, A., Khanna, G.: Series of Abstractions for Hybrid Automata. In: Hybrid Systems: Computation and Control. pp. 465-478. Springer (2002)
23. Wernli, R.L.: Low Cost UUV's for Military Applications: Is the Technology Ready? In: Pacific Congress on Marine Science and Technology (2001)
24. Willcox, S., Vaganay, J., Grieve, R., Rish, J.: The Bluefin BPAUV: An Organic Widearea Bottom Mapping and Mine-hunting Vehicle. Unmanned Untethered Submersible Technology (2001)