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

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2008.52

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.52REFERENCES

- [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. |