Analyzing Real Time Linear Control Systems Using Software Verification

Parasara Sridhar Duggirala, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationProceedings - 2015 IEEE 36th Real-Time Systems Symposium, RTSS 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages11
ISBN (Electronic)9781467395076
StatePublished - Jan 14 2016
Event36th IEEE Real-Time Systems Symposium, RTSS 2015 - San Antonio, United States
Duration: Dec 1 2015Dec 4 2015

Publication series

NameProceedings - Real-Time Systems Symposium
ISSN (Print)1052-8725


Other36th IEEE Real-Time Systems Symposium, RTSS 2015
Country/TerritoryUnited States
CitySan Antonio


  • Abstract Interpretation Satisfiability Modulo Theories
  • Bounded Model Checking
  • Hybrid Systems
  • Linear Control Systems
  • Real-time Systems Verification
  • Software Verification
  • Verification of Closed Loop Systems

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications


Dive into the research topics of 'Analyzing Real Time Linear Control Systems Using Software Verification'. Together they form a unique fingerprint.

Cite this