TY - GEN
T1 - Analyzing Real Time Linear Control Systems Using Software Verification
AU - Duggirala, Parasara Sridhar
AU - Viswanathan, Mahesh
N1 - Publisher Copyright:
© 2015 IEEE.
Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2016/1/14
Y1 - 2016/1/14
N2 - Deployed embedded software interacts with sensors and actuators to control a physical environment. While the evolution of the control system is specified by Ordinary Differential Equations (ODEs), the embedded software periodically senses the state of the system, performs computation over the inputs, and initiates the actuators based on the result of computation. In this paper, we present a bounded time safety verification technique for periodically actuated linear control systems. The model considered in this paper takes into account that the control tasks are executed on a real time operating system and hence the task, in some instances misses the real time deadlines. Using matrix exponentiation, and symbolic evaluation of inputs, we reduce the verification problem of such systems into software verification with computation over reals. We compare different techniques for verifying such software, highlight the merits of each of the approaches, and present our experimental results.
AB - Deployed embedded software interacts with sensors and actuators to control a physical environment. While the evolution of the control system is specified by Ordinary Differential Equations (ODEs), the embedded software periodically senses the state of the system, performs computation over the inputs, and initiates the actuators based on the result of computation. In this paper, we present a bounded time safety verification technique for periodically actuated linear control systems. The model considered in this paper takes into account that the control tasks are executed on a real time operating system and hence the task, in some instances misses the real time deadlines. Using matrix exponentiation, and symbolic evaluation of inputs, we reduce the verification problem of such systems into software verification with computation over reals. We compare different techniques for verifying such software, highlight the merits of each of the approaches, and present our experimental results.
KW - Abstract Interpretation Satisfiability Modulo Theories
KW - Bounded Model Checking
KW - Hybrid Systems
KW - Linear Control Systems
KW - Real-time Systems Verification
KW - Software Verification
KW - Verification of Closed Loop Systems
UR - http://www.scopus.com/inward/record.url?scp=84964608711&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84964608711&partnerID=8YFLogxK
U2 - 10.1109/RTSS.2015.28
DO - 10.1109/RTSS.2015.28
M3 - Conference contribution
AN - SCOPUS:84964608711
T3 - Proceedings - Real-Time Systems Symposium
SP - 216
EP - 226
BT - Proceedings - 2015 IEEE 36th Real-Time Systems Symposium, RTSS 2015
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 36th IEEE Real-Time Systems Symposium, RTSS 2015
Y2 - 1 December 2015 through 4 December 2015
ER -