An interleaving model for real time

conference paper An interleaving model for real time published yes Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724 Zohar Manna author Amir Pnueli author JCIT: Jerusalem Conference on Information Technology The interleaving model is both adequate and sufficiently abstract to allow for the practical specification and verification of many properties of concurrent systems. We incorporate real time into this model by defining the abstract notion of a real-time transition system as a conservative extension of traditional transition systems: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upper-bound real-time requirements for transitions. We present proof rules to establish lower and upper real-time bounds for response properties of real-time transition systems. This proof system can be used to verify bounded-invariance and bounded-response properties, such as timely termination of shared-variables multi-process systems, whose semantics is defined in terms of real-time transition systems. IEEE1990Jerusalem, Israel eng Proceedings of the 5th Jerusalem Conference on Information Technology 0-8186-2078-110.1109/JCIT.1990.128356 717 - 730 yes T. A. Henzinger, Z. Manna, and A. Pnueli, “An interleaving model for real time,” in Proceedings of the 5th Jerusalem Conference on Information Technology, Jerusalem, Israel, 1990, pp. 717–730. Henzinger, T. A., Manna, Z., & Pnueli, A. (1990). An interleaving model for real time. In Proceedings of the 5th Jerusalem Conference on Information Technology (pp. 717–730). Jerusalem, Israel: IEEE. <a href="https://doi.org/10.1109/JCIT.1990.128356">https://doi.org/10.1109/JCIT.1990.128356</a> Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “An Interleaving Model for Real Time.” In Proceedings of the 5th Jerusalem Conference on Information Technology, 717–30. IEEE, 1990. <a href="https://doi.org/10.1109/JCIT.1990.128356">https://doi.org/10.1109/JCIT.1990.128356</a>. Henzinger, Thomas A., et al. “An Interleaving Model for Real Time.” Proceedings of the 5th Jerusalem Conference on Information Technology, IEEE, 1990, pp. 717–30, doi:<a href="https://doi.org/10.1109/JCIT.1990.128356">10.1109/JCIT.1990.128356</a>. Henzinger TA, Manna Z, Pnueli A. An interleaving model for real time. In: Proceedings of the 5th Jerusalem Conference on Information Technology. IEEE; 1990:717-730. doi:<a href="https://doi.org/10.1109/JCIT.1990.128356">10.1109/JCIT.1990.128356</a> Henzinger TA, Manna Z, Pnueli A. 1990. An interleaving model for real time. Proceedings of the 5th Jerusalem Conference on Information Technology. JCIT: Jerusalem Conference on Information Technology, 717–730. T.A. Henzinger, Z. Manna, A. Pnueli, in:, Proceedings of the 5th Jerusalem Conference on Information Technology, IEEE, 1990, pp. 717–730. 45102018-12-11T12:09:14Z2022-02-15T15:51:25Z