{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:31:10Z","timestamp":1750307470693,"version":"3.41.0"},"reference-count":24,"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>MARTE\/CCSL specifications express chronological and causal relations on UML models. In a previous work, we proposed a mechanism to verify Esterel implementations against MARTE\/CCSL specifications. The mechanism was thought to be general enough to be extended to other languages. However, preserving the polychronous semantics of CCSL was pretty easy with a synchronous language but is much harder when the target language does not directly support coincidence\/simultaneity. We show here how coincidence can be encoded. The process is illustrated using VHDL<\/jats:p>","DOI":"10.1145\/1921532.1921554","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":2,"title":["Logical time"],"prefix":"10.1145","volume":"36","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Mallet","sequence":"first","affiliation":[{"name":"Universit\u00e9 Nice Sophia Antipolis, INRIA Sophia Antipolis M\u00e9diterran\u00e9e"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charles","family":"Andr\u00e9","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Nice Sophia Antipolis, INRIA Sophia Antipolis M\u00e9diterran\u00e9e"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"de Simone","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Nice Sophia Antipolis, INRIA Sophia Antipolis M\u00e9diterran\u00e9e"}],"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":"crossref","unstructured":"Luca\n      Aceto Augusto\n      Burgue\u00f1o and \n      Kim Guldstrand\n      Larsen\n    .\n  Model checking via reachability testing for timed automata\n  . In Bernhard Steffen editor TACAS volume \n  1384\n   of \n  Lecture Notes in Computer Science pages \n  263\n  --\n  280\n  . \n  Springer 1998\n  .   Luca Aceto Augusto Burgue\u00f1o and Kim Guldstrand Larsen. Model checking via reachability testing for timed automata. In Bernhard Steffen editor TACAS volume 1384 of Lecture Notes in Computer Science pages 263--280. Springer 1998.","DOI":"10.1007\/BFb0054177"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-6400-7_7"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542452.1542475"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SIES.2010.5551372"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.01.036"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_2_1_9_1","volume-title":"The foundations of Esterel","author":"Berry G.","year":"2000","unstructured":"G. Berry . The foundations of Esterel . In C. Stirling G. Plotkin and M. Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press , 2000 . G. Berry. The foundations of Esterel. In C. Stirling G. Plotkin and M. Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000."},{"key":"e_1_2_1_10_1","first-page":"579","volume-title":"FDL","author":"Hedia Belgacem Ben","year":"2005","unstructured":"Belgacem Ben Hedia , Fabrice Jumel , and Jean-Philippe Babau . Formal evaluation of quality of service for data acquisition . In FDL , pages 579 -- 589 . ECSI, 2005 . Belgacem Ben Hedia, Fabrice Jumel, and Jean-Philippe Babau. Formal evaluation of quality of service for data acquisition. In FDL, pages 579--589. ECSI, 2005."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2007.4392797"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/944645.944651"},{"key":"e_1_2_1_13_1","first-page":"309","volume-title":"Sangiovanni-Vincentelli. A methodology for correct-byconstruction latency insensitive design","author":"Carloni Luca P.","year":"1999","unstructured":"Luca P. Carloni , Kenneth L. McMillan , Alexander Saldanha , and Alberto L . Sangiovanni-Vincentelli. A methodology for correct-byconstruction latency insensitive design . In Jacob K. White and Ellen Sentovich, editors, IC-CAD, pages 309 -- 315 . IEEE , 1999 . Luca P. Carloni, Kenneth L. McMillan, Alexander Saldanha, and Alberto L. Sangiovanni-Vincentelli. A methodology for correct-byconstruction latency insensitive design. In Jacob K. White and Ellen Sentovich, editors, IC-CAD, pages 309--315. IEEE, 1999."},{"key":"e_1_2_1_14_1","volume-title":"Synchronous Programming of Reactive Systems","author":"Halbwachs Nicolas","year":"1992","unstructured":"Nicolas Halbwachs . Synchronous Programming of Reactive Systems . Kluwer Academic Publishers , Norwell, MA, USA , 1992 . Nicolas Halbwachs. Synchronous Programming of Reactive Systems. Kluwer Academic Publishers, Norwell, MA, USA, 1992."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/646055.677894"},{"key":"e_1_2_1_16_1","first-page":"1076a","author":"IEEE","year":"2000","unstructured":"IEEE . IEEE Standard VHDL Language Reference Manual. IEEE Standard , 2000 . IEEE Std 1076a - 12000 . IEEE. IEEE Standard VHDL Language Reference Manual. IEEE Standard, 2000. IEEE Std 1076a-2000.","journal-title":"IEEE Standard VHDL Language Reference Manual. IEEE Standard"},{"key":"e_1_2_1_17_1","volume-title":"IEEE Standard, 2004","author":"IEEE.","year":"2004","unstructured":"IEEE. IEEE Standard for VHDL Register Transfer Level (RTL) Synthesis . IEEE Standard, 2004 . IEEE Std 1076.6- 2004 . IEEE. IEEE Standard for VHDL Register Transfer Level (RTL) Synthesis. IEEE Standard, 2004. IEEE Std 1076.6-2004."},{"key":"e_1_2_1_18_1","volume-title":"IEEE Standard, 2005","author":"IEEE.","year":"1850","unstructured":"IEEE. IEEE Standard for Property Specification Language (PSL) . IEEE Standard, 2005 . IEEE Std 1850 -2005. IEEE. IEEE Standard for Property Specification Language (PSL). IEEE Standard, 2005. IEEE Std 1850-2005."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018998524196"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-008-0055-2"},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"CAV","author":"McMillan K.L.","year":"2003","unstructured":"K.L. McMillan . Interpolation and SAT-based model checking . In Warren A. Hunt Jr. and Fabio Somenzi, editors, CAV , volume 2725 of Lecture Notes in Computer Science , pages 1 -- 13 . Springer , July 2003 . K.L. McMillan. Interpolation and SAT-based model checking. In Warren A. Hunt Jr. and Fabio Somenzi, editors, CAV, volume 2725 of Lecture Notes in Computer Science, pages 1--13. Springer, July 2003."},{"key":"e_1_2_1_22_1","volume-title":"May","author":"Systems Modeling OMG.","year":"2008","unstructured":"OMG. Systems Modeling Language (SysML) Specification 1.1. Object Management Group , May 2008 . OMG document number: ptc\/08-05-17. OMG. Systems Modeling Language (SysML) Specification 1.1. Object Management Group, May 2008. OMG document number: ptc\/08-05-17."},{"key":"e_1_2_1_23_1","volume-title":"UML Profile for MARTE, v1.0","author":"OMG.","year":"2009","unstructured":"OMG. UML Profile for MARTE, v1.0 . Object Management Group , Nov. 2009 . OMG document number: formal\/09-11-02. OMG. UML Profile for MARTE, v1.0. Object Management Group, Nov. 2009. OMG document number: formal\/09-11-02."},{"key":"e_1_2_1_24_1","volume-title":"v2.2","author":"Superstructure OMG. UML","year":"2009","unstructured":"OMG. UML Superstructure , v2.2 . Object Management Group , February 2009 . formal\/2009-02-02. OMG. UML Superstructure, v2.2. Object Management Group, February 2009. formal\/2009-02-02."},{"key":"e_1_2_1_25_1","series-title":"Lecture Notes in Computer Science","first-page":"108","volume-title":"FMCAD","author":"Sheeran M.","year":"2000","unstructured":"M. Sheeran , S. Singh , and G. St\u00e5lmarck . Checking safety properties using induction and a satsolver . In W. A. Hunt Jr. and S. D. Johnson, editors, FMCAD , volume 1954 of Lecture Notes in Computer Science , pages 108 -- 125 . Springer , November 2000 . M. Sheeran, S. Singh, and G. St\u00e5lmarck. Checking safety properties using induction and a satsolver. In W. A. Hunt Jr. and S. D. Johnson, editors, FMCAD, volume 1954 of Lecture Notes in Computer Science, pages 108--125. Springer, November 2000."},{"key":"e_1_2_1_26_1","volume-title":"Analysis, Design","author":"Weilkiens Tim","year":"2008","unstructured":"Tim Weilkiens . Systems Engineering with SysM-L\/UML: Modeling , Analysis, Design . The MK\/OMG Press , Burlington, MA, USA ., 2008 . Tim Weilkiens. Systems Engineering with SysM-L\/UML: Modeling, Analysis, Design. The MK\/OMG Press, Burlington, MA, USA., 2008."}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1921532.1921554","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1921532.1921554","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.1921554"}},"subtitle":["specification vs. implementation"],"short-title":[],"issued":{"date-parts":[[2011,1,24]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1,24]]}},"alternative-id":["10.1145\/1921532.1921554"],"URL":"https:\/\/doi.org\/10.1145\/1921532.1921554","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"}}]}}