Commits
Comments (0)
Files changed (28)

+6 0.gitignore

+0 0data/figures/V_T.pdf

+0 0data/figures/alpha_beta.pdf

+0 0data/figures/elevons.pdf

+0 0data/figures/euler_angles.pdf

+0 0data/figures/fast_updates.pdf

+0 0data/figures/position.pdf

+0 0data/figures/propulsion.pdf

+0 0data/figures/rotation_rate.pdf

+0 0data/figures/slow_updates.pdf

+1 0data/latex/out.stamp

+24 0data/latex/tbl_aero_gen.tex

+22 0data/latex/tbl_aero_stab.tex

+12 4nonlinear_model/aircraft.py

+251 0ref.bib

+0 0ref/Nonlinbook.pdf

+0 0ref/Point_Out_Of_Flight_Envelope.pdf

+0 0ref/Results_vs_Prediction.pdf

+0 0ref/XFLR5_and_Stability_analysis.pdf

+0 0ref/[Khalil]  Nonlinear Systems.pdf

+0 0ref/aae666notes.pdf

+0 0ref/iolyap.pdf

+0 0ref/nonlinearDynamicInversion.pdf

+0 0ref/slideswindtunnelcfd.pdf

+0 0ref/systemIdentificationSummary.pdf

+0 0ref/windtunneluav.pdf

+609 0report.tex

+1 1test.py
data/figures/V_T.pdf
Binary file modified.
data/figures/alpha_beta.pdf
Binary file modified.
data/figures/elevons.pdf
Binary file modified.
data/figures/euler_angles.pdf
Binary file modified.
data/figures/fast_updates.pdf
Binary file modified.
data/figures/position.pdf
Binary file modified.
data/figures/propulsion.pdf
Binary file modified.
data/figures/rotation_rate.pdf
Binary file modified.
data/figures/slow_updates.pdf
Binary file modified.
data/latex/tbl_aero_gen.tex
data/latex/tbl_aero_stab.tex
nonlinear_model/aircraft.py
ref.bib
+ Author = {Alur, Rajeev and Courcoubetis, Costas and Halbwachs, Nicolas and Henzinger, Thomas A and Ho, PH and Nicollin, Xavier and Olivero, Alfredo and Sifakis, Joseph and Yovine, Sergio},
+ Abstract = {In this paper we describe the tool d/dt which provides automatic safety verification of hybrid systems with linear continuous dynamics with uncertain input. The verification procedure is based on a method for overapproximating reachable sets by orthogonal polyhedra. The tool also allows to synthesize a controller which switches the system between continuous modes in order to satisfy a safety specification.},
+ Abstract = {This paper concerns computational methods for verifying properties of polyhedral invariant hybrid automata (PIHA), which are hybrid automata with discrete transitions governed by polyhedral guards. To verify properties of the state trajectories for PIHA, the planar switching surfaces are partitioned to define a finite set of discrete states in an approximate quotient transition system (AQTS). State transitions in the AQTS are determined by the reachable states, or flow pipes, emitting from the switching surfaces according to the continuous dynamics. This paper presents a method for computing polyhedral approximations to flow pipes. It is shown that the flowpipe approximation error can be made arbitrarily small for general nonlinear dynamics and that the computations can be made more efficient for affine systems. The paper also describes CheckMate, a MATLABbased tool for modeling, simulating and verifying properties of hybrid systems based on the computational methods previously described.},
+ Title = {Verification of polyhedralinvariant hybrid automata using polygonal flow pipe approximations},
+ Author = {Cimatti, Alessandro and Clarke, Edmund and Giunchiglia, Enrico and Giunchiglia, Fausto and Pistore, Marco and Roveri, Marco and Sebastiani, Roberto and Tacchella, Armando},
+ Abstract = {A new method of controlling a flappingwing micro air vehicle by varying the velocity profiles of the wing strokes is presented in this manuscript. An exhaustive theoretical analysis along with simulation results show that this new method, called splitcycle constantperiod frequency modulation, is capable of providing independent control over vertical and horizontal body forces as well as rolling and yawing moments using only two physical actuators, whose oscillatory motion is defined by four parameters. An actuated bobweight is introduced to enable independent control of pitching moment. A general method for deriving sensitivities of cycleaveraged forces and moments to changes in wingbeat kinematic parameters is provided, followed by an analytical treatment for a case where the angle of attack of each wing is passively regulated and the motion of the wing spar in the stroke plane is driven by a splitcycle waveform. These sensitivities are used in the formulation of a cycleaveraged control law that successfully stabilizes and controls two different simulation models of the aircraft. One simulation model is driven by instantaneous aerodynamic forces derived from bladeelement theory, while the other is driven by an empirical representation of an unsteady aerodynamic model that was derived from experiments.},
+ Title = {Model Checking of a FlappingWing MircoAirVehicle Trajectory Tracking Controller Subject to Disturbances},
+ Abstract = {A hybrid system is a dynamical system whose behavior exhibits both discrete and continuous change. A hybrid automaton is a mathematical model for hybrid systems, which combines, in a single formalism, automaton transitions for capturing discrete change with di
+ Title = {A Modelbased Approach to Verification of Spacecraft Software using the SPIN Model Checker},
+ Title = {Nonlinear control using discretetime dynamic inversion under input saturation: theory and experiment on the Stanford dragonfly UAVs},
+ Title = {UAV Adaptive Control Laws Using NonLinear Dynamic Inversion Augmented with an Immunitybased Mechanism},
+ Author = {Moncayo, Hever and Perhinschi, Mario G and Wilburn, Brenton and Wilburn, Jennifer and Karas, Ondrej},
+ Abstract = {This article introduces a computational tool called CheckMate. CheckMate is a tool for modelling, prototyping, simulating specific situation and formally verifying hybrid dynamic systems based on the MATLAB/Simulink and Stateflow Toolbox from The MathWorks, Inc. This paper presents the elements of CheckMate from the user’s perspective and illustrates its features using a three dimensional linear system example. The theory underlying CheckMate is also reviewed briefly. More complete presentations of the theory can be found in [17].},
+ Title = {An assessment of the current status of algorithmic approaches to the verification of hybrid systems},
+ Title = {Towards Certification of Autonomous Unmanned Aircraft Using Formal Model Checking and Simulation},
ref/Nonlinbook.pdf
Binary file added.
ref/Point_Out_Of_Flight_Envelope.pdf
Binary file added.
ref/Results_vs_Prediction.pdf
Binary file added.
ref/XFLR5_and_Stability_analysis.pdf
Binary file added.
ref/[Khalil]  Nonlinear Systems.pdf
Binary file added.
ref/aae666notes.pdf
Binary file added.
ref/iolyap.pdf
Binary file added.
ref/nonlinearDynamicInversion.pdf
Binary file added.
ref/slideswindtunnelcfd.pdf
Binary file added.
ref/systemIdentificationSummary.pdf
Binary file added.
ref/windtunneluav.pdf
Binary file added.
report.tex
+\IEEEcompsocitemizethanks{\IEEEcompsocthanksitem James Goppert is with the School of Aeronautical and Astronautical Engineering,
+As unmanned aerial systems (UASs) assume more roles in our society, it is important that we ensure their safe operation. Model checking is a powerful tool that can be used to verify safety critical systems; however, it can only be directly applied to finite state machines. Existing methods have used reachable sets to transform systems with continuous and discrete (hybrid) dynamics into a finite state machine, but they often neglect disturbances. In this paper, we propose the use of Lyapunov theory to augment reachable sets for regulated linear systems in the presence of bounded disturbances. The restriction to linear systems can appear to be limiting, but we demonstrate that through dynamic inversion this method can be employed for model checking a nonlinear autopilot. The algorithm was flight tested on a small fixedwing UAS and the results demonstrate the effectiveness of the algorithm in identifying when the vehicle can operate safely. In addition, the algorithm is efficient and can be executed in realtime. Consequently, the algorithm can be used for runtime assurance in the presence of machine learning or varying environmental conditions.
+%The abstract sums up the contribution s of your projectmake it just as you would any journal or conference abstract: context, your results and why your results are better than some results among your references.
+%The course project will involve the modeling, analysis, design, and experimental or realistic simulation verification of a physical system under digital control. The physical system can be the system that you are working with in your research or you can talk with me to get some idea. The report should follow standard engineering technical paper 2 columns format that may include (but not limited to): Abstract under 200 words; Introduction  including literature research, System modeling and analysis; Controller synthesis; Stability and stability robustness analysis; Robustness to plant parameter variations; Robustness to input/output signal and controller parameter quantization; Effect of computation resource (time) and sampling time; Performance comparison with continuoustime controller; Simulation Study and Verification; Experimental Verification Conclusion and Discussion  Why did the controller/estimator work or or not work? (VERY IMPORTANT) References The report should be limited to 15 pages including figures and drawings.
+Model Checking, Dynamic Inversion, Lyapunov, LMI, Bounded, Disturbance, PIHA, RealTime, Runtime Assurance
+%Describe the problem you will work on. Give background or state or the art in the area with references. Also state the motivation of the problem. The style of writing should be like in any research paper or engineering report. Please get one of your classmates to read your material before submission, so you don't unnecessarily lose points for the five classes of mistakes mentioned in the syllabus.
+%\textbf{Motivate your problem here with adequate background and references}.Why is your problem important?
+\IEEEPARstart{A}s unmanned aerial systems (UASs) are trusted to perform more complex tasks, the associated safety risks increase. UASs typically have a complex controller that depends on both continuous vehicles states and discrete modes. Systems with tight coupling of continuous and discrete dynamics are known as hybrid systems. Verification and validation of hybrid systems is a difficult problem that has not been solved except for a few simple cases.
+In order to verify safety properties of software, model checking is typically employed~\cite{Baier2008}; however, model checking can only be directly applied to finite state machines. For systems with state dependent mode transitions, reachable sets are used to create a finite state machine simulation of the original hybrid system. Reachable set analysis is computationally expensive, but approximations using polyhedrons can efficiently overapproximate or underapproximate the reachable set~\cite{Chutinan1999}. Over approximation of the reachable set can prove a state is not reachable (safety), and under approximation can prove that a system is reachable (reachability). These properties can be formulated using computational tree logic (CTL), and verified efficiently using model checking software such as NuSMV~\cite{Cimatti2002}.
+Typical hybrid model checking is performed on systems with unstable modes~\cite{Silva2000,Silva2001}. In the UAS autopilot, the vehicle is regulated along the desired trajectory. If disturbances such as wind are not accounted for, the trajectory of the vehicle will eventually approach the deterministic reference trajectory~\cite{Goppert2013}. Consequently, the reachable set of the autopilot will be underestimated and unsafe sets may be reachable. In our previous work~\cite{Goppert2013}, we accounted for disturbances using the Hinfinity norm although this was an under approximation of the true reachable set. Disturbances can be more accurately accounted for using Lyapunov theory. For linear systems with bounded disturbances, the reachable set can be efficiently computed using an linear matrix inequality (LMI)~\cite{Khalil2002} and we will apply this method in this paper.
+When model checking a hybrid system, an intelligent selection of the controller can significantly reduce the complexity of the analysis~\cite{Goppert2013}. We employ dynamic inversion to linearize the dynamics of the vehicle. Dynamic inversion based controllers have already been shown to be effective at controlling UASs~\cite{Jang2004,Moncayo2012}. The reachable set can be calculated efficiently because of the linearized dynamics. Dynamic inversion is susceptible to modelling errors; however, these errors can be treated as bounded disturbances to the linear dynamics. Therefore, the LMI used to account for environmental disturbances such as wind can also be used to address modelling errors.
+The paper is organized as follows: Section~\ref{sec:sampling} discusses the sampling and quantization issues,
+Section~\ref{sec:results} contains simulation and flight test results of the Bormatec CamFlyer Q UAS (shown in Fig.~\ref{fig:camflyer}) flying a mission consisting of a series of waypoints. We demonstrate the identification of a logic error in the guidance algorithm using the model checking algorithm proposed.
+%Section~\ref{sampling} contains sampling and quantization issues, section~\ref{discretemodel} presents the sampled model, section~\ref{representation} gives various representations of the model and identification of parameters, section~\ref{stability} analyzes stability, sensitivity and robustness, controllability/observability analysis. Section~\ref{control1} presents control designs via the inputoutput approach, section~\ref{control2} via the polynomial approach, and section~\ref{control3} via state space approach. Section~\ref{optimal} presents optimal estimation and control, and section~\ref{implementation} covers implementation issues.
+%Discuss the sampling and quantization issues and potential implementation in this update. Your discussion needs to be quantitative. It will not be final, as you will need to iterate on this after you do your control designs.
+The PixHawk autopilot, shown in Fig.~\ref{fig:pixhawk} is the autopilot used for flight testing and the model for the simulation. The PixHawk has inertial sensors consisting of an ST Micro L3GD20 3axis 16bit gyroscope, an ST Micro LSM303D 3axis 14bit accelerometer / magnetometer, an Invensense MPU 6000 3axis accelerometer/gyroscope, and an MEAS MS5611 barometer. The accelerometer is read at 800 Hz with a low pass filter at 260 Hz, the gyroscope is read at 760 Hz with a low pass filter at 256 Hz, the magnetometer and barometer are both read at 150 Hz. Note that the inertial sensors communicate over serial and that ADC sampling and low pass filtering is occurring within the firmware of the sensors. The autopilot also has an external MPXV7002DP differential pressure sensor for airspeed that is sampled by the onboard 12bit ADC at 100 Hz and an external GPS module that sends serial packets at 5 Hz.
+The servos on the CamFlyer Q UAS are driven using pulse width modulated (PWM) analog signals output by the PixHawk autopilot. The frequency of the PWM signal 50 Hz. This limits the bandwidth of the signal transmitted to the main propeller motor and control actuator servos to the Nyquist frequency of 25 Hz.
+\item \emph{Rigid Body}: We neglect flexing of the airframe. This is valid except for the wings which flex during flight. The wing flexure modifies the aerodynamic performance which is reflected in the tables, but the associated dynamics are neglected. A notch filter will be used to suppress the structural modes of the wings.
+\item \emph{Constant Mass}: We are using an electric motor with a battery so it is reasonable to neglect mass changes. If a payload is dropped then a discrete mass change can be accounted for by changing the current mass/rotational inertia, but mass dynamics are nelected.
+\item \emph{Flat Earth}: We neglect the rotation of the Earth and assume that a local tangent frame is inertial. This is valid because the rate of Earths rotation is below the measurement capabilities of the sensors. This is because the Coriolis term is scales with the velocity of the aircraft. At the equator and at cruise velocity the magnitude of the Coriolis term would be on the magnitude of 1E5 rad/s, but our gyroscope resolution is only 1E4 rad/s.
+\item \emph{Consant Wind}: We neglect the effect of wind accleration on the system. It is assumed that the dynamics of the aircraft are much faster than the dynamics of the wind gusts. This is generally true for the nonwindy conditions in which the UAV can operate safely.
+\item \emph{n}: Navigation frame  This frame translates with the aircraft center of mass and rotates so that is locally tangent to the surface of the Earth. It is a right handled set given by North, East, and down.
+\item \emph{b}: Body frame  This frame is fixed in the aircraft. It is a right handed set given by forward, over the right wing, and down in the aircraft frame.
+\item \emph{s}: Stability frame  This frame is rotated from the body frame by the sideslip angle ($\beta$) about the body zaxis.
+\item \emph{w}: Wind frame  This frame is rotated from the stability frame by the angle of attach ($\alpha$) about the stabiliy yaxis.
+For now, the propulsion system is modelled as a first order system. The time constant is obtained experimentally. The effect of velocity on thrust is neglected.
+where $\mathbf{F}$ is the sum of forces on the rigid body, $m$ is the total mass, ${}^i\mathbf{v}^{cm}$ is the velocity of the center of mass, $\mathbf{M}$ is the sum of moments on the rigid body, $J_{cm}$ is the rotational inertia matrix about the center of mass, and $\mathbf{\omega}_{n/b}$ is the angular velocity of the b frame fixed in the rigid body with respect to the inertial frame i.
+where $V_T$ is referred to as the true velocity, ${}^e\mathbf{v}^{wind}$ is the wind velocity with respect to the earth at the current location of the aircraft, and $\hat{\mathbf{w}}_x$ is the unit vector in the wind frame x direction.
+Applying the constant mass, and flat earth assumptions and the defintion of relative velocity yields:
+note frame e is the earth frame which is now considered equivalent to frame i due to the flat Earth assumption.
+If we neglect $ \frac{^ed}{dt} {}^e\mathbf{v}^{wind}$ using the constant wind assumptions and mechanize the force equation in the wind frame, since the aerodynamic forces are most easily expressed in this frame, we obtain:
+\frac{^wd}{dt} \left[\mathbf{v}_{rel}\right]_w + \left[({}^e\mathbf{\omega}^b + {}^b\mathbf{\omega}^w ) \times \mathbf{v}_{rel}\right]_w &= \left[\mathbf{F}\right]_w/m
+ \dot{V_T} \hat{\mathbf{w}}_x + \left[{}^b\mathbf{\omega}^w \times \mathbf{v}_{rel}\right]_w &= \left[\mathbf{F}\right]_w/m  \left[{}^e\mathbf{\omega}^b \times \mathbf{v}_{rel}\right]_w
+%Develop your discrete model (simple baseline, or even part of your system to begin with), and pulse transfer functions between your reference inputs and measurements.
+\section{Transfer Function and State Space Representations and System ID}\label{sec:representation}
+%Represent your system in several ways in state space and transfer function/transfer matrix forms, document the physical parameters of your system and the uncertainty in their values. Obtain the parameters and their uncertainty through system ID methods if need be. Also document the relative speeds of sensing, actuation, and your plant itself so as to justify your system representation and simplifications for control design.
+\section{Stability, Sensitivity and Robustness, Controllability/Observability Analysis}\label{sec:stability}
+% Analyze your system representation for stability, observability and controllability. Check also whether the system is practically stableis it stable under all combinations of parameters possible? How observable is it? The observability matrix may be full rank, but it may take a long time to estimate its state because the observability matrix is ill conditioned. Similar considerations may apply to controllability.
+% Develop control designs for your plant via the inputoutput approach. Compare several discretizations of the PID controllers for performance. What discretizations are best for different input signals?
+% Develop your control designs for your system using the polynomial approach. Show your requirements and how you systematically satisfy them with the polynomial approach.
+% Apply state space control design methods to your system. Show how they meet design requirementsbe explicit with design requirements. Do the designs operate within actuator limits (displacement and speed)? Compare these results to your previous results from polynomial and inputoutput designs by plotting frequency responses on the same plot (with legends), and time responsestracking and control effort versus timeon the same plot for all designs.
+% Apply LQR, LQG and LQR with Kalman filter to your plant. Add these results to your comparison plots in both time domain and frequency domain (Bode). Compare your control effort to that obtained from pole placement designsee if you can choose Q and R to get realistic control effort.
+% Test your control designs on high fidelity models via simulation; you can try nonlinear or adaptive designs or LMI designs if you like. Clean up your work and develop abstract and conclusions. Submit your matlab/simulink codes along with your final updates. The submissions should be clean: 1 pdf file, 1 matlab file and a simulink file.
.gitignore