Accession Number : ADA265408


Title :   The Priority Inversion Problem and Real-Time Symbolic Model Checking


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE


Personal Author(s) : Champos, Sergio V


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a265408.pdf


Report Date : 23 Apr 1993


Pagination or Media Count : 25


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


Descriptors :   *REAL TIME , *SYSTEMS ANALYSIS , *DEBUGGING(COMPUTERS) , ALGORITHMS , SYMBOLIC PROGRAMMING , PROBLEM SOLVING , INVERSION


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE