Formal modeling and verification of fractional order linear systems

详细信息    查看全文

• 作者：Chunna Zhao^a ; ^{chunnazhao@163.com" class="auth_mail" title="E-mail the corresponding author} ; Likun Shi^b ; Yong Guan^b ; Xiaojuan Li^b ; Zhiping Shi^b
• 关键词：High-order logic ; Theorem proving ; Fractional order linear systems ; Formal verification
• 刊名：ISA Transactions
• 出版年：2016
• 出版时间：May 2016
• 年：2016
• 卷：62
• 期：Complete
• 页码：87-93
• 全文大小：973 K

文摘

This paper presents a formalization of a fractional order linear system in a higher-order logic (HOL) theorem proving system. Based on the formalization of the Grünwald–Letnikov (GL) definition, we formally specify and verify the linear and superposition properties of fractional order systems. The proof provides a rigor and solid underpinnings for verifying concrete fractional order linear control systems. Our implementation in HOL demonstrates the effectiveness of our approach in practical applications.