Abstract
The major problem of checking a parallel composition of real-time systems for a real-time property is the explosion of untimed states and time regions. To attack this problem, one can use bisimulation equivalence w.r.t. the property to be checked to minimise the system state space. In this paper, we define such equivalence for the integrated linear duration properties of real-time automaton networks with shared variables. To avoid exhaustive state space exploration, we define a compatibility relation, which is a one-direction simulation relation between configurations. Based on this technique, we develop an algorithm for checking a real-time automaton network with shared variables w.r.t. a linear duration property. Our algorithm can avoid exhaustive state space exploration significantly when applied to Fischer’s mutual exclusion protocol.
On leave from Department of Computer Science, Nanjing University, Nanjing 210093, P.R. China. email: seg@nju.edu.cn. Partly supported by National NSF.
On leave from the Institute of Information Technology, Nghia Do, Tu Liem, Hanoi, Vietnam.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, and T.A. Henzinger. Computing accumulated delays in real-time systems. In Proceedings of the Fifth Conference on Computer-Aided Verification, LNCS 693, pages 181–193. Springer-Verlag, 1993.
R. Alur and D. Dill. Automata for Modelling Real-Time Systems. In Proc. of ICALP’90, LNCS 443, 1990.
C.Daws, A.Olivero, S.Tripakis, and S.Yovine. The tool Kronos. In Hybrid Systems III, Verification and Control, number 1066 in Lecture Notes in Computer Science. Springer-Verlag, 1996.
Zhou Chaochen, C.A.R. Hoare, and A.P. Ravn. A Calculus of Durations. In Information Processing Letter 40,5, pages 269–276, 1991.
Zhou Chaochen, Zhang Jingzhong, Yang Lu, and Li Xiaoshan. Linear Duration Invariants. Research Report 11, UNU/IIST, P.O.Box 3058, Macau, July 1993. Published in: Formal Techniques in Real-Time and Fault-Tolerant systems, LNCS 863, 1994.
Li Xuan Dong and Dang Van Hung. Checking Linear Duration invariants by Linear Programming. Research Report 70, UNU/IIST, P.O.Box 3058, Macau, May 1996. Published in Joxan Jaffar and Roland H. C. yap (Eds.), Concurrency and Palalellism, Programming, Networking, and Securiry LNCS 1179, Springer-Verlag, Dec 1996, pp. 321–332.
Li Xuan Dong, Dang Van Hung, and Zheng Tao. Checking Hybrid Automata for Linear Duration Invariants. Research Report 109, UNU/IIST, P.O.Box 3058, Macau, June 1997. Published in R.K.Shamasundar, K.Ueda (Eds.), Advances in Computing Science, Lecture Notes in Computer Science 1345, Springer-Verlag, pp.166–180.
Kere J. Kristoffersen, Francois Larroussinie, Kim G.Larsen, Paul Pettersson, and Wang Yi. A Compositional Proof of a Real-Time Mutual Exclusion Protocol. In Proceedings of TAPSOFT’97, the 7th International Joint Conference on the Theory and Practice of Software Development, pages 14–18, April 1997.
Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction. December 1997. Accepted for presentation at the 18th IEEE Real-Time Systems Symposium. San Francisco, California, USA.
Kim G Larsen and Paul Pettersson Wang Yi. UPPAAL: Status & Developments. In Orna Grumberg, editor, Proceedings of the 9th International Conference on Computer-Aided Verification. Haifa, Israel, LNCS 1254, pages 456–459. Springer-Verlag, June 1997.
T.A.Henzinger, P.-H. Ho, and H. Wong-Toi. A Users Guide to HyTech. Technical report, Department of Computer Science, Cornell University, 1995.
Pham Hong Thai and Dang Van Hung. Checking a regular class of Duration Calculus Models for Linear Duration Invariants. Technical Report 118, UNU/IIST, P.O.Box 3058, Macau, July 1997. Published in the Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems (PDSE’98), 20–21 April 1998, Kyoto, Japan, Bernd Kramer, Naoshi Uchihira, Peter Croll and Stefano Russo (Eds), IEEE Computer Society Press, 1998, pp. 61–71.
Mihalis Yannakakis and David Lee. An Efficient Algorithm for Minimizing Real-Time Transition Systems. Formal Methods in System Design, 11(2):113–136, August 1997.
Y.Kesten, A.Pnueli, J.Sifakis, and S.Yovine. Integration Graphs: A Class of Decidable Hybrid Systems. In Hybrid System, number 736 in LNCS, pages 179–208, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jianhua, Z., Van Hung, D. (1998). On checking parallel real-time systems for linear duration properties. In: Ravn, A.P., Rischel, H. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1998. Lecture Notes in Computer Science, vol 1486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055351
Download citation
DOI: https://doi.org/10.1007/BFb0055351
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65003-4
Online ISBN: 978-3-540-49792-9
eBook Packages: Springer Book Archive