Failsafe Mechanism Design of Multicopters Based on Supervisory Control Theory

TL;DR

This paper introduces a failsafe mechanism for multicopters using supervisory control theory, modeling safety requirements as automata, synthesizing supervisors, and implementing decision codes to enhance safety during flight failures.

Contribution

It presents a novel supervisory control-based method for designing multicopter failsafe mechanisms, including modeling, supervisor synthesis, and implementation strategies.

Findings

Successfully models multicopter safety requirements as automata

Synthesizes supervisors to prevent unsafe states

Provides implementation approach for real-time decision-making

Abstract

In order to handle undesirable failures of a multicopter which occur in either the pre-flight process or the in-flight process, a failsafe mechanism design method based on supervisory control theory is proposed for the semi-autonomous control mode. Failsafe mechanism is a control logic that guides what subsequent actions the multicopter should take, by taking account of real-time information from guidance, attitude control, diagnosis, and other low-level subsystems. In order to design a failsafe mechanism for multicopters, safety issues of multicopters are introduced. Then, user requirements including functional requirements and safety requirements are textually described, where function requirements determine a general multicopter plant, and safety requirements cover the failsafe measures dealing with the presented safety issues. In order to model the user requirements by discrete-event systems, several multicopter modes and events are defined. On this basis, the multicopter plant and control specifications are modeled by automata. Then, a supervisor is synthesized by monolithic supervisory control theory. In addition, we present three examples to demonstrate the potential blocking phenomenon due to inappropriate design of control specifications. Also, we discuss the meaning of correctness and the properties of the obtained supervisor. This makes the failsafe mechanism convincingly correct and effective. Finally, based on the obtained supervisory controller generated by TCT software, an implementation method suitable for multicopters is presented, in which the supervisory controller is transformed into decision-making codes.

Equations

$$\mathbf{G}=\left(Q,\Sigma ,\delta ,q_0,Q_m\right)$$

$$L\left(\mathbf{G}\right)=\left\{s\in {\Sigma }^{\ast }|\delta \left(q,s\right)!\right\}$$

$$L_m\left(\mathbf{G}\right)=\left\{s\in L\left(\mathbf{G}\right)|\delta \left(q_0,s\right)\in Q_m\right\}\subseteq L\left(\mathbf{G}\right).$$

$$\Sigma ={\Sigma }_c\dot{\cup }{\Sigma }_u$$

$$\begin{array}[c]{l}L_{m}\left(\mathbf{S}\right)=\sup\mathcal{C}\left(\mathbf{E\cap}L_{m}\left(\mathbf{G}\right)\right)\subseteq L_{m}\left(\mathbf{G}\right)\\ \overline{L_{m}\left(\mathbf{S}\right)}=L\left(\mathbf{S}\right)\end{array}$$

$$\mathbf{EVENTS}=\mathbf{allevents}\left(\mathbf{PLANT}\right)$$

$${\mathbf{E}}_j=\mathbf{sync}\left({\mathbf{E}}_j,\mathbf{EVENTS}\right).$$

$$\mathbf{E}=\mathbf{sync}\left({\mathbf{E}}_1,{\mathbf{E}}_2,\cdots {\mathbf{E}}_{25}\right).$$

$$\mathbf{S}=\mathbf{supcon}\left(\mathbf{PLANT},\mathbf{E}\right).$$

$$1$$

$$k=0;$$

Full text

Keywords: Multicopter, failsafe mechanism, supervisory control.

I Introduction

Multicopters are well-suited to a wide range of mission scenarios, such as search and rescue [2], [3], package delivery [4], border patrol [5], military surveillance [6] and agricultural production [7]. In either pre-flight process or in-flight process, multicopter failures cannot be absolutely avoided. These failures may abort missions, crash multicopters, and moreover, injure or even kill people. In order to handle undesirable failures in industrial systems, a technique named Prognostics and Health Management (PHM) is presented [8]. As shown in Figure 1, an integrated PHM system generally contains three levels: monitoring, prediction and management [9]. On the one hand, the monitoring and prediction levels assess the quantitative health of the studied system, where some quantitative indices are introduced to measure system health, such as residuals [10]-[12], data features [13], [14] and reliability-based indices [15]-[18]. On the other hand, the management level imports the quantitative health results from the monitoring and prediction levels, and then responds to meet qualitative safety or health requirements. In our previous paper [19], multicopter health is quantitatively evaluated in the face of actuator failures. This paper studies a safety decision-making logic by Supervisory Control Theory (SCT) to guarantee flight safety from a qualitative perspective.

In the framework of multicopters, guidance, attitude control, PHM, and other low-level subsystems work together under the coordination of a high-level decision-making module [20]. In this module, a failsafe mechanism is an important part. It is a control logic that receives information from all subsystems to decide the best flight maneuver from a global perspective, and send flight instructions to low-level subsystems [21]. However, current academic literature covering failure-related topics of multicopters mainly focuses on fault detection techniques [22]-[26] and fault-tolerant control algorithms [27]-[32], which belong to a study of low-level subsystems. For the study of the high-level decision-making module, most research focuses on path planning [33]-[35] and obstacle avoidance [36], [37] of an individual multicopter, or PHM-based mission allocation of a multicopter team [6], [38], [39]. However, few studies have focused on the failsafe mechanism design of an individual multicopter subject to multiple potential failures. References [40], [41] proposed an emergency flight planning for an energy-constrained situation. Reference [42] proposed a failsafe design for an uncontrollable situation. Reference [43] designed multiple failsafe measures dealing with different anomalies of unmanned aerial vehicles. Nevertheless, that research only considers certain ad-hoc failsafe mechanisms for certain faults or anomalies, and so far does not present a comprehensive failsafe mechanism for a multicopter. In current autopilot products (for example, DJI autopilot [44] and ArduPilot [45]), there exist comprehensive failsafe mechanisms to cope with communication, sensor and battery failures, but such mechanisms are either proprietary, or can be accessed only in part. Moreover, as far as the authors know, these failsafe mechanisms are mainly developed and synthesized according to engineering experience. As a result, such a development process lacks a theoretical foundation; this will inevitably lead to man-made mistakes, logical bugs and an incomplete treatment. Motivated by these, this paper first summarizes safety issues and user requirements for multicopters in the semi-autonomous control manner as comprehensively and systematically as possible, and then uses SCT of Discrete-Event Systems (DES) to design a failsafe mechanism of multicopters.

SCT [46], [47], also known as Ramadge-Wonham (RW) theory, is a method for synthesizing supervisors that restrict the behavior of a plant such that as much as possible of the given control specifications are fulfilled and never violated. Currently, SCT has been developed with a solid theoretical foundation [48]-[50], and it has been successfully applied to practical systems such as flexible manufacturing systems [51]-[53]. Thus, this paper formalizes the problem of failsafe mechanism design as a DES control problem. The solution procedure is shown in Figure 2. In order to obtain the expected failsafe mechanism, the following steps are performed: 1) define related modes and events by studying the user requirements (including functional and safety requirements); 2) model the multicopter plant by transforming the functional requirements to an automaton with defined modes and events; 3) analyze the safety requirements by taking the defined modes and events into account, and transform the safety requirements to automata as control specifications; 4) synthesize the supervisor by TCT software; 5) implementation the failsafe mechanism based on the obtained supervisor.

The contributions of the paper mainly lie in two aspects.

• •

First, this paper introduces SCT into a new application area. The proposed SCT based method in this paper is a scientific method with solid theoretical foundation to design the failsafe mechanism of multicopters. In the field of aircraft engineering, especially of multicopters and drones, traditional design methods are based on engineering experience. The failsafe mechanism obtained by these methods may be problematic (for example, the failsafe mechanism may contain unintended deadlocks), especially when multiple safety issues are taken into account. Compared to existing empirical design methods, the proposed method can guarantee the correctness and effectiveness of the obtained failsafe mechanism owing to the properties of supervisors. This is an urgent need for multicopter designers and manufacturers.

• •

Second, for the application of SCT, this paper emphasizes the modeling process of the plant and control specifications with a practical application, rather than developing a new theory of SCT. We believe this work is important to both the development of SCT research and practical engineering, because SCT is presented with complex mathematical terminology and theory which many engineers may not understand. Motivated by this, this paper presents the procedure of applying SCT to an engineering problem, from requirements described textually, to specificarions in form of automata, then to a synthesized supervisor and finally to implementation on a real-time flight simulation platform of quadcopters developed by MATLAB. In addition, we present three examples to demonstrate the potential blocking phenomenon due to inappropriate design of control specifications. From the perspective of practitioners, this paper can be a guide for engineers, who are not familiar with SCT, to solve their own problems in their own projects by SCT and related software.

The remainder of this paper is organized as follows. Section II presents preliminaries of SCT for the convenience of presenting the subsequent sections. Section III lists some relevant safety issues of multicopters. Also, user requirements including functional requirements and safety requirements are textually described. In order to transform the user requirements to automata, several multicopter modes and events are defined in Section IV. On this basis, a detailed modeling process of the multicopter plant and control specifications is presented in Section V, where functional requirements determine a general multicopter plant, and safety requirements are modeled as control specifications. Then, TCT software is used to perform the process of supervisor synthesis. Section VI illustrates three examples to demonstrate some possible reasons leading to a problematic supervisor, and gives a brief discussion about the scope of applications and properties of the used method. Section VII shows an implementation process of the proposed failsafe mechanism on the platform of MATLAB and FlightGear. Section VIII presents our conclusion and suggests future research.

II Preliminaries of Supervisory Control Theory

As SCT is well established, readers can refer to textbooks [46], [55], [56] for detailed background and knowledge. This section only reviews some basic concepts and notation.

In RW theory [46], [47], the formal structure of DES is modeled by an automaton (generator)

[TABLE]

where $Q$ is the finite state set; $\Sigma$ is the finite event set (also called an alphabet); $\delta:Q\times\Sigma\rightarrow Q$ is the (partial) transition function; $q_{0}\in Q$ is the initial state; $Q_{m}\subseteq Q$ is the subset of marker states. Let $\Sigma^{\ast}$ denote the set of all finite strings, including the empty string $\epsilon$. In general, $\delta$ is extended to $\delta:Q\times\Sigma^{\ast}\rightarrow Q$, and we write $\delta\left(q,s\right)!$ to mean that $\delta\left(q,s\right)$ is defined. The closed behavior of $\mathbf{G}$ is the language

[TABLE]

and the marked behavior is

[TABLE]

A string $s_{1}$ is a prefix of a string $s$, written $s_{1}\leqslant s$, if there exists $s_{2}$ such that $s_{1}s_{2}=s$. The prefix closure of $L_{m}\left(\mathbf{G}\right)$ is $\overline{L_{m}\left(\mathbf{G}\right)}:=\left\{s_{1}\in\Sigma^{\ast}|\left(\exists s\in L_{m}\left(\mathbf{G}\right)\right)\text{ }s_{1}\leqslant s\right\}$. We say that $\mathbf{G}$ is nonblocking if $\overline{L_{m}\left(\mathbf{G}\right)}=L\left(\mathbf{G}\right)$. The three equivalent meanings of “nonblocking” are 1) the system can always reach a marker state from every reachable state; 2) every string in the closed behavior can be extended to a string in the marked behavior; 3) every physically possible execution can be extended to completing distinguished tasks.

The usual way to combine several automata into a single, more complex automaton is called synchronous product. For two automata $\mathbf{G}_{i}=\left(Q_{i},\Sigma_{i},\delta_{i},q_{0,i},Q_{m,i}\right),i=1,2$, the synchronous product $\mathbf{G}=\left(Q,\Sigma,\delta,q_{0},Q_{m}\right)$ of $\mathbf{G}_{1}$ and $\mathbf{G}_{2}$, denoted by $\mathbf{G}_{1}\|\mathbf{G}_{2}$, is constructed to have marked behavior $L_{m}\left(\mathbf{G}\right)=L_{m}\left(\mathbf{G}_{1}\right)\|L_{m}\left(\mathbf{G}_{2}\right)$ and closed behavior $L\left(\mathbf{G}\right)=L\left(\mathbf{G}_{1}\right)\|L\left(\mathbf{G}_{2}\right)$ [46, Chapter 3.3]. The synchronous product of more than two automata can be constructed similarly.

For a practical system, the plant can be modeled as an automaton $\mathbf{G}$. The desired behavior of the controlled system is determined by a control specification, also modeled as an automaton $\mathbf{E}$. Both the plant $\mathbf{G}$ and the control specification $\mathbf{E}$ may be the synchronous product of many smaller components.

For supervisory control, the alphabet $\Sigma$ is partitioned as

[TABLE]

where $\Sigma_{c}$ is the subset of controllable events that can be disabled by an external supervisor, and $\Sigma_{u}$ is the subset of uncontrollable events that cannot directly be prevented from occurring. Here $\Sigma_{c}$ and $\Sigma_{u}$ are disjoint subsets. A supervisory controller (supervisor) forces the plant to respect the control specification by disabling certain controllable events that are originally able to occur in the plant.

To synthesize a satisfactory supervisor, SCT provides a formal method for theoretically solving the typical supervisory control problem [54]: Given a plant $\mathbf{G}$ over alphabet $\Sigma=\Sigma_{c}\dot{\cup}\Sigma_{u}$ and control specification $\mathbf{E}$, find a maximally permissive supervisor $\mathbf{S}$ such that the controlled system $\mathbf{S/G}$ is non-blocking and meets the control specification $\mathbf{E}$. That is $\mathbf{S}$ satisfies

[TABLE]

where $\sup\mathcal{C}\left(L\right)$ means the supremal controllable sublanguage of $L$. Equation (2) means that the supervisor $\mathbf{S}$ never violates the control specification $\mathbf{E}$. Here, $\mathbf{S}$ is a monolithic (namely fully centralized) supervisor [46, Chapter 4.6]. If there exist several control specifications, the supervisor can be also designed in a decentralized framework. Decentralized supervisory control assigns a separate specialized supervisor to satisfy each control specification $\mathbf{E}_{j}$. For each control specification $\mathbf{E}_{j}$, a decentralized supervisor $\mathbf{S}_{j}$ is computed in the same way as for a monolithic supervisor. Then, all the decentralized supervisors work together to meet the control specification $\mathbf{E}=\mathbf{E}_{1}\|\mathbf{E}_{2}\|\cdots$. Here, if the synthesized supervisors are blocking, a coordinator is required to make the supervisors nonblocking. The main advantage of the decentralized supervisory control framework is that the synthesized supervisors are relatively small-scale, and are easier to understand, maintain and change.

Related algorithms in DES and SCT can be performed on software platforms such as TCT software [46], Supremica [57] and Discrete Event Control Kit written in MATLAB [58].

III Safety Issues and User Requirements

This section lists some relevant safety issues of multicopters. Also, user requirements including functional requirements and safety requirements are textually described.

III-A Safety issues

Major types of multicopter failures that may cause accidents will be introduced. Here, three types of failures are considered, including communication breakdown, sensor failure and propulsion system anomaly.

• •

Communication breakdown. Communication breakdown mainly refers to a contact anomaly between the Remote Controller (RC) transmitter and the multicopter, or between the Ground Control Station (GCS) and the multicopter. In this paper, for simplicity, only RC is considered.

• •

*Sensor failure. *Sensor failure mainly implies that a sensor on the multicopter cannot accurately measure related variables, or cannot work properly. This paper considers the sensor failures including barometer failure, compass failure, GPS failure, Inertial Navigation System (INS) failure.

• •

*Propulsion system anomaly. *Propulsion system anomaly mainly refers to battery failure and propulsor failure caused by Electronic Speed Controllers (ESCs), motors or propellers.

More information about safety issues can be found in the book [1].

III-B User requirements

From the commercial perspective of customers and users, a multicopter product is required to have general functions as a rotorcraft, and also be capable of coping with the relevant safety issues. Thus, functional requirements and safety requirements are listed in Tables 1-4, respectively. They are summarized by referring the material from [45] and the authors’ knowledge and engineering experience.

III-B1 Functional requirements

The following functional requirements describe what behavior the multicopter is able to perform.

Table 1. Functional requirements

[TABLE]

III-B2 Safety requirements

The safety requirements restrict what action the user wants the multicopter to perform under specific situations when it is on the ground, in flight, or in process of returning and landing.

Table 2. Safety requirements on ground

[TABLE]

Table 3. Safety requirements in flight

[TABLE]

Table 4. Safety requirements on returning and landing

[TABLE]

IV Multicopter Mode and Event Definition

In order to transform the user requirements to automata, several multicopter modes and events are defined in this section.

IV-A Multicopter mode

Referring to [45], the whole process from taking off to landing of multicopters is divided into eight multicopter modes. They form the basis of the failsafe mechanism.

• •

POWER OFF MODE. This mode implies that a multicopter is out of power. In this mode, the remote pilot can (possibly) disassemble, maintain and replace the hardware of a multicopter.

• •

STANDBY MODE. When a multicopter is connected to the power module, it enters a pre-flight status. In this mode, the multicopter is not armed, and the remote pilot can arm the multicopter manually. Afterwards, the multicopter will perform a safety check and then transit to the next mode according to the results of the safety check.

• •

GROUND-ERROR MODE. This mode indicates that the multicopter has a safety problem. In this mode, the buzzer will turn on an alarm to alert the remote pilot that there exist errors in the multicopter.

• •

LOITER MODE. Under this mode, the remote pilot can use the control sticks of the RC transmitter to control the multicopter. Horizontal location can be adjusted by the roll and pitch control sticks. When the remote pilot releases the control sticks, the multicopter will slow to a stop. Altitude can be controlled by the throttle control stick. The heading can be set with the yaw control stick. When the remote pilot releases the roll, pitch and yaw control sticks and pushes the throttle control stick to the mid-throttle deadzone, the multicopter will automatically maintain the current location, heading and altitude.

• •

ALTITUDE-HOLD MODE. Under this mode, a multicopter maintains a consistent altitude while allowing roll, pitch and yaw to be controlled normally. When the throttle control stick is in the mid-throttle deadzone, the throttle is automatically controlled to maintain the current altitude and the attitude is also stabilized but the horizontal position drift will occur. The remote pilot will need to regularly give roll and pitch commands to keep the multicopter in place. When the throttle control stick goes outside the mid-throttle deadzone, the multicopter will descend or climb depending upon the deflection of the control stick.

• •

STABILIZE MODE. This mode allows a remote pilot to fly the multicopter manually, but self-levels the roll and pitch axes. When the remote pilot releases the roll and pitch control sticks, the multicopter automatically stabilizes its attitude but position drift may occur. During this process, the remote pilot will need to regularly give roll, pitch and throttle commands to keep the multicopter in place as it might be pushed around by wind.

• •

RETURN-TO-LAUNCH (RTL) MODE. Under this mode, the multicopter will return to the base location from the current position, and hover there.

• •

AUTOMATIC-LANDING (AL) MODE. In this mode, the multicopter realizes automatic landing by adjusting the throttle according to the estimated height 333Even if the barometer fails, the height estimation is acceptable within a short time. Similarly, the other estimates generated by filters could continue to be used for a short time, even if related sensors fail..

IV-B Event definition

Three types of events are defined here: Manual Input Events (MIEs), Mode Control Events (MCEs) and Automatic Trigger Events (ATEs). The failsafe mechanism detects the occurrence of MIEs and ATEs, and uses MCEs to decide which mode the multicopter should stay in or switch to. Here, MIEs and MCEs are controllable, while ATEs are uncontrollable in the sense of SCT.

IV-B1 MIEs

MIEs are instructions from the remote pilot sent through the RC transmitter. This part defines eight MIEs as shown in Table 5.

Table 5. MIE definition

[TABLE]

Here, MIE6, MIE7 and MIE8 are realized by a three-position switch (namely the flight mode switch) on the RC transmitter as shown in Figure 3.

IV-B2 MCEs

MCEs are instructions from multicopter’s autopilot. As shown in Table 6, these events will control the multicopter to switch to a specified mode.

Table 6. MCE definition

[TABLE]

IV-B3 ATEs

ATEs are independent of the remote pilot’s operations. As shown in Table 7, these events contain the health check results of onboard equipment and sensor measurements of the multicopter status.

Table 7. ATE definition

[TABLE]

Here, note that this paper assumes the health check of equipment above can be performed by effective fault diagnosis and health evaluation methods. For simplified presentation, the statements of “check result of” and “measured” are omitted in the subsequent sections.

Remark 1. MCEs are defined to guarantee the controllability of the plant, because supervisory control restricts the behavior of a plant such that the given control specifications are fulfilled and as much as possible never violated, by enabling or disabling controllable events in the plant. According to safety requirements, the user declares which mode the multicopter should enter. This leads to the definition of controllable events related to mode transitions, namely MCEs.

V Failsafe Mechanism Design

The failsafe mechanism uses multicopter modes and switch conditions among them to make multicopters satisfy the user’s safety requirements. In this section, functional requirements are used to model a multicopter plant automaton with defined multicopter modes and events. Then, from the safety requirements, multiple control specifications are represented by automata. These control specifications should indicate the preferable failsafe measures consistent with the textually described safety requirements. After the plant and control specifications have been obtained, the supervisor is synthesized by using monolithic supervisory control.

V-A Multicopter plant modeling

V-A1 Modeling principles

Modeling the multicopter plant is to mathematically describe what behavior the multicopter is able to perform with an automaton transformed from functional requirements. In this paper, the modeling principles of the multicopter plant include: i) modeling from a simple schematic diagram to a comprehensive automaton model; 2) modeling from the ‘on ground’ component to the ‘in air’ component; 3) events of each transition modeled mutually exclusively. Figure 4 depicts a schematic diagram of the ‘on ground’ component and ‘in air’ component of the multicopter plant, respectively. The schematic diagram lists all modes which the multicopter possibly enters, after a series of MIEs and ATEs occur.

V-A2 Model details

By extending the above schematic diagrams with detailed events and transitions, the plant is described by an automaton as shown in Figure 5. It describes the basic function of a multicopter. Specifically, Plant contains 27 states (S0-S26), 37 events and 63 transitions. Here, the states S${}_{0},$S${}_{3},$S${}_{13},$S14 are marked as accepting states. The state S0 represents POWER OFF MODE; the state S3 represents STANDBY MODE; the state S13 represents GROUND-ERROR MODE; the state S14 integrates other multicopter modes. Plant can be divided into two parts: one (consists of states S0-S14 and transitions among them) describes the multicopter behavior on the ground (‘on ground’ component), and the other one (consists of states S3,S12-S26 and transitions among them) describes the behavior during flight (‘in air’ component). These correspond to the schematic diagram shown in Figure 4.

V-B Control specification design

V-B1 Modeling principle

In this part, control specifications are designed to restrict the behavior of Plant according to the description of the safety requirements. In order to obtain a correct and non-blocking supervisor, the control specifications must cover all possible strings (enable desirable strings and disable the others) in the plant, and the control specifications must have no conflict among themselves.

V-B2 Control specification design ‘on ground’

Through a study of safety requirements, it can be seen that SR1 describes the intended failsafe measure when the multicopter is on the ground. In other words, SR1 restricts what action the user wants the multicopter to perform under specific situations when it is on the ground. Thus, we design a control specification to cover all possible strings in the ‘on ground’ component of Plant. The requirements given in Tables 1-3 are different from the designed specifications. The former is textually and informally described, whereas, based on which, the latter is designed formally described in form of automaton. Several requirements may be described by one specification, or one requirement may be described by several specifications.

In safety requirement SR1, the user lists the required conditions for a successful arm. In order to model it with an automaton, the key is to split the branches in the ‘on ground’ component of Plant, and enable only one mode which the user expects the multicopter to switch to. Following this principle, a control specification named Specification 1 is designed as shown in Figure 6. It contains 8 states (S0-S7), 24 events and 68 transitions. Here, the states S${}_{0},$S1 are marked as accepting states. The state S1 represents STANDBY MODE, and the state S0 integrates other multicopter modes. Here, two points need to be noted:

i) The selfloops on the state S${}_{0},$S${}_{4},$S6 are used to guarantee that the irrelevant events will not interrupt the event sequence presented in Plant, and not influence the occurrence of other control specifications.

ii) SR1 itself is textually and informally described. It does not mention which mode the multicopter should enter, if it cannot be successfully armed. Furthermore, it does not take all possible strings into consideration. In this case, during the design of control specifications, it is required to appropriately infer the user’s potential intention, and add the omitted part to guarantee that the control specification covers all possible strings in the ‘on ground’ component of Plant.

V-B3 Control specification design ‘in ground’ (Specification 7)

For the ‘in air’ component of Plant, safety requirements* SR2-SR13* restrict what action the user wants the multicopter to perform under specific situations when it is in air. Thus, we design 24 control specifications to cover all possible strings in the ‘in air’ component of Plant. The traversal relation between the designed control specifications and the structure of the ‘in air’ component of Plant is shown in Figure 7.

Here, because of limitation of space, we take Specification 7 as an example to demonstrate the design of control specifications for the ‘in air’ component of Plant. This control specification is obtained by transforming “safety requirements* SR7* and* SR8*” to an automaton model. As shown in Figure 8, Specification 7 contains 6 states (S0-S5), 31 events and 91 transitions. Here, the states S${}_{0},$S1 are marked as accepting states. The state S1 represents LOITER MODE, and the state S0 integrates other multicopter modes. The details of other control specifications are presented in the support material available in http://rfly.buaa.edu.cn/resources.

V-C Supervisor synthesis on TCT software

The algorithms and operations in this part are performed on TCT software. In order to synthesize a supervisor by TCT software, the modeled multicopter plant and designed control specifications are first input. The multicopter plant is named as “PLANT”, and the 25 control specifications are named as “$\mathbf{E}_{j}$”, $j=1,2,\cdots,25$. The input process is shown in http://rfly.buaa.edu.cn/resources.

V-C1 Control specification completion

Here, note that PLANT contains 37 events, while the number of events in each $\mathbf{E}_{j}$ is less than 37 (i.e. the alphabet of each $\mathbf{E}_{j}$ is different from that of PLANT). This is because the given textual safety requirements only emphasize the events we are concerned with and ignore the remaining events. For supervisory control, the alphabet of each $\mathbf{E}_{j}$ should be equal to the alphabet of PLANT. Thus, the control specification should be completed by the following TCT instructions:

[TABLE]

where $\mathbf{EVENTS}$ is a selfloop automaton containing all events in the alphabet of PLANT. Then, for each $\mathbf{E}_{j}$, we have

[TABLE]

Here, the events present in PLANT but not in $\mathbf{E}_{j}$ are added into $\mathbf{E}_{j}$ in form of selfloops.

V-C2 Supervisor synthesis

In the monolithic supervisory control framework, all the control specifications should be synchronized into a monolithic one. That is

[TABLE]

It turns out that $\mathbf{E}$ is nonblocking, and contains 133 states and 2219 transitions. Then, a monolithic supervisor is synthesized by

[TABLE]

The obtained supervisor is the expected failsafe mechanism. It contains 784 states, 37 events and 1554 transitions. There are 8 accepting states to be marked, which correspond respectively to 8 multicopter modes. Besides the monolithic supervisory control, the supervisor can also be synthesized by decentralized supervisory control, and a supervisor reduction process can also be carried out for an easier realization in practice. The synthesis is also carried out in the software Supremica with the result same to TCT. These source files are presented in http://rfly.buaa.edu.cn/resources.

VI Examples and Discussion

This section illustrates three examples to demonstrate some possible reasons leading to a problematic supervisor, and gives a brief discussion about the scope of applications and properties of the method.

VI-A Examples

The design of control specifications is a process to understand and re-organize the safety requirements. If the designer synthesizes a blocking supervisor, he must recheck the correctness of control specifications and make modifications. Here, we illustrate three examples demonstrating the blocking phenomenon due to inappropriate design of control specifications and conflicting safety requirements.

Example 1. The aim of this example is to show that missing information in control specification may lead to a blocking supervisor. In this example, we delete transitions “S${}_{6}\rightarrow$ATE13$\rightarrow$S6”, “S${}_{6}\rightarrow$ATE14$\rightarrow$S6” and “S${}_{6}\rightarrow$ATE15$\rightarrow$S6” in Specification 1. In this case, Specification 1 is changed to an automaton named Example 1 as shown in Figure 9. By replacing Specification 1 with Example 1, the supervisor is synthesized and turns out to be blocking. The blocking branch is depicted in Figure 10. The reason is that blocking occurs owing to the missing selfloops at state S6 in Example 1. The missing selfloops make the automaton “think” that events ATE13, ATE14 and ATE15 will not occur at state S6, while these events should occur in Plant. Thus, a blocking supervisor is synthesized. This means an uncertainty as to what should occur in the blocking point.

Example 2. The aim of this example is to show that conflict in control specifications will lead to a blocking supervisor. In this example, we replace the transition “S${}_{6}\rightarrow$MCE2$\rightarrow$S1” with a transition “S${}_{6}\rightarrow$MCE3$\rightarrow$S1” in Specification 1. In this case, Specification 1 is changed to an automaton named Example 2 as shown in Figure 11. By adding Example 2 to the whole control specification, the supervisor is synthesized and turns out to be blocking. The blocking branch is depicted in Figure 12. The reason that blocking occurs is the conflict between Specification 1 and Example 2. Specification 1 indicates a transition “S${}_{6}\rightarrow$MCE2$\rightarrow$S1”, while Example 2 has a transition “S${}_{6}\rightarrow$MCE3$\rightarrow$S1”. This conflict will “confuse” the supervisor, and make it impossible to decide which transition should occur. Thus, a blocking supervisor is synthesized.

Example 3. The aim of this example is to show that conflict in user requirements will lead to a blocking supervisor. Assume we have a new safety requirement described as follows: “when the multicopter is flying, the multicopter can be manually switched to return to the base by the RC transmitter. This switch requires that the INS, GPS, barometer, compass and propulsors are all healthy. Otherwise, the switch cannot occur.” Then, this safety requirement is transformed to an automaton as shown in Figure 13. By adding Example 3 to the whole control specification, the supervisor is synthesized and turns out to be blocking. The blocking branch is depicted in Figure 14. The reason that blocking appeared is the conflict between the original SR7 and the newly presented safety requirement. In SR7, it indicates that “this switch requires that the INS, GPS, barometer, compass, propulsors are all healthy, and the battery’s capacity is able to support the multicopter to return to the base”. However, the new safety requirement does not restrict the condition of battery’s capacity. As in Example 2, this conflict leads to a blocking supervisor.

Remark 2. From the above examples, it can be seen that an incorrect failsafe mechanism might be obtained during the design process due to conflicting safety requirements or incorrect and inappropriate design of control specifications. The mistake might be introduced inadvertently, and the designer cannot easily detect the problem by using empirical design methods. However, by relying on the SCT-based method, we can check the correctness of the obtained failsafe mechanism, and make modifications if a problematic supervisor is generated. This is a big advantage of the proposed method over empirical design methods. Once a nonblocking supervisor is obtained, the resulting failsafe mechanism is logically correct, and able to deal with all relevant safety issues appearing during flight.

VI-B Discussion

This paper aims to study a method to guarantee the correctness in the design of the failsafe mechanism. Actually, correctness can be interpreted in two different ways. On the one hand, correctness can be explained as absolute safety, meaning that the multicopter can cope with all possible safety problems. On the other hand, correctness is defined as consistency between the obtained failsafe mechanism and safety requirements. Given a model and a control specification for an autonomous system, synthesis approaches can automatically generate a protocol (or strategy) for controlling the system that satisfies or optimizes the property. This process is named as “correct-by-design”  [59]. In this domain, various formal methods and techniques, such as SCT and linear temporal logic, are used to design control protocol of autonomous systems, including autonomous cars [60], aircraft [61]-[63] and swarm robots [64]. Similar to the above literature, in this paper, we focus on the meaning of correctness that all requirements can be correctly satisfied. With a precise description of both the multicopter and its correct behavior, the proposed method allows a failsafe mechanism that guarantees the correct behavior of the system to be automatically designed.

Here, the generated supervisor by SCT satisfies the following properties:

i) Deterministic. This property has two aspects. First, there exists no situation that one event triggers a transition from a single source state to different target states in the obtained supervisor. This is a necessary condition for a deterministic automaton. However, this situation might occur due to man-made mistakes in an empirical failsafe mechanism design. Second, after occurrence of MIEs and ATEs, SCT can guarantee that only one MCE is enabled by disabling other MCEs due to deliberate design of control specifications. In this case, after occurrence of certain MIEs and ATEs, the mode which the multicopter should enter is deterministic.

ii) Nonconflicting [46, Chapter 3.6]. None of the control specifications conflict with any others. If there exist conflicts, the supervisor will not be successfully synthesized, because SCT cannot decide which control specification is the user’s true intention. If so, the designer should check 1) the correctness of control specifications transforming from user requirements; or 2) the reasonableness of the user requirements.

iii) Nonblocking. The generated supervisor is nonblocking, which can be interpreted that all possible strings in Plant are considered (either enabled or disabled) in the supervisor. If there are some strings which are not considered in the control specifications, the marker states may not be reached in some branches from the initial state. Then, the obtained supervisor might be incomplete (even empty). This is because SCT cannot compute control due to incorrect user’s specifications. If so, the designer should modify the control specifications to make them consistent.

iv) Logical correctness. SCT is a mature and effective tool to be used in the area of decision-making. If the plant and control specifications are correctly modeled, the logic of the generated supervisor will correctly satisfy user requirements without introducing man-made mistakes and bugs.

VII Implementation and Simulation

Based on the obtained supervisory controller generated by TCT software or Supremica, an implementation method suitable for multicopter is presented, in which the supervisory controller is transformed into decision-making codes.

VII-A Failsafe mechanism implementation

On the one hand, we would want to avoid manual implementation of the calculated supervisors, since this may introduce errors and is also difficult for a complex case. On the other hand, we expect an easy way to generate an Application Programming Interface (API) function with events as the input and marked states as output so that it can be easily integrated into the existing program in flight boards. The information required from a synthesized supervisor is a transition matrix, which is an $m\times 3$ matrix where $m$ is the number of transitions in the synthesized supervisor (We have developed a function to export the transition matrix based on the output file of Supremica,* *available in http://rfly.buaa.edu.cn/resources). As shown in Table 8, in each row, it consists of a source state, a destination state and a triggered event. For example, if the multicopter is in source state $1$ and the triggered event is $1,$ then the destination state will be $2$. By taking the synthesized supervisor of multicopters as an example, it contains $784$ states, $37$ events and $1554$ transitions. So, the transition matrix is an $1554\times 3$ matrix. In fact, we only need to consider $8$ accepting states, namely POWER OFF MODE, STANDBY MODE, GROUND-ERROR MODE, LOITER MODE, ALTITUDE-HOLD MODE, STABILIZE MODE, RTL MODE and AL MODE. Based on them, corresponding low-level control actions exist. However, there exist many intermediate states in the transition matrix ($784-8=776$ intermediate states for the considered multicopter), to which no control actions correspond. Therefore, after one decision period, the system must be in an accepting state. This is a major problem we need to solve. Fortunately, this is always true.

Table 8. Transition matrix

[TABLE]

In practice, the events will be detected every $0.01s$ for example, while the decision period may be $1s$. All triggered events are collected in every decision period. By recalling Figure 5, since the events in every transition are mutually exclusive, one and only one event must be triggered for any transition. As a result, the system does not stop at intermediate states after feeding in all detected events. For example, by recalling the ‘in air’ component in Figure 5, if the initial state is S14 and we collect the events MIE5, MIE6, ATE1, ATE3, ATE5, ATE7, ATE9, ATE11, ATE13, ATE16, ATE18, ATE20, then the system will go to S26 in Plant. Consequently, only one MCEi will be enabled by the autopilot according to the specifications. Therefore, the system will stop at an accepting state finally. For our case, the failsafe mechanism is implemented as shown in Table 9, where $\Delta>0$ represents a decision-making time interval. Actually, the high-level decision-making should be a relatively slow process in practice. Thus, the failsafe mechanism implementation is not synchronized with the low-level flight control system.

Table 9. Decision-making logic implementation

[TABLE]

VII-B Simulation

In this part, we put the failsafe mechanism into a real-time flight simulation platform of quadcopters developed by MATLAB. Although it is realized by MATLAB, this method is applicable to any programming language. The simulation diagram is shown in Figure 15. This simulation contains three main functions: i) the failsafe mechanism can determine the flight mode according to the health check result, instruction of RC transmitter and quadcopter status; ii) the remote pilot can fly the quadcopter through RC transmitter; iii) the flight status of quadcopter can be visually displayed by FlightGear. Thus, this simulation can be viewed as a semi-autonomous autopilot simulation of quadcopters. A video of this simulation is presented in https://www.youtube.com/watch?v=b1-K2xWbwF8&feature=youtu.be or http://t.cn/RXmhnu6. It contains three scenarios: i) the remote pilot manually controls the quadcopter to arm, fly, return to launch, and land; ii) anomalies of GPS, barometer, and INS are occurred during flight; iii) the connection of RC transmitter is abnormal during flight.

VIII Conclusions

This paper proposes an SCT based method to design a failsafe mechanism of multicopters. The modeling process of system plant and control specifications is presented in detail. The failsafe mechanism is obtained by synthesizing a supervisor in a monolithic framework. It ignores the detailed dynamic behavior underlying each multicopter mode. This is reasonable because the failsafe mechanism belongs to the high-level decision-making module of a multicopter, while the dynamic behavior can be characterized and controlled in the low-level flight control system. Also, we discuss the meaning of correctness and the properties of the obtained supervisor. This makes the failsafe mechanism convincingly correct and effective, demonstrating that the proposed method improves on purely empirical design methods. This paper deals with the health status of multicopter components in a qualitative manner. In future research, a quantitative health index will be added to extend the failsafe mechanism.