Loading...

arXiv.org > 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

Loading...