The Priority Inversion Problem and Real-Time Symbolic Model Checking

Abstract

Priority inversion is a serious problem that can make real time systems unpredictable in subtle ways. This makes it more difficult to implement and debug such systems. Our work discusses this problem and presents one possible solution. The solution is formalized and verified using temporal logic model checking techniques. In order to perform the verification, the BDD-based symbolic model checking algorithm given in previous works was extended to handle real-time properties using the bounded until operator. We believe that this algorithm, which is based on discrete time, is able to handle many real-time properties that arise in practical problems

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 23, 1993
Accession Number
ADA265408

Entities

People

  • Sergio V. Champos

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Air Traffic
  • Air Traffic Control Systems
  • Air Traffic Controllers
  • Algorithms
  • Analyzers
  • Computations
  • Computer Science
  • Computers
  • Consumers
  • Control Systems
  • Detectors
  • Guarantees
  • Inversion
  • Iterations
  • Language
  • Neurobehavioral Manifestations
  • Time Intervals

Fields of Study

  • Computer science

Readers

  • Acoustical Oceanography.
  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Distributed Systems and Data Platform Development