{'fraction_non_alphanumeric': 0.03556975083320108, 'fraction_numerical': 0.008768449452467863, 'mean_word_length': 4.4023148644303935, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 20, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Formally expressing the semantics of observer-based fault detection software

The aim is to create reliable and verifiable fault detection software to detect abrupt changes in safety-critical dynamic systems. Fault detection methods are implemented as software on digital computers that monitor and control the system. We implement three observer-based fault detection methods on a 3 degrees of freedom (3DOF) laboratory helicopter, in the form of software. We examine the performance of those methods to detect different faults during flight in a closed-loop setup. All selected methods show acceptable detection performance. However, it is not possible to repeat the test for every possible conditions, inputs and fault scenarios. In this paper, we translate fault detection properties and mathematical proofs into a formal language, previously used in software validation and verification. We include the translated properties in software in the form of non-executable annotations that can be read by machine. Consequently, some high level functional properties of the code can be verified by automatic software verification tools. This certifies fault detection software for a set of bounded data and increases the reliability in practice.


Introduction
Fault detection is an essential part of any complicated and safety-critical system. For years, several methods have been introduced for detecting possible issues in dynamic systems to guarantee normal functionality of the system. In practice, the designer selects one out of several fault detection methods, based on the specifications of the system and the nature of possible faults. Some methods are more suitable for off-line fault detection test. One example is subspace-based detection method, introduced in [1,2]. The method is used for health monitoring of mechanical structures, such as bridges.
Other methods aim at detecting faults online. All observer-based methods belong to this category. The observer or estimator filter provides analytical redundancy for health monitoring of the system, analyzing input-output data and comparing the result with the nominal behavior of the system. Most studies on model-based fault detection develop such approaches. A survey on such methods is provided in [3] (see also [4,5,6,7]). Among those approaches, some are stochastic and the others are deterministic. All those methods are passive in the sense that the detector only monitors input and output data and decides on health of the system. Recently, active methods are introduced that aim at guaranteeing or improving fault detection by designing and injecting auxiliary signals into the system (see [8,9,10,11]). Among all the aforementioned methods, some can be used only in open-loop setup, while the others can be applied to closedloop systems. Fault isolation and estimation is another property that only some of the methods provide (see [12,13,14]). In conclusion, the designer has a broad range of selection and can choose the most suitable method based on all the requirements.
After selecting a proper fault detection method, the designer needs to calculate the design parameters and simulate the method, based on system model, and using software such as Matlab, Simulink, Scicos, etc. A successful simulation result is promising to move on to the next step. Then the method is implemented on the real system. In recent years, digital computers and micro controllers have been developed rapidly. Now, it is economically reasonable to implement control, estimation and fault detection methods in the form of software on digital computers. Therefore, software that already passed simulation tests can be installed on computers or micro controllers connected to the real system. If the real system is complicated and sensitive, a prototype, small model or a physical simulator can be used to test the method before implementing to the real system.
Through the process of design and implementation, several scientists and engineers may collaborate together. The software implementation of control, estimation and fault detection methods can be finalized or be modified by computer scientists and the code created initially by a control engineer might be merged to the other pieces of codes. In the end, the software might be different from what it is supposed to be in the original design, can have bugs and errors and may not satisfy the expectations of the original designer. Some parameters might be changed by trial and error and, finally, there is no mathematical evidence supporting the flawless operation of the implemented method. Even if the code does not undergo any changes, computers work with binary numbers and floating point that computer use are different from real numbers in math. Therefore, there always exist calculation errors and the implemented software is deviated from the theory that supports it. In conclusion, the results are not exactly what we expect from control and signal processing theories. This issue is more crucial for fault detection in safety-critical systems, such as airplanes and helicopters. In the light of evolving software certification requirements, it becomes important to formally specify the correctness of these algorithms. We look for the solution in software verification.
Software verification is already implemented to check the stability of the control systems [15] (see also [16,17]). The aim of control software verification tools is to verify the correct implementation of control methods in the form of codes. For that purpose, software annotations are included in control software so that the software can be readable for computer scientists and be analysed by verification tools. Control properties are expressed by invariant sets to which software variables belong. It makes a bridge for the other scientists who are not familiar with control or signal processing techniques to verify the software. The final aim is to verify the software using verification tools that can read the annotations, evaluate formal methods and certified the proofs at the level of the software (see [18]).
In this research we select three observer-based fault detection methods, capable of detecting abrupt changes in closed-loop systems. We implement the methods in the form of software to monitor a laboratory 3DOF helicopter and show that all the methods can detect some pre-specified fault scenarios. However, it does not guarantee the functionality of the software in any circumstances. Therefore, the question is how to develop formal methods of verification for the software and create a detection software that provides us a higher level of reliability. Properties that have mathematical proofs are translated in formal language, understandable for computer scientists, as well as computers that verify software automatically, and are added to the software as annotations. Hence, those specifications are preserved in software level and can contribute to the validation of a complete system during implementation process.

System modeling and problem formulation
Model-based fault detection methods need the system to be represented by mathematical equations. Continuous-time dynamic systems can be modeled by differential equations. Original models are usually nonlinear, but a linear model of the following forṁ can be obtained around the operating point of the system, where x(t) ∈ ℜ n and u(k) ∈ ℜ m are the state vector and the known input vector at time t, respectively. f (t) ∈ ℜ n f is an additive fault to the system that should be detected. f d (t) ∈ ℜ n d represents all unknown signals to the system that we do not aim at detecting. This signal acts as a secondary fault to the system. No prior knowledge on f (t) and f d (t) is available. Although the methods in this paper are capable of detecting sensor faults, we do not discuss sensor fault detection in that context to avoid complexity. Instead we focus on the correct software implementation. A ∈ ℜ n×n and B ∈ ℜ n×m are state transition and input matrices, respectively. Here, y(t) ∈ ℜ p is the output vector and C ∈ ℜ p×n is the corresponding output matrix. We assume (A,C) is observable. E f determines how the system fault affects the system and E d defines the structure of faults that we do not want to detect. In this paper we consider three problems, namely fault detection, fault detection and isolation and fault estimation. The value of f (t) and f d (t) are zero for nominal (fault-free) system. The aim of the fault detection is to raise an alarm whenever these value differs significantly from zero (faulty system). Note that most unwanted changes in the system that lead to a system matrix change can be represented by signal f (t). Fault detection and isolation considers the case in which the observer detects only particular faults and bypasses the others. We are only interested in detecting f (t). The detector must be as sensitive as possible to f (t) and, at the same time, insensitive to f d (t). Finally fault estimation provides a method to reconstruct f (t) and f d (t).

Observer-based fault detection: informal methods
We consider three different observer-based fault detection methods in this paper. In this section, we briefly summarize the theory of those methods. Those methods have been used for designing fault detection observers for years. However, the original methods are not expressed in the formal language of computer science and software verification. We call them informal methods to comply with computer science terminology. In Section 5 we translate the properties of these methods into formal language.

Output observer design for fault detection
The simplest observer that can be used for fault detection is the output observer. It monitors the outputs of the real system and compares them with those simulated with a nominal model of the system. The material in this section has been explained in detail in most fault detection books, see for example [12,14]. In this approach, no specific strategy is provided for fault isolation. Therefore the observer is sensitive to both f (t) and f d (t), and detects both. The core of the output observer detector is a full-order state observerẋ A simple output observer (3) produces a residual signal, r(t), to compare the estimated output with the measured one Introducing the estimation error, e(t) = x(t) −x(t), we calculate the dynamics of the errorė From (6)- (7), r(t) goes to zero for the nominal system (where f (t) and f d (t) are zero) when the observer matrix L is so chosen that A − LC is stable. In nominal case,x(t) also provides a unbiased estimate for For this simple observer, the only design parameter is L, which should be selected so that the error dynamics is stable. We can use any pole placement method to select L for that purpose. When the observer is implemented as software, it receives input-output data, the residual signal r(t) is calculated online and the norm of this signal is usually compared to a threshold. If the norm of r(t) reaches the threshold a fault alarm is raised. We discuss about it more in Section 5.1.1. The threshold is selected so that small norm faults does not raise an alarm.

Fault detection and isolation using Unknown Input Observers (UIO)
The method introduced in [13] is summarized in this section, with slight modifications. An unknown input observer for the system (1)-(2) is an observer that its state estimation error approaches zero asymptotically, regardless of the presence of the unknown input f d (t) in the system. Several methods have been proposed in the literature to design UIO. The order of the observer might be different from that of the system [13].
Here we assume that the observer and the system are of the same order. The observer is modeled aṡ It has been proved that UIO does not exist if Notice that if the number of fault input channels is bigger than the number of measured outputs, we cannot design a UIO. Suppose that (12) is not true. Assume that e(t) = x(t) − x(t) is the estimation error. Let FH be represented by K 2 and K = K 1 + FH.
Hence we have K = K 1 + K 2 . The error dynamics can be obtained as followṡ In order to have stable error dynamics, we enforce the following conditions and select F to be Hurwitz. Such a selection leads toė(t) = Fe(t) for non-faulty system ( f (t) is zero) and the observation error asymptotically converges to zero. From (14), all we need to stabilize F is to select K 1 using pole placement methods. When (C, A − HCA) is observable, K 1 can be calculated using conventional eigenvalue assignment approaches. No more algebraic manipulations are required. If (C, A − HCA) is not observable but detectable, a particular approach can be used to design K 1 . In what follows, we explain the approach. Note that (C, A − HCA) is detectable whenever it is either observable or non-observable modes are stable.
We can find a similarity transformation matrix P so that (see [19,13]) In that case A 11 is stable if (C, A − HCA) is detectable. We select matrix K 2 p so that the eigenvalues of A 22 − K 2 p C 2 are assigned at desired stable locations. Then K 1 can be obtained as where K 1 p is any arbitrary matrix of proper dimensions. In the end, observer matrices are computed as follows The designed UIO is robust to unknown input f d (t). Hence, we havė If T E f = 0, the additive fault f (t) can be detected.

Fault estimation using sliding-mode fault detector
Consider again the system (1)- (2). It can be rewritten aṡ whereĒ The sliding-mode fault estimator is supposed to estimatef (t). Notice that fault estimation is more complicated than fault isolation. It calculates an estimation of any unknown input signal. We assume that B,Ē f and C are full rank and the number of system faults is smaller than the number of outputs. Also we suppose that any invariant zero of (A,Ē f ,C) is stable. These assumptions guarantee the existence of a slidingmode detector. An sliding-mode detector design approach is introduced in [20]. The following observer is proposed to estimate the states of the system (21)-(22) where, and ν = −ρ(t, y, u) D 2 P 2 e y P 2 e y +σ if e y = 0 0 otherwise.
Here, D 2 , A 12 , A 22 , A s 22 , ρ(t, y, u), P 2 and T o must be selected so that e y goes to zero in finite time. σ is a small positive scalar added to the denominator of the discontinuous part of the ν to reduce the chattering effects [20]. The corresponding sliding surface is {e ∈ ℜ n |Ce = 0}. Also we suppose ρ(t, y, u) is selected so that [21] f (t) < ρ(t, y, u).
In practice, ρ can be selected as a positive constant scalar [20]. Here, we briefly explain the design procedure. It can be shown that there exists a similarity transformation matrix, T o , that can transform system (21)-(22) intȯ where A 11 has negative eigenvalues. For (32)-(33) we use the observer belloẇ in which A s 22 is a design matrix that must be Hurwitz. P 2 in (30) is a Lyapunov matrix for A s 22 that guarantees quadratic stability of the error dynamics of the observeṙ Suppose that sliding motion is taken place and consequently e y (t) = Ce(t) = 0 andė y (t) = 0. Considering (38)-(39), and from the fact that A 11 is stable we obtain lim t→∞ e 1 (t) = 0 and From (41), we propose the residual Note that this residual not only does detect the fault, but also its value is an estimate of the fault.

Experimental results
To show that the methods presented in this paper are efficient in practice in detecting faults, we implement them in the form of software to detect some predefined faults to a laboratory 3DOF helicopter. The helicopter is shown in Figure 1. A linear model of the system is provided by the manufacturer that is derived from highly nonlinear differential equations of the system. The order of the system is six and all its poles are at zero. The linear model of the system is given in Appendix. This model comes with an LQR controller. In this research we use that controller. Details of controller design is given in [22]. Therefore we study the methods in a closed-loop setup.

System fault in closed-loop setup
In general, feedback attenuate the effect of a fault in the system (see [8,23,24]). Therefore, it is harder to detect faults in a closed-loop setup. The controller is already designed, and we access the input data that the controller sends to the helicopter, as well as the outputs of the system measured by sensors. In the first experiment, three independent faults affect the system consecutively. Each fault lasts 10 seconds and then the system returns to its normal operating condition for 10 seconds. Fault 1 is a horizonal force implemented to the helicopter that deviates it from the operating point ( Figure  2). It mainly changes travel angle, however it affects pitch angle inevitably. A small mass is put on one of the propellers to make Fault 2 ( Figure 3). This small mass does not change the elevation angle but alters the pitch angle. Finally, Fault 3 is made by a heavy mass which is put on the main arm. This fault changes the elevation angle ( Figure 4). The system operates in nominal mode in the beginning of the experiment. After 10 seconds Fault 1 takes place. This fault lasts for 10 seconds and then the system returns to the nominal mode for 10 seconds. Fault 2 happens at t=30 sec. The system returns to the nominal mode again for 10 seconds. At t=50 sec. fault 3 takes place and lasts till the end of the experiment. Figures 8-10 depict the residual signals of three detectors designed using the second method, UIO, to detect faults on travel angle, peach angle and elevation angle, respectively. Three different detectors are designed using UIO method. In each design, only one of the faults is supposed to be detected and the others are bypassed. It can be seen that all the three faults are detected while each detector is sensitive only to one of the faults. Hence, fault isolation requirements are satisfied. From the figures, it seems that the first method provides isolation in some extent while not as good as the second method. However the acceptable result is obtained by trial and error while the second method is more systematic for this purpose.      In the second experiment, we try to detect loss of control during flight [25]. One reason that such faults may take place is that the performance of the actuators degrades. This fault changes the behavior of the system and the steady state of the system. Note that we do not design new observer detectors, but try to detect the loss of control effects using the observers designed for the first experiment. As the steady state values change due to this fault, we expect it to be detected by some of those observers. To model the loss of control effects, we send the control commandū(t) to the system in place of u(t) where [25]ū (t) = Xu(t). The second experiment takes 30 seconds. In nominal mode X = I. After 10 seconds loss of control occurs and X changes to For the rest of the experiment X does not change. Again, experiment is repeated using the three fault detection methods. Figures 13-15 show the three residuals produced by the output observer method. The second and the third residuals clearly show a change while the effect of the change in the third residual disappears in steady state.    We remind that chattering effect, which is a serious problem in sliding-mode control, is not very critical in fault detection. While the chattering in control may cause problems for actuators, the residual in fault detection is merely used to decide on the occurrence of the faults.
Remark 4.1 In this experiment, the real input u(t) is provided to the detector whilē u(t) is sent to the system. The matrix X models an actuator fault degradation which is supposed to be inside the system. However, the controller calculates the control signal correctly and provides it to the detector.

Fault detection software verification: towards formal methods
The theories supporting three fault detection methods are presented in Section 3. The methods are successfully applied to a real system in Section 4. However, those methods are implemented as softwares and there always exist a semantic gap between theory and real software implementation. The methods in Section 3 should be implemented, either in graphical programming language tools such as Simulink or as computer codes in computer languages such as Matlab or C. Due to the different real life restrictions and computation errors, there might be a difference between implemented method in software form and the ideal method in theory. Simulations and practical tests are used to show that the methods work well. However, we cannot test the system for all possible conditions, initial values and faults. For that reason, we are interested in software verification approaches to include original design properties in the software and verify the correct operation of the software for all possible scenarios, based on the theory, and at least based on the model of the system used in the original design. We aim at annotating the software so that an expert or a machine can track the operation of the software and verify that the original design criteria are satisfied at software level. The idea developed in [15] to formally document the stability of closed-loop systems is extended to fault detection methods in this section. Here, we focus on the fault detection methods introduced in Section 3

Output observer
The first system specification we must document in the software is the stability of the detector, i.e the variables of the observer software stay bounded over time. We need to verify the stability of error dynamics in (6)- (7). In addition, we need to check that the fault detection duty of the software is performed correctly. More precisely we need to show that 1. Observer stability is guaranteed: the error dynamics are stable, i.e. e(t) in (6) stays around origin when system is in nominal mode and remains bounded in faulty mode.
2. Fault detection performance predicted by theory is guaranteed: the residual, r(t), correctly detects the fault. In other words the residual is not around zero if the fault signal (for this method including both f (t) and f d (t)) passes a predefined threshold. On the other hand r(t) stays around zero if the fault does not reach the threshold.
Here, we start from the informal method in Section 3.1. We translate its properties into a formal language, compatible with software verification tools. Here, we assume that the closed-loop system is stable, and we have already verified the stability of the closed-loop system using the method in [15]. The result is that y(t), and u(t) accordingly, remain bounded in (3)-(5). Thus, we only verify that error dynamics, e(t), is bounded. This assumption is necessary, asx(t) blows up if y(t) goes to infinity while e(t) may remain bounded.
One approach to examine the stability of dynamic systems is to use Lyapunov theory, which is shown, on the other hand, to be a very efficient tool in control software verification (see [15]). We can check the stability by calculating the place of system poles if the system is linear, as well. However, it is preferred for software verification purposes to express desired properties in the form of invariant sets to which software variables must belong. We remind that in software implementation of the fault detection filter, observer state vectorx(t) is a software variable (or a set of variables). Also, having the model of the system, a piece of code can represent the operation of the nominal system, with x(t) a software variable. This code is synchronised with the detection filter (see closed-loop verification in [15]).

Steady state properties
According to the properties above, there are two modes of the detection filter with respect to the observed system that we are mainly interested in to verify: 1. The detector is stable (e(t) is bounded), the system is in nominal mode (fault signal is small enough, in terms of norm) and it is correctly detected (r(t) is smaller than the predefined threshold).
2. The detector is stable (e(t) is bounded), the system is faulty mode (fault signal is big enough) and it is correctly detected (r(t) is larger than the predefined threshold).
Both these properties are related to steady state specifications of the system. Other specifications might be important for the designer that are related to transient specifications. We discuss them in Section 5.1.3. Consider a Lyapunov function V (t) = e T (t)Pe(t) with a proper positive definite P. We know that V (t) decreases along system state trajectories andV (t) < 0. The following ellipsoid set is the invariant set in which e(t) resides if the error dynamics are stable for ∀t ∈ ℜ, where ζ ≥ 0 is a scalar. ζ is related to the threshold on r(t). There are different ways to define a threshold on the residual. We may bound the peak value, the norm, the average norm over a time interval, etc. of r(t) (see [12]). Consequently, fault alarm is raised if r(t) > r th where . can be any norm, and r th is the threshold. In addition to the common norms in robust control theory, we are interested in the peak amplitude of the residual vector. Also in(43) we deal with peak value. We use the peak-norm which has been used in fault detection studies [12] Notice that r(t) = Ce(t), namely we compare only the sensor measurements (and not the other quantities that are not directly measured) with the estimated values by the observer. We need to translate this threshold in the state space, define the reachable set of system trajectories corresponding to the threshold, and select ζ . To this end, we need to find the system norm of the detector, π = supf (t) =0 r(t) / f (t) wheref (t) is defined in (24). This can be calculated using LMI's, and depends on the norm that has been used to define the threshold. Using π and r th we can find the maximum norm of the augmented fault signalf (t) that is allowed by the initial design so that an alarm is not raised. So far, we know the set of fault signals that are tolerable by the detection observer (do not raise an alarm). The next step is to findπ = supf (t) =0 P 1 2 e(t) 2 / f (t) solving some LMI's. Finally ζ is obtained knowingπ and the maximum norm off (t) that does not raise an alarm.
For the faulty mode, we can introduce another ellipsoid invariant set around the new equilibrium point. However, we do not know where the new equilibrium point is, as the fault signals are assumed to be completely unknown. But in practice, f (t) and f d (t) are norm bounded. Suppose that f (t) <σ . We introduce the invariant set below In (45)ζ isζ and f (t) <σ .
Hence, we have introduced two ellipsoid sets. As far as V (t) ∈ E n for ∀t ∈ ℜ, i.e. E n is an invariant set, the system is in nominal mode and the detector is stable. Whenever V (t) ∈ E f for ∀t ∈ ℜ so that ∃t,V (t) ∈ E n , i.e. E f be an invariant set while E n is not, the system is in faulty state and the detector is stable. We include all this information in the software as annotations. Other engineers who test the code can understand how the state space variables are supposed to behave in terms of invariant sets, without verifying the place of poles directly. If the annotations are expressed in a standard format, software verification tools can check it and certify that the software works well according to the original design.
To conclude this section we propose following Lemmas, which helps to calculate ζ andζ . More results can be found in [26,27] Lemma 5.1 given the systeṁ for a given constant ρ 1 > 0 where P 1 is a positive definite symmetric matrix we have if there exist Q 1 > 0 so that Also if y(t) = Cx(t) then for a givenρ 1 > 0 if there existQ 1 > 0 so that Lemma 5.2 given the systeṁ where for a given constant ρ 2 > 0 where P 2 is a positive definite symmetric matrix we have if there exist scalars υ > 0 ϕ > 0 and a matrix Q 2 > 0 so that Also for a givenρ 2 > 0 if there existῡ > 0φ > 0 andQ 2 > 0 so that Lemma 5.3 given the systeṁ for a given constant ρ 3 > 0 we have if there exist Q 3 > 0 so that

Instability of the detector
For the verification of commercial software, the properties expressed in Section 5.1.1 are certified. It is obvious that the final software product guarantees the stability and correct performance. There are other modes that are undesired, however. We specify those modes to help the test engineers to detect errors of the software, before finalizing the product. Based on Lyapunov theory for linear systems, the detector is unstable if E f is not invariant.

Further analysis and transient mode
Verifying that E n or E f is invariant ensures the steady state properties of the detection filter, as we discussed in Section 5.1.1. However, transient mode, namely changing from nominal to faulty mode, cannot be completely analysed. In this section, other properties obtained from Lyapunov theory and the theory of linear systems control and observation are used to complete the documentation of the software. We aim at verifying the mode of the system at each time instant. For instance if V (t) ∈ E f − E n at time t, we cannot infer whether the system is faulty or the detector is unstable using the material in in Section 5.1.1. We need to prove that ∀t,V (t) ∈ E f to conclude the system is faulty. In this section, we aim at concluding some results on any state trajectory point that software variables reach, before investigating the entire set. Let us introduce the following new variable According to the original design requirements, the system is in nominal mode if and only if θ (t) < θ th . It is faulty if and only if θ (t) ≥ θ th . Now suppose that system trajectory is in E f − E n and the software verification tool is trying to verify whether or not E f is invariant. Assume, θ (t) < θ th ; it means the system is in nominal mode, and therefore V (t) ∈ E f − E n for some t show that the detector is unstable and E f cannot be invariant. The verification tool should be able to find V (t + τ) ∈ E f for some τ continuing the same trajectory. If such an example does not exist, there is an error in the code. Note θ th depends on the threshold on fault signal. If we know the fault signal threshold on each fault input channel, the exact threshold can be calculated. If the norm of the fault vector is available, un upper bound can be obtained from the triangle inequality. Further results can be deduced from the derivative of the Lyapunov function.V (t) can be used to analyse the correct operation of the detector in some modes. For instance, if V (t) ∈ E n and and θ > θ th , then we must have V (t) > ε V for some positive ε V . Otherwise some implementation errors exist in the code. A summary of all possible modes is provided in Table 1. Here, "convergence issue" refers to the instability of the observer. In this table we suppose that faulty system will not return to nominal mode, as it is usually assumed. Removing this assumption leads to a more complected table and the derivative of the Lyapunov function should be used to distinguish between "returning to nominal mode from faulty mode" and the "convergence issue".  Figure 21 shows the space of error and the nominal and faulty regions. The order of the system is two, in order to be able to draw the error space in two dimensions. One property that is important in transient response of linear systems is settling time t s . In safety-critical systems, it is of great importance to verify that the fault detection mechanism works fast enough to detect fault before they lead to catastrophic consequences. Settling time is the time elapsed from the application of a step input to the time at which the output has entered and remained within a specified error band, usually symmetrical about the final value (see [28]). The same concept can be introduced and be verified for the detection observers. We are interested in testing the settling time to verify that the observer is fast enough, according to the original design. The settling time can be computed as described in [28]. Here, we translate the idea in the space of errors and based on invariant sets for verification purposes. As such, it will be possible to certify that property in the code and track possible changes in settling time due to the modifications that can be possibly made by each line of the code. Settling time depends on the place of the observer poles. For each pair of input-residual, we can find the corresponding settling time and the steady state value of the error, e s . Applying such a unit step input as fault signal, the following set must become invariant after t s seconds.
Here, ζ t is selected so that the projection of E t on the corresponding residual direction is equal to the error bound around the steady state of the residual after settling time. Figure 22 shows how to verify the settling time. Note that the settling time can be calculated from the place of dominant poles of the detection filter. On the other hand, we can express these transient time response properties in the form of LMI's, [29,30]. An easier way to obtain an upper bound on settling time for multi input multi output systems is to calculate the settling time from an input to all states and select the maximum. should be implemented to approximate the derivative, where a is a small scaler and s is Laplace transform variable.
It is important to know that software verification is an approach to check the mathematical proofs in the software level. If some properties of a dynamic system seems to be correct in some cases in simulation or practical tests but concrete proofs does not support the general case, software verification cannot automatically prove it. The method of output observer implemented for fault detection uses a general purpose observer to detect additive faults and does not claim on fault isolation. Although one may show isolation properties by simulations or practical experience, as we do in Section 4 for our particular application and fault scenarios, the method originally does not provide proofs. Consequently, fault isolation is not verified for this method. On contrary, UIO provides fault isolation properties, as we discuss in Section 5.2. Therefore, the proof can be implemented for software verification. This is an important advantage of using UIO, even though output observers give good results in practice.

Annotation of the software implemented on the helicopter
Here we consider the last fault scenario described in Section 4.1. The following P is used for the verification purpose Assume the threshold on the 2-norm of the residual is selected as r th by the designer. Using Lemma 5.3 we can compute the H ∞ norm of the observer. To compute the norm we need to solve LMI's by YALMIP [31]. Hence the maximum ρ 3 that satisfies (59) is 0.0086 and the corresponding Q 3 obtains as bellow The upper bound on settling time for this observer is 0.8479sec.

Unknown input observer
The stability of the fault detection filter is the first property, again, that we need to document in the software in a formal manner. Also, we need to show that the software is capable of detecting unwanted inputs. However, fault isolation should be consider in addition to the fault detection property, unlike for output observer detectors in Section 5.1. Here, we summarize the main properties we need to be verified: 1. Stability is guaranteed: the dynamics of the error remains bounded whether the system is in nominal mode or in faulty mode.
2. Fault detection performance is guaranteed: the detector works correctly, i.e. the residual r(t) is around zero if fault f (t) is around zero and deviates from zero if f (t) is greater than a predefined threshold.
3. Fault isolation is certified: the faults that we do not want to detect using the filter, f d (t), have no (or negligible) influence on r(t).
As in Section 5.1, we assume that the closed-loop system stability is verified and y(t) and u(t) stay bounded. Again, we use Lyapunov theory to translate the stability property into the formal language. For the verification of fault detection performance, we need to show that a fault signal that is strong enough results in a fault alarm. These two parts are similar to the verification of output observer in Section 5.1. We briefly discuss them, without going through the details. The last property, the verification of fault isolation, is however new and we discuss it in detail. In the software implementation of the detector, z(t), u(t), y(t) are the variables of detection filter software. Also, the system model can be implemented as a piece of code with x(t) a software variable. These two softwares are synchronized and work together.

Fault isolability
We need to introduce a new variable, θ (t), to verify fault isolability. The same variable will be used for further analysis as in Section 5.1.3, later. To explain the reason, we need to return to the error dynamics for UIO. Consider equation (13) and the following inequalities where ε ≥ 0 is a small scalar. According to the discussions in Section 3.2, ε must be equal to zero for an error-free system. However, software variables are floating numbers and not real numbers and the right hand of (14) is never exactly zero. Also computation errors always exist in the software implementation. Hence, we introduce an error tolerance for computational errors by ε. These conditions are added to the code of the detector as annotations, before verifying the stability. If (64)-(66) are satisfied, only fault f (t) and f d (t) are the major exogenous inputs to the error dynamics. As the fault signals are unknown, we are not able to evaluate the those terms in (13). However, it is possible to work with θ (t) defined bellow Assume that (64)-(66) are satisfied. To cancel out the effect of f (t) on θ (t), consider where (E f T ) ⊥ is the left annihilator of E f T . We need to verify that through the code. Here, (68) guarantees that the system is insensitive to f d (t). Note that (64)-(66) and (68) must be satisfied in all modes of the system and the detector, in order to guarantee the isolability. If we guarantee that the effect of f d (t) on the error dynamics is negligible, then the rest of verification process is similar to the verification of output observer. We briefly explain it bellow.

Steady state properties
In this section, we suppose that fault isolation conditions, (64)-(66) and (68), are satisfied. We need to document and verify two main operating modes 1. The detector is stable (e(t) is bounded), the system is in nominal mode ( f (t) is small enough in terms of norm) and it is correctly detected (r(t) is smaller than a predefined threshold). Isolability condition is satisfied (r(t) is not affected by f d (t)).
2. The detector is stable (e(t) is bounded), the system is in faulty mode ( f (t) is not small enough) and it is correctly detected (r(t) is larger than the predefined threshold). Isolability condition is satisfied (r(t) is not affected by f d (t)).
To verify the stability of the error dynamics we use Lyapunov theory, as in previous section. We suppose that the fault f (t) acts as an step signal. But, the magnitude of the signal is unknown. It means that the equilibrium point of the system changes because of the fault. However, we do not have any information about the new equilibrium point. Considering a Lyapunov function V (t) = e T (t)Pe(t) for a positive definite P, we can show that the e(t) remains in a predefined invariant ellipsoid for ∀t ∈ ℜ, if the detector is stable and the system is in nominal mode. Here, ζ ≥ 0 is a scalar.
Assuming that f (t) < σ . We introduce for the faulty mode. In (70)ζ is If E n is invariant, the system is in nominal mode and the observe is stable. Whenever V (t) ∈ E f is invariant while E n is not, the system is faulty and the detector is stable. See the details given in Section 5.1.1. Figure 21 is still valid for UIO, assuming that isolation requirements are satisfied.

Instability of the detector
If for some t we have V (t) ∈ E f and the fault isolation conditions are satisfied, the dynamics of error and consequently the detector are unstable.

Further analysis and transient mode
Assume isolability conditions are satisfied. For further analysis we make use of θ (t) comparing its norm against a predefined threshold as in Section 5.1.3. We can also useV (t). The approach is the same and we do not repeat it. Transient mode is again specified by settling time.

Annotation of the software implemented on the helicopter
Even if all computations are correct inside the code, (E f T ) ⊥ is not usually zero due to the computation errors in null space. In this example the order of the error is 10 −15 . This error is greater than any error in (64)-(66). In order to be sure that such an error will not propagate in the code and will not affect the isolability we select ε = 10 −10 . Calculating the other parameters is similar to those for the output observer and we do not give the details.

Sliding-mode fault detector
Sliding-mode observers are nonlinear. Some of nice properties that we can conclude for linear observers cannot be easily extended to sliding-mode observers. We discuss the properties that we can verify, in this section.
We need to document and verify the stability and correct estimation of the detector. Correct fault estimation needs that error dynamics reside on the sliding surface. For the sliding-mode observers, we need to verify the following properties 1. The detector is stable (e(t) is bounded), 2. Sliding motion takes place on sliding surface and the error dynamics states remain on the sliding surface.
We need to show that an sliding motion takes place on in finite time and the dynamics of error in (38)-(39) are stable. If these two conditions are satisfied, we can conclude (41) is correct, and consequently (42) is an estimation of the fault. Based on the proofs in [20] the following invariant ellipsoids are considered for the verification of the sliding-mode method for sufficiently small predefined scalars α > 0 and β > 0, where for Q 1 ∈ ℜ (n−p)×(n−p) and Q 2 ∈ ℜ p×p be symmetric positive definite matrices. We need the linear transformation T o to obtain x 1 (t) from x(t). Details are given in [20]. It has been shown that sliding motion takes place on sliding surface in finite time. We show that time interval by t s . An upper bound on the time error dynamic need to reach the sliding surface is given in [20].
If E e is an invariant set, and E s is invariant after t s , sliding motion takes place, dynamics of error is stable and consequently the detector can detect faults f (t) < ρ(t, y, u), according to the theory. Figure 23 shows the trajectories of dynamics of error and corresponding invariant sets.
Note that stability of the dynamics of error is necessary but not sufficient condition for correct fault detection. Sliding motion must take place as well. Hence, both E e and E s should remain invariant sets.

Annotation of the software implemented on the helicopter
Assume Q 1 is an identity matrix. The other parameters and Lyapunov matrices are obtained as bellow

Discussions
Three observers introduced in this paper are different from the view point of software documentation and verification. If the only purpose is the detection of any unknown input to the system, all three methods can be verified. However, if we consider fault isolation in the software level, the first method, output observer, cannot be verified, thought isolation might be achieved in particular cases in practice by trial and error.
In that regards, UIO and sliding-mode approaches are superior. Fault isolation and estimation properties can be verified as it is shown in Sections 5.1 and 5.3. Another point that should be considered is the possibility of extending the results to discrete-time systems. Although we implement methods in continuous-time and Simulink provides the possibility of implementing them to the helicopter model, all digital computers work in discrete-time in practice. As long as the sampling frequency is high, continuous-time behavior is simulated. However, it is sometimes proffered to design the detectors in discrete-time by sampling input-output data and using a discrete-time model of the system. As such, the performance will not depend on the sampling frequency. The theory of output observer design and UIO design can be easily extended to discrete-time systems. However, it is not straightforward to do the same for sliding-mode observers. To the best of our knowledge, the method in Section 3.3 is not extended for discrete-time systems, yet. On the other hand tuning the parameter ρ is not easy in practice when we design sliding-mode observers. That affects the correct estimation of the fault claimed by sliding-mode method. If this parameter is not selected correctly by the original designer, fault estimation reduces to isolation, i.e. the reconstructed fault estimate does not show the correct magnitude of the fault. Note the main advantage of sliding-mode method is to estimate the fault while the other two methods only claim to detect it. The linear structure of UIO, which is simpler than the nonlinear sliding-mode detector, is another advantage that should be consider if only fault isolation is required.

Auto-coding and auto verification of the software
In previous sections, we translated traditional observer-based methods into formal properties that should be annotated in the fault detection software. Annotating the software, software semantics are expressed inside the code, usually in the form of invariant sets to which software variables belong. In [15], it is explained how to annotate a controller software. State variables belong to an invariant ellipsoid. Each line of the code may or may not change the ellipsoid. If the code makes any change to the ellipsoid, the change is expressed as annotations. The annotations are based on Hoare logic proposed first by Charlie Hoare [32]. For each line of the code, some pre-conditions and some post conditions are provided. Pre-conditions are supposed to be true before the execution of that line. They might be concluded from previous lines of the code or might be external assumptions. Post-condition must be true after the execution of the line. A verification tool certifies that the post-condition is true if the pre-condition is true if the corresponding line of the code is executed.
There are two main changes that a piece of code may apply to invariant sets. Firstly, it may perform a linear transformation on the variables. As an example, consider the case in which system states are multiplied by sytem matrix, A. Secondly, the code may concatenate two invariant ellipsoids. This operation leads to a new invariant ellipsoid. As an example, consider the case that bounded inputs are added to bounded system states. In [15], S-procedure is used to calculate the resulting ellipsoid. Annotations express how these two main operations change invariant ellipsoids.
We need to express the annotations in a standard format so that it can be read by standard verification tools. To unify the annotations, C Specification Language (ACSL) [33] can be used. In Table 2, we have a piece of C code that assigns the square of the variable x to x.
Notice the logic predicates x <= 0 and x >= 0 right before the piece of code denoted by the symbols "@ require" and "@ ensures". These are annotations expressed in ACSL [33]. The ACSL keyword "require" denotes a pre-condition. The "ensures" keyword denotes the post-condition.
Another example is given in Table 3. This example corresponds to a simple discretetime state space system of order one. The symbols "@ assumes" shows an "external Table 2: Annotated code sample using ACSL / * @require x ≤ 1 @ensures x ≤ 2 * / { x=2*x; } assumption" on u, i.e. the input to the system. Note that the pre-condition " x * x <= 1" might be concluded from previous lines of the code, while the bound on u is not imposed by the code. If the states are quadratically bounded before the loop, the infinite loop will not change the property and system states must remain in the original ellipsoid. An example of annotated codes for fault detection and control software is provided in [34]. Table 3: Annotated code sample using ACSL / * @assumes u * u < 1; @requires x * x <= 1 @ensures x * x <= 1 * / { while (1) { x = 0.5 * x + 0.5 * u; } } After auto-coding the software, we need to verify the code. For that purpose, Frama-C/WP platform [35] [36] can read the annotations produced by ASCL and converts them to logic properties. Such logic statements, then are processed by Why3 tool [37] which converts these properties into a format readable by the interactive theorem prover PVS [38]. PVS is the tool that certifies the correctness of the software.

Conclusions
In this research we focus on software implementation of the observer-based fault detection methods. Mathematical proofs that support correct operation of the observers are translated in a formal language based on invariant sets and are annotated in software implementation of the observers. Therefore, design specifications and properties can be understood by computer scientists as well as software verification tools. Those tools can certify the original design requirements by tracking software variables that represent observer error states. Only properties that are supported by mathematical proofs are annotated. Hence, properties that are achieved by trial and error, seem correct without mathematical proof, cannot be verified. We provide the details of the material that should be documented in the software for three different observer-based fault detection methods. Those methods are proposed for fault detection, isolation and estimation in theory. The methods are implemented on an experimental lab helicopter system. It is shown that all the methods work fine in practice, detecting a set of pre-defined fault scenarios. However, software implementation of each method is different. Successful simulation results and even practical tests does not certify that the observer works fine for all possible conditions. However, software verification techniques can certify the properties that are supported by theory and are translated in the formal language.