The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.06 - November/December (2008 vol.34)
pp: 844-859
Jin Song Dong , National University of Singapore, Singapore
Ping Hao , National University of Singapore, Singapore
Shengchao Qin , Durham University, Durham
Jun Sun , National University of Singapore, Singapore
Wang Yi , North Eastern University, China, and Uppsala University, Sweden
ABSTRACT
Timed Automata have proven to be useful for specification and verification of real-time systems. System design using Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have been developed. However, Timed Automata lack of composable patterns for high-level system design. Logic-based specification languages like Timed CSP and TCOZ are well suited for presenting compositional models of complex real-time systems. In this work, we define a set of composable Timed Automata patterns based on hierarchical constructs in timed enriched process algebras. The patterns facilitate hierarchical design of complex systems using Timed Automata. They also allow a systematic translation from Timed CSP/TCOZ models to Timed Automata so that analyzers for Timed Automata can be used to reason about TCOZ models. A prototype has been developed to support system design using Timed Automata patterns or, if given a TCOZ specification, to automate the translation from TCOZ to Timed Automata.
INDEX TERMS
Specification, Validation
CITATION
Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, Wang Yi, "Timed Automata Patterns", IEEE Transactions on Software Engineering, vol.34, no. 6, pp. 844-859, November/December 2008, doi:10.1109/TSE.2008.52
REFERENCES
[1] R. Alur, C. Couroubetis, and D.L. Dill, “Model-Checking for Real-Time Systems,” Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 414-425, 1990.
[2] R. Alur and D.L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183-235, 1994.
[3] S. Bornot and J. Sifakis, “Relating Time Progress and Deadlines in Hybrid Systems,” Proc. Int'l Workshop Hybrid and Real-Time Systems, pp. 286-300, 1997.
[4] S. Bornot, J. Sifakis, and S. Tripakis, “Modeling Urgency in Timed Systems,” Proc. Int'l Symp. Compositionality: The Significant Difference, pp. 103-129, 1997.
[5] H. Bowman, “Modelling Timeouts without Timelocks,” Proc. Fifth Int'l AMAST Workshop Formal Methods for Real-Time and Probabilistic Systems, pp. 334-353, 1999.
[6] H. Bowman and R. Gómez, “How to Stop Time Stopping,” Formal Aspect of Computing, vol. 18, no. 4, pp. 459-493, 2006.
[7] H. Bowman, R. Gómez, and L. Su, “A Tool for the Syntactic Detection of Zeno-Timelocks in Timed Automata,” Electronic Notes in Theoretical Computer Science, vol. 139, no. 1, pp. 25-47, 2005.
[8] P. Brooke, “A Timed Semantics for a Hierarchical Design Notation,” PhD dissertation, Univ. of York, 1999.
[9] S.D. Brooke, “A Model for Communicating Sequential Processes,” PhD dissertation, Oxford Univ., 1983.
[10] A.M.K. Cheng, Real-Time Systems: Scheduling, Analysis, and Verification. John Wiley & Sons, 2002.
[11] A. David and M.O. Möller, “From HUPPAAL to UPPAAL: A Translation from Hierarchical Timed Automata to Flat Timed Automata,” Technical Report RS-01-11, BRICS, Mar. 2001.
[12] J. Davies, Specification and Proof in Real-Time CSP. Cambridge Univ. Press, 1993.
[13] J.S. Dong, N. Fulton, L. Zucconi, and J. Colton, “Formalizing Process Scheduling Requirements for an Aircraft Operational Flight Program,” Proc. First IEEE Int'l Conf. Formal Eng. Methods, pp. 161-169, 1997.
[14] J.S. Dong, P. Hao, S.C. Qin, J. Sun, and W. Yi, “Timed Patterns: TCOZ to Timed Automata,” Proc. Sixth Int'l Conf. Formal Eng. Methods, pp. 483-498, 2004.
[15] J.S. Dong, P. Hao, J. Sun, and X. Zhang, “A Reasoning Method for Timed CSP Based on Constraint Solving,” Proc. Eighth Int'l Conf. Formal Eng. Methods, pp. 342-359, 2006.
[16] J.S. Dong, B.P. Mahony, and N. Fulton, “Modeling Aircraft Mission Computer Task Rates,” Proc. World Congress on Formal Methods, p. 1855, 1999.
[17] R. Duke and G. Rose, “Formal Object Oriented Specification Using Object-Z,” Cornerstones of Computing, Macmillan, 2000.
[18] M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, “Patterns in Property Specifications for Finite-State Verification,” Proc. 21st Int'l Conf. Software Eng., pp. 411-420, 1999.
[19] H. Fuhrmann, J. Koch, J. Rennhack, and R.v. Hanxleden, “The Aerospace Demonstrator of DECOS,” Proc. Eighth Int'l IEEE Conf. Intelligent Transportation Systems, pp. 19-24, 2005.
[20] C. Ghezzi, D. Mandrioli, and A. Morzenti, “Trio: A Logic Language for Executable Specifications of Real-time System,” J.Systems and Software, vol. 12, no. 2, pp. 107-123, May 1990.
[21] UML Resource Page, Object Management Group, http://www.omg.orguml/, 2008.
[22] V. Gruhn and R. Laue, “Patterns for Timed Property Specifications,” Electronic Notes in Theoretical Computer Science, vol. 153, no. 2, pp. 117-133, 2006.
[23] L. Grunske, K. Winter, and R. Colvin, “Timed Behavior Trees and Their Application to Verifying Real-Time Systems,” Proc. 18th Australian Software Eng. Conf., pp. 211-222, 2007.
[24] D. Harel and E. Grey, “Executable Object Modeling with Statecharts,” Computer, vol. 30, no. 7, pp. 31-42, July 1997.
[25] K. Havelund, A. Skou, K.G. Larsen, and K. Lund, “Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using UPPAAL,” Proc. 18th IEEE Real-Time Systems Symp., pp. 2-13, 1997.
[26] I.J. Hayes and M. Utting, “Deadlines Are Termination,” Proc. IFIP Working Conf. Programming Concepts and Methods, 1998.
[27] C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall, 1985.
[28] J. Hoenicke and E.-R. Olderog, “Combining Specification Techniques for Processes, Data and Time,” Proc. Third Int'l Conf. Integrated Formal Methods, pp. 245-266, 2002.
[29] F. Jahanian and A.K. Mok, “A Graph-Theoretic Approach for Timing Analysis and Its Implementation,” IEEE Trans. Computers, vol. 36, no. 8, pp. 961-975, Aug. 1987.
[30] S. Konrad and B.H.C. Cheng, “Real-Time Specification Patterns,” Proc. 27th Int'l Conf. Software Eng., pp. 372-381, 2005.
[31] L.M. Lai and P. Watson, “A Case Study in Timed CSP: The Railroad Crossing Problem,” Proc. Int'l Workshop Hybrid and Real-Time Systems, pp. 69-74, 1997.
[32] K.G. Larsen, M. Mikucionis, B. Nielsen, and A. Skou, “Testing Real-Time Embedded Software Using UPPAAL-TRON: An Industrial Case Study,” Proc. Fifth ACM Int'l Conf. Embedded Software, pp. 299-306, 2005.
[33] K.G. Larsen, P. Pettersson, and Y. Wang, “Uppaal in a Nutshell,” Int'l J. Software Tools for Technology Transfer, vol. 1, nos. 1-2, pp.134-152, 1997.
[34] M. Lindahl, P. Pettersson, and Y. Wang, “Formal Design and Analysis of a Gearbox Controller,” Springer Int'l J. Software Tools for Technology Transfer, vol. 3, no. 3, pp. 353-368, 2001.
[35] N.A. Lynch and F.W. Vaandrager, “Action Transducers and Timed Automata,” Formal Aspects of Computing, vol. 8, no. 5, pp.499-538, 1996.
[36] B. Mahony and J.S. Dong, “Timed Communicating Object Z,” IEEE Trans. Software Eng., vol. 26, no. 2, pp. 150-177, Feb. 2000.
[37] B.P. Mahony and J.S. Dong, “Network Topology and a Case Study in TCOZ,” Proc. 11th Int'l Conf. Z Users, pp. 308-327, 1998.
[38] J. Ouaknine and J. Worrell, “Timed CSP = Closed Timed Epsilon-Automata,” Nordic J. Computing, vol. 10, no. 2, pp. 99-133, 2003.
[39] A.W. Roscoe, The Theory and Practice of Concurrency. Prentice Hall, 1997.
[40] S. Schneider, Concurrent and Real-Time Systems. John Wiley & Sons, 2000.
[41] J. Sifakis, “The Compositional Specification of Timed Systems—A Tutorial,” Proc. 11th Int'l Conf. Computer Aided Verification, pp. 2-7, 1999.
[42] J. Sun, J.S. Dong, J. Liu, and H. Wang, “A Formal Object Approach to the Design of ZML,” Annals of Software Eng., vol. 13, pp. 329-356, 2002.
[43] J. Woodcock and J. Davies, Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.
6 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool