Software Engineering Institute | Carnegie Mellon University
Software Engineering Institute | Carnegie Mellon University

Digital Library

Javascript is currently disabled for your browser. For an optimal search experience, please enable javascript.

Advanced Search

Basic Search

Content Type


Publication Date


Verifying Periodic Real-Time Software

  • August 2014
  • Colloquium presentation for Oregon University EECS Department that discusses recent developments in SEI's ongoing research on verifying periodic programs.
  • Cyber-Physical Systems
  • Publisher: Software Engineering Institute
  • Abstract

    Abstract: In this talk, I will present recent developments in our ongoing research on verifying periodic programs -- a commonly used form of real-time software that consists of a set of asynchronous tasks running periodically and being scheduled preemptively based on their priorities. We focus on an approach based on sequentialization -- reducing the verification of a time-bounded periodic program to that of an equivalent sequential program. We present a new compositional form of sequentialization that improves on earlier work in terms of both scalability and completeness (i.e., false warnings) by leveraging temporal separation between jobs in the same hyper-period and across multiple hyper-periods. We also show how the new sequentialization can be further improved in the case of harmonic systems to generate sequential programs of asymptotically smaller size. Experiments indicate that our new sequentialization improves verification time by orders of magnitude compared to competing schemes. This is joint work with Arie Gurfinkel, Soonho Kong, and Ofer Strichman. Further details available at:
    Originally presented at the Oregon State University Colloquium, October 2013.