{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:24:09Z","timestamp":1761488649719,"version":"3.41.0"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2011,1,24]],"date-time":"2011-01-24T00:00:00Z","timestamp":1295827200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2011,1,24]]},"abstract":"<jats:p>Using UML or SysML models in a verification-centric method requires a property expression language, a formal semantics, and a tool. The paper introduces TEPE, a graphical TEmporal Property Expression language based on SysML parametric diagrams. TEPE enriches the expressiveness of other common property languages in particular with the notion of physical time and unordered signal reception. TEPE is further instantiated in the AVATAR real-time UML profile. TTool, an open-source toolkit, implements a press-button approach for the formal verification of AVATAR-TEPE properties with UPPAAL. An elevator system serves as example<\/jats:p>","DOI":"10.1145\/1921532.1921556","type":"journal-article","created":{"date-parts":[[2011,3,17]],"date-time":"2011-03-17T12:40:16Z","timestamp":1300365616000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["TEPE"],"prefix":"10.1145","volume":"36","author":[{"given":"Daniel","family":"Knorreck","sequence":"first","affiliation":[{"name":"Institut Telecom \/ Telecom ParisTech, LTCI CNRS, Sophia-Antipolis Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ludovic","family":"Apvrille","sequence":"additional","affiliation":[{"name":"Institut Telecom \/ Telecom ParisTech, LTCI CNRS, Sophia-Antipolis Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"de Saqui-Sannes","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Toulouse, LAAS-CNRS, ISAE, Cedex 4, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,1,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.34"},{"key":"e_1_2_1_2_1","volume-title":"Top-cased 3.4 tutorial - requirement management. In http:\/\/www.topcased.org\/index.php? documentsSynthesis=y&Itemid=59","author":"Audrain M.","year":"2010","unstructured":"M. Audrain and B. Marconato . Top-cased 3.4 tutorial - requirement management. In http:\/\/www.topcased.org\/index.php? documentsSynthesis=y&Itemid=59 , 2010 . M. Audrain and B. Marconato. Top-cased 3.4 tutorial - requirement management. In http:\/\/www.topcased.org\/index.php? documentsSynthesis=y&Itemid=59, 2010."},{"key":"e_1_2_1_3_1","unstructured":"Accellera Organization Inc. SystemVerilog 3.1a Language Reference Manual www.systemverilog.org.  Accellera Organization Inc. SystemVerilog 3.1a Language Reference Manual www.systemverilog.org."},{"key":"e_1_2_1_4_1","volume-title":"Property specification language, reference manual, version 1.1","author":"Accellera Organization Inc.","year":"2004","unstructured":"Accellera Organization Inc. Property specification language, reference manual, version 1.1 . 2004 . Accellera Organization Inc. Property specification language, reference manual, version 1.1. 2004."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1416729.1416764"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 12th European Workshop on Dependable Computing","author":"Apvrille Ludovic","year":"2009","unstructured":"Ludovic Apvrille and Pierre De Saqui-Sannes . Making formal verification amenable to real-time UML practitioners . In Proceedings of the 12th European Workshop on Dependable Computing , Toulouse, France , May 2009 . Ludovic Apvrille and Pierre De Saqui-Sannes. Making formal verification amenable to real-time UML practitioners. In Proceedings of the 12th European Workshop on Dependable Computing, Toulouse, France, May 2009."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011227529550"},{"key":"e_1_2_1_8_1","volume-title":"Brasilian Symposium on Aeropspace Engineering and Applications, S\u00e3o Jos\u00e9 dos Campos, SP","author":"da Silva E. C.","year":"2009","unstructured":"E. C. da Silva and E. Villani . Integrando SysML e model checking para v&v de software cr\u00edtico espacial . In Brasilian Symposium on Aeropspace Engineering and Applications, S\u00e3o Jos\u00e9 dos Campos, SP , Brasil , September 2009 . E. C. da Silva and E. Villani. Integrando SysML e model checking para v&v de software cr\u00edtico espacial. In Brasilian Symposium on Aeropspace Engineering and Applications, S\u00e3o Jos\u00e9 dos Campos, SP, Brasil, September 2009."},{"key":"e_1_2_1_9_1","volume-title":"ERTSS - Embedded Real Time Software and Systems","author":"Fontan B.","year":"2008","unstructured":"B. Fontan , P. De Saqui-sannes, and L. Apvrille . Timing requirement description diagrams for real-time system verification . In ERTSS - Embedded Real Time Software and Systems , Jan 2008 . B. Fontan, P. De Saqui-sannes, and L. Apvrille. Timing requirement description diagrams for real-time system verification. In ERTSS - Embedded Real Time Software and Systems, Jan 2008."},{"key":"e_1_2_1_10_1","volume-title":"Testing solutions with UML\/SysML. In http:\/\/www.artistembedded.org\/docs\/Events\/2010\/UML AADL\/slides\/Session1 Matthew Hause.pdf","author":"Hause M.","year":"2010","unstructured":"M. Hause and J. Holt . Testing solutions with UML\/SysML. In http:\/\/www.artistembedded.org\/docs\/Events\/2010\/UML AADL\/slides\/Session1 Matthew Hause.pdf , 2010 . M. Hause and J. Holt. Testing solutions with UML\/SysML. In http:\/\/www.artistembedded.org\/docs\/Events\/2010\/UML AADL\/slides\/Session1 Matthew Hause.pdf, 2010."},{"key":"e_1_2_1_11_1","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/978-3-642-02571-6_18","volume-title":"Objects, Components, Models and Patterns","author":"Knorreck Daniel","year":"2009","unstructured":"Daniel Knorreck , Ludovic Apvrille , and Renaud Pacalet . Fast simulation techniques for design space exploration . In Objects, Components, Models and Patterns , volume 33 of Lecture Notes in Business Information Processing , pages 308 -- 327 . Springer Berlin Heidelberg , 2009 . Daniel Knorreck, Ludovic Apvrille, and Renaud Pacalet. Fast simulation techniques for design space exploration. In Objects, Components, Models and Patterns, volume 33 of Lecture Notes in Business Information Processing, pages 308--327. Springer Berlin Heidelberg, 2009."},{"key":"e_1_2_1_12_1","volume-title":"ERTSS - Embedded Real Time Software and Systems","author":"Knorreck Daniel","year":"2010","unstructured":"Daniel Knorreck , Ludovic Apvrille , and Renaud Pacalet . An interactive system level simulation environment for Systems on Chip . In ERTSS - Embedded Real Time Software and Systems , May 2010 . Daniel Knorreck, Ludovic Apvrille, and Renaud Pacalet. An interactive system level simulation environment for Systems on Chip. In ERTSS - Embedded Real Time Software and Systems, May 2010."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2010.41"},{"key":"e_1_2_1_14_1","volume-title":"A UML profile for MARTE, beta 2, www.omg.org","author":"OMG.","year":"2008","unstructured":"OMG. A UML profile for MARTE, beta 2, www.omg.org . 2008 . OMG. A UML profile for MARTE, beta 2, www.omg.org. 2008."},{"key":"e_1_2_1_15_1","volume-title":"SystemC Verification Standard Specification Version 1.0e, www.systemc.org","author":"Members of the SystemC Verification Working Group","year":"2003","unstructured":"Members of the SystemC Verification Working Group . SystemC Verification Standard Specification Version 1.0e, www.systemc.org . 2003 . Members of the SystemC Verification Working Group. SystemC Verification Standard Specification Version 1.0e, www.systemc.org. 2003."},{"key":"e_1_2_1_16_1","unstructured":"SysML companion. In http:\/\/www.realtimeatwork.com\/?page id=683.  SysML companion. In http:\/\/www.realtimeatwork.com\/?page id=683."},{"key":"e_1_2_1_17_1","first-page":"14","volume-title":"In Proceedings of the 5th International Symposium on Requirements Engineering","author":"Smith Margaret H.","year":"2001","unstructured":"Margaret H. Smith . Events and constraints: a graphical editor for capturing logic properties of programs . In In Proceedings of the 5th International Symposium on Requirements Engineering , pages 14 -- 22 , 2001 . Margaret H. Smith. Events and constraints: a graphical editor for capturing logic properties of programs. In In Proceedings of the 5th International Symposium on Requirements Engineering, pages 14--22, 2001."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1131481.1131512"},{"key":"e_1_2_1_19_1","volume-title":"e Language Reference Manual, www.ieee1647.org\/downloads\/prelim_e_lrm.pdf","author":"Verisity Design Inc.","year":"2002","unstructured":"Verisity Design Inc. e Language Reference Manual, www.ieee1647.org\/downloads\/prelim_e_lrm.pdf . 2002 . Verisity Design Inc. e Language Reference Manual, www.ieee1647.org\/downloads\/prelim_e_lrm.pdf. 2002."}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1921532.1921556","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1921532.1921556","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:41Z","timestamp":1750248521000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1921532.1921556"}},"subtitle":["a SysML language for time-constrained property modeling and formal verification"],"short-title":[],"issued":{"date-parts":[[2011,1,24]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1,24]]}},"alternative-id":["10.1145\/1921532.1921556"],"URL":"https:\/\/doi.org\/10.1145\/1921532.1921556","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2011,1,24]]},"assertion":[{"value":"2011-01-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}