Specifying and verifying a real-time priority queue with modal algebra

Yodaiken, V. ; Ramamritham, K. (1990) Specifying and verifying a real-time priority queue with modal algebra Proceedings of the 11th IEEE Symposium on Real-Time Systems . pp. 300-310.

Full text not available from this repository.

Official URL: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnum...

Related URL: http://dx.doi.org/10.1109/REAL.1990.128761


The authors use the modal primitive recursive (MPR) arithmetic to facilitate definition, composition, and reasoning about the very large-scale finite state machines that represent substantive real-time systems. The MPR arithmetic provides a language of integer-valued functions which allow for compact and intuitive specification of state machines without enumeration of state sets or transition functions. The MPR arithmetic proof system is intended to be as close as possible to the proof system of classical algebra. The expressive range of the language extends from detailed description of multilevel concurrent algorithms to abstract properties of liveness and safety in a style similar to that of the temporal logics. The behavior of a real-time priority queue or communication pipeline is specified with MPR as an example, and the correctness of an implementation is verified.

Item Type:Article
Source:Copyright of this article belongs to IEEE Press.
ID Code:94337
Deposited On:05 Sep 2012 06:44
Last Modified:05 Sep 2012 06:44

Repository Staff Only: item control page