This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
TURTLE: A Real-Time UML Profile Supported by a Formal Validation Toolkit
July 2004 (vol. 30 no. 7)
pp. 473-487

Abstract—This paper presents a UML 1.5 profile named TURTLE (Timed UML and RT-LOTOS Environment) endowed with a formal semantics given in terms of RT-LOTOS. TURTLE relies on UML's extensibility mechanisms to enhance class and activity diagrams. Class diagrams are extended with specialized classes named Tclasses, which communicate and synchronize through gates. Also, associations between Tclasses are attributed by a composition operator (Parallel, Synchro, Invocation, Sequence, or Preemption) which provides them with a formal semantics. TURTLE extends UML activity diagrams with synchronization actions and temporal operators (deterministic delay, nondeterministic delay, time-limited offer, and time-capture). The real-time dimension of TURTLE has been further improved by the addition of two composition operators, Periodic and Suspend, as well as suspendable delay, latency, and time-limited offer operators at the activity diagram level. Core characteristics of TURLE are supported by TTool—the TURTLE toolkit—which includes a diagram editor, a RT-LOTOS code generator and a result analyzer. The toolkit reuses RTL, a RT-LOTOS validation tool offering debug-oriented simulation and exhaustive analysis. TTool hides RT-LOTOS to the end-user and allows him/her to directly check TURTLE modeling against logical errors and timing inconsistencies. Besides the foundations of the TURTLE profile, this paper also discusses its application in the context of space-based embedded software.

[1] C. André, M.-A. Peraldi-Frati, and J.-P. Rigault, Integrating the Synchronous Paradigm into UML: Application to Control-Dominated Systems Proc. Int'l Conf. Unified Modeling Language, J.-M. Jézéquel, H. Hußmann, and S. Cook, eds., 2002.
[2] L. Apvrille, P. de Saqui-Sannes, C. Lohr, P. Sénac, and J.-P. Courtiat, A New UML Profile for Real-Time System Formal Design and Validation Proc. Int'l Conf. Unified Modeling Language, M. Gogolla and C. Kobryn, eds., pp. 287-301, 2001.
[3] L. Apvrille, P. de Saqui-Sannes, and F. Khendek, TURTLE-P: A UML Profile for Distributed Architecture Validation Proc. Colloque Francophone sur l'Ingénierie des Protocoles, Oct. 2003.
[4] L. Apvrille, P. de Saqui-Sannes, P. Sénac, and C. Lohr, Verifying Service Continuity in a Dynamic Reconfiguration Procedure: Application to a Satellite System Automated Software Eng., vol. 11, no. 2, Apr. 2004.
[5] Artisan Software,http://www.artisansw.com/UMLCenterUML. asp , 2003.
[6] M. Bjorkander, Real-Time Systems in UML and SDL Embedded System Eng., Oct./Nov. 2000, http:/www.telelogic.com.
[7] J.-M. Bruel, Integrating Formal and Informal Specification Techniques. Why? How? Proc. IEEE Workshop Industrial-Strength Formal Specification Techniques, 1999.
[8] R.G. Clarck and A.M.D. Moreira, Use of E-LOTOS in Adding Formality to UML J. Universal Computer Science, vol. 6, no. 11, pp. 1071-1087, 2000.
[9] K. Compton, Y. Gurevich, J. Huggins, and W. Shen, An Automatic Verification Tool for UML Technical Report CSE-TRE-423-00, Univ. of Michigan, 2000.
[10] S. Combes, C. Fouquet, and V. Renat, Packet-Based DAMA Protocols for New Generation Satellite Networks Proc. 19th AIAA Int'l Comm. Satellite Systems Conf., 2001.
[11] J.-P. Courtiat, C.A.S. Santos, C. Lohr, and B. Outtaj, Experience with RT-LOTOS, a Temporal Extension of the LOTOS Formal Description Technique Computer Comm., vol. 23, no. 12, pp. 1104-1123, 2000.
[12] W. Damm, B. Josko, A. Votintseva, and A. Pnueli, A Formal Semantics for a UML Kernel Language OMEGA project deliverable IST/33522/WP1.1/D1.1.2, Jan. 2003.
[13] J. Delatour and M. Paludetto, UML/PNO, a Way to Merge UML and Petri Net Objects for the Analysis of Real-Time Systems Proc. Workshop Object-Oriented Technology and Real Time Systems (ECOOP '98), 1998.
[14] K. Diethers, U. Goltz, and M. Huhn, Model Checking UML Statecharts with Time Proc. Workshop on Critical Systems Development with UML (UML '02), J.-M. Jézéquel, H. Hußmann, and S. Cook, eds., 2002.
[15] L. Doldi, UML2 illustrated: Developing Real-Time and Communications Systems. TMSO, Oct. 2003.
[16] S. Dupuy and L. du Bouquet, A Multi-Formalism Approach for the Validation of UML Models Formal Aspects of Computing, no. 12, pp. 228-230, 2001.
[17] ESTEC,http://www.estec.esa.nl/wsmwww/erc32erc32.html , free simulation software for ERC-32:http://www.estec.esa.nl/wsmwww/erc32freesoft.html , 1999.
[18] A.S. Evans, S. Cook, S. Mellor, J. Warmer, and A. Wills, Advanced Methods and Tools for a Precise UML Proc. Second Int'l Conf. Unified Modeling Language (UML '99), 1999.
[19] S. Flake and W. Mueller, A UML Profile for Real-Time Constraints with the OCL Proc. Int'l Conf. Unified Modeling Language, J.-M. Jézéquel, H. Hußmann, S. Cook, eds., 2002.
[20] S. Gerard, F. Terrier, and Y. Tanguy, Using the Model Paradigm for Real-Time Systems Development: ACCORD/UML Proc. Conf. Advances in Object-Oriented Information Systems, OOIS 2002 Workshops, J.-M. Bruel and Z. Bellahsene, eds., pp. 260-269, 2002.
[21] A. Le Guennec, Méthodes Formelles avec UML: Modélisation, Validation et Génération de Tests Actes du 8éme Colloque Francophone sur l'Ingénierie des Protocoles (CFIP '2000), pp. 151-166, 2000.
[22] J. Hooman, Towards Formal Support for UML-Based Development of Embedded Systems Proc. PROGRESS Workshop Embedded Systems, Oct. 2002.
[23] C. Jard, J.-F. Monin, and R. Groz, Development of Véda, A Prototyping Tool for Distributed Algorithms IEEE Trans. Software Eng., vol. 14, no. 3, Mar. 1988.
[24] Kronos,http://www-verimag.imag.fr/TEMPORISEkronos , 2002.
[25] R. Laleau and A. Mammar, An Overview of a Method and Its Support Tool for Generating B Specifications from UML Notations Proc. 15th IEEE Int'l Conf. Automated Software Eng., 2000.
[26] J. Lilius and I.P. Paltor, vUML: A Tool for Verifying UML Models Proc. 14th IEEE Int'l Conf. Automated Software Eng., 1999.
[27] C. Lohr and J.-P. Courtiat, From the Specification to the Scheduling of Time-Dependent Systems Proc. Seventh Int'l Symp. Formal Techniques in Real-Time and Fault Tolerant Systems, pp. 129-145, 2002.
[28] C. Lohr, L. Apvrille, P. de Saqui-Sannes, and J.-P. Courtiat, New Operators for the TURTLE Real-Time UML Profile Proc. IFIP Int'l Conf. Formal Methods for Open Object-Based Distributed Systems, E. Najm, U. Nestmann, and P. Stevens, eds., pp. 214-228, 2003.
[29] Object Management Group, Unified Modeling Language Specification Version 1.5,http://www.omg.org/docs/formal03-03-01.pdf , Mar. 2003.
[30] Object Management Group, UML 2.0 Superstructure Specification http://www.omg.org/docs/ptc03-08-02.pdf, 2003.
[31] http://www.ilogix.com/products/rhapsodyindex.cfm , 2003.
[32] http:/www.rational.com, 2003.
[33] L. Roullet et al., SAGAM Demonstrator of a G.E.O. Satellite Multimedia Access System: Architecture&Integrated Resource Manager Proc. European Conf. Satellite Comm., 1999.
[34] Real-time LOTOS,http://www.laas.frRT-LOTOS, 1998.
[35] B. Selic and J. Rumbaugh, Using UML for Modeling Complex Real-Time Systems http:/www.rational.com, 1998.
[36] http:/www.telelogic.com, 2003.
[37] B.D Theelen, P.H.A. van der Putten, and J.P.M. Voeten, Using the SHE Method for UML-Based Performance Modeling Proc. Forum on Specification and Design Languages (FDL '02), 2002.
[38] I. Traoré, An Outline of PVS Semantics for UML Statecharts J. Universal Computer Science, vol. 6, no. 11, pp. 1088-1108, 2000.
[39] http://www.eurecom.fr/apvrille/TURTLEindex.html , 2003.

Index Terms:
Real-time systems, UML, RT-LOTOS, formal validation.
Citation:
Ludovic Apvrille, Jean-Pierre Courtiat, Christophe Lohr, Pierre de Saqui-Sannes, "TURTLE: A Real-Time UML Profile Supported by a Formal Validation Toolkit," IEEE Transactions on Software Engineering, vol. 30, no. 7, pp. 473-487, July 2004, doi:10.1109/TSE.2004.34
Usage of this product signifies your acceptance of the Terms of Use.