Analyzing Real Time Linear Control Systems Using Software Verification
Real-Time Systems Symposium(2015)
摘要
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.
更多查看译文
关键词
Verification of Closed Loop Systems,Real-time Systems Verification,Hybrid Systems,Software Verification,Abstract Interpretation Satisfiability Modulo Theories,Bounded Model Checking,Linear Control Systems
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络