Formal Analysis of Linear Control Systems using Theorem Proving


Cornell University Library We gratefully acknowledge support from the Simons Foundation and member institutions > cs > arXiv:1707.06967 Search or Article ID inside arXiv All papers (Help | Advanced search) Broaden your search using Full-text links:

Download: PDF Other formats (license)

Current browse context: cs.LO < prev | next > new | recent | 1707

Change to browse by: cs cs.SY

References & Citations NASA ADS

DBLP - CS Bibliography listing | bibtex Adnan Rashid Osman Hasan

Bookmark (what is this?)

Computer Science > Logic in Computer Science Title: Formal Analysis of Linear Control Systems using Theorem Proving Authors: Adnan Rashid, Osman Hasan (Submitted on 21 Jul 2017) Abstract: Control systems are an integral part of almost every engineering and physical system and thus their accurate analysis is of utmost importance. Traditionally, control systems are analyzed using paper-and-pencil proof and computer simulation methods, however, both of these methods cannot provide accurate analysis due to their inherent limitations. Model checking has been widely used to analyze control systems but the continuous nature of their environment and physical components cannot be truly captured by a state-transition system in this technique. To overcome these limitations, we propose to use higher-order-logic theorem proving for analyzing linear control systems based on a formalized theory of the Laplace transform method. For this purpose, we have formalized the foundations of linear control system analysis in higher-order logic so that a linear control system can be readily modeled and analyzed. The paper presents a new formalization of the Laplace transform and the formal verification of its properties that are frequently used in the transfer function based analysis to judge the frequency response, gain margin and phase margin, and stability of a linear control system. We also formalize the active realizations of various controllers, like Proportional-Integral-Derivative (PID), Proportional-Integral (PI), Proportional-Derivative (PD), and various active and passive compensators, like lead, lag and lag-lead. For illustration, we present a formal analysis of an unmanned free-swimming submersible vehicle using the HOL Light theorem prover. Comments: International Conference on Formal Engineering Methods Subjects: Logic in Computer Science (cs.LO); Systems and Control (cs.SY) Cite as: arXiv:1707.06967 [cs.LO]

(or arXiv:1707.06967v1 [cs.LO] for this version)

Submission history From: Adnan Rashid [view email] [v1] Fri, 21 Jul 2017 16:28:57 GMT (1148kb,D) Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?) Link back to: arXiv, form interface, contact. Loading [MathJax]/jax/input/TeX/config.js


Formal Analysis of Linear Control Systems using Theorem Proving

Cornell University Library We gratefully acknowledge support from the Simons Foundation and member institutions > cs > arXiv:1707.06967 Sea...

57KB Sizes 1 Downloads 15 Views

Recommend Documents

Modelling, analysis and control of linear systems using - GIPSA-Lab
Definition. Pole placement control. Specifications. Integral Control. Observer. Observation. Observability. Observer des

2 analysis of linear control systems - IEEE Control Systems Society
2 ANALYSIS OF LINEAR. CONTROL SYSTEMS. 2.1 INTRODUCTION. In this introduction we give a brief description of control pro

Optimization Of Linear Control Systems
control systems doc, optimization of linear control systems epub optimization of linear control systems ebook, optimizat

Linear Control Systems | SpringerLink
Anyone seeking a gentle introduction to the methods of modern control theory and engineering, written at the level of a

Linear Control Systems
Note : For time-invariant control systems – in the controllability definition – the initial time t0 can be set equal

Linear Control Systems (LCSL)
Jul 31, 2016 - Linear Control Systems specialise in the design, installation & maintenance of bespoke Building Energy Ma

Types of Control Systems | Linear and Non Linear Control System
Before I introduce you the theory of control system it is very essential to know the various types of control systems. N

Numerical solution of linear control systems using interpolation scal
Dec 12, 2016 - Abstract. The current paper proposes a technique for the numerical solution of linear control systems. Th

stability analysis of linear control systems with - Yuguang Fang

Stability analysis of networked and quantized linear control systems
Nonlinear Analysis: Hybrid Systems journal homepage: Stability analysis of networked and q