
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Jin Song Dong, Ping Hao, Shengchao Qin, Jun Sun, Wang Yi, "Timed Automata Patterns," IEEE Transactions on Software Engineering, vol. 34, no. 6, pp. 844859, November/December, 2008.  
BibTex  x  
@article{ 10.1109/TSE.2008.52, author = {Jin Song Dong and Ping Hao and Shengchao Qin and Jun Sun and Wang Yi}, title = {Timed Automata Patterns}, journal ={IEEE Transactions on Software Engineering}, volume = {34}, number = {6}, issn = {00985589}, year = {2008}, pages = {844859}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2008.52}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Timed Automata Patterns IS  6 SN  00985589 SP844 EP859 EPD  844859 A1  Jin Song Dong, A1  Ping Hao, A1  Shengchao Qin, A1  Jun Sun, A1  Wang Yi, PY  2008 KW  Specification KW  Validation VL  34 JA  IEEE Transactions on Software Engineering ER   
[1] R. Alur, C. Couroubetis, and D.L. Dill, “ModelChecking for RealTime Systems,” Proc. Fifth Ann. IEEE Symp. Logic in Computer Science, pp. 414425, 1990.
[2] R. Alur and D.L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183235, 1994.
[3] S. Bornot and J. Sifakis, “Relating Time Progress and Deadlines in Hybrid Systems,” Proc. Int'l Workshop Hybrid and RealTime Systems, pp. 286300, 1997.
[4] S. Bornot, J. Sifakis, and S. Tripakis, “Modeling Urgency in Timed Systems,” Proc. Int'l Symp. Compositionality: The Significant Difference, pp. 103129, 1997.
[5] H. Bowman, “Modelling Timeouts without Timelocks,” Proc. Fifth Int'l AMAST Workshop Formal Methods for RealTime and Probabilistic Systems, pp. 334353, 1999.
[6] H. Bowman and R. Gómez, “How to Stop Time Stopping,” Formal Aspect of Computing, vol. 18, no. 4, pp. 459493, 2006.
[7] H. Bowman, R. Gómez, and L. Su, “A Tool for the Syntactic Detection of ZenoTimelocks in Timed Automata,” Electronic Notes in Theoretical Computer Science, vol. 139, no. 1, pp. 2547, 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, RealTime 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 RS0111, BRICS, Mar. 2001.
[12] J. Davies, Specification and Proof in RealTime 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. 161169, 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. 483498, 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. 342359, 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 ObjectZ,” Cornerstones of Computing, Macmillan, 2000.
[18] M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, “Patterns in Property Specifications for FiniteState Verification,” Proc. 21st Int'l Conf. Software Eng., pp. 411420, 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. 1924, 2005.
[20] C. Ghezzi, D. Mandrioli, and A. Morzenti, “Trio: A Logic Language for Executable Specifications of Realtime System,” J.Systems and Software, vol. 12, no. 2, pp. 107123, 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. 117133, 2006.
[23] L. Grunske, K. Winter, and R. Colvin, “Timed Behavior Trees and Their Application to Verifying RealTime Systems,” Proc. 18th Australian Software Eng. Conf., pp. 211222, 2007.
[24] D. Harel and E. Grey, “Executable Object Modeling with Statecharts,” Computer, vol. 30, no. 7, pp. 3142, 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 RealTime Systems Symp., pp. 213, 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. 245266, 2002.
[29] F. Jahanian and A.K. Mok, “A GraphTheoretic Approach for Timing Analysis and Its Implementation,” IEEE Trans. Computers, vol. 36, no. 8, pp. 961975, Aug. 1987.
[30] S. Konrad and B.H.C. Cheng, “RealTime Specification Patterns,” Proc. 27th Int'l Conf. Software Eng., pp. 372381, 2005.
[31] L.M. Lai and P. Watson, “A Case Study in Timed CSP: The Railroad Crossing Problem,” Proc. Int'l Workshop Hybrid and RealTime Systems, pp. 6974, 1997.
[32] K.G. Larsen, M. Mikucionis, B. Nielsen, and A. Skou, “Testing RealTime Embedded Software Using UPPAALTRON: An Industrial Case Study,” Proc. Fifth ACM Int'l Conf. Embedded Software, pp. 299306, 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. 12, pp.134152, 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. 353368, 2001.
[35] N.A. Lynch and F.W. Vaandrager, “Action Transducers and Timed Automata,” Formal Aspects of Computing, vol. 8, no. 5, pp.499538, 1996.
[36] B. Mahony and J.S. Dong, “Timed Communicating Object Z,” IEEE Trans. Software Eng., vol. 26, no. 2, pp. 150177, 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. 308327, 1998.
[38] J. Ouaknine and J. Worrell, “Timed CSP = Closed Timed EpsilonAutomata,” Nordic J. Computing, vol. 10, no. 2, pp. 99133, 2003.
[39] A.W. Roscoe, The Theory and Practice of Concurrency. Prentice Hall, 1997.
[40] S. Schneider, Concurrent and RealTime 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. 27, 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. 329356, 2002.
[43] J. Woodcock and J. Davies, Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.