{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:50:37Z","timestamp":1750308637078,"version":"3.41.0"},"reference-count":17,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2012,7,16]],"date-time":"2012-07-16T00:00:00Z","timestamp":1342396800000},"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":[[2012,7,16]]},"abstract":"<jats:p>Behavioral types for model-based development comprise abstract behavioral aspects of the models they are associated with. Behavioral types allow checking that a model fulfills these behavioral aspects. Furthermore, as types can be related with each other, they support more complex checks and guarantees like compatibility in composition and refinement of models in a model based development process.<\/jats:p>\n          <jats:p>We propose a behavioral type system and explain its properties, specically targeting a subset of UML state-machines. We present an early implementation that generates behavioral type definitions out of an Eclipse-based modeling environment. These type definitions are generated for the higher-order proof assistant Coq as files. We present checking and comparison techniques based on these files for behavioral aspects that can be derived from the model definition.<\/jats:p>","DOI":"10.1145\/2237796.2237814","type":"journal-article","created":{"date-parts":[[2012,7,13]],"date-time":"2012-07-13T23:07:36Z","timestamp":1342220856000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Towards a formal foundation of behavioral types for UML state-machines"],"prefix":"10.1145","volume":"37","author":[{"given":"Jan Olaf","family":"Blech","sequence":"first","affiliation":[{"name":"fortiss GmbH, Munich, Germany"}]},{"given":"Bernhard","family":"Sch\u00e4tz","sequence":"additional","affiliation":[{"name":"fortiss GmbH, Munich, Germany"}]}],"member":"320","published-online":{"date-parts":[[2012,7,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.010"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2010.12"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2075679.2075687"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2220336.2220346"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11561163_3"},{"volume-title":"States, Events, and Modes Automotive Software Workshop in San Diego","year":"2006","author":"Braun P.","key":"e_1_2_1_7_1"},{"volume-title":"HOL-OCL - A Formal Proof Environment for UML\/OCL. Fundamental Approaches to Software Engineering. vol 4961 of LNCS","year":"2008","author":"Brucker A. D.","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","series-title":"LNCS","volume-title":"Clocks as first class abstract types. EMSOFT","author":"Colaco J.-L.","year":"2003"},{"key":"e_1_2_1_10_1","unstructured":"The Coq Development Team. The Coq System. http:\/\/coq.inria.fr.  The Coq Development Team. The Coq System. http:\/\/coq.inria.fr."},{"key":"e_1_2_1_11_1","series-title":"LNCS","volume-title":"The linear time - branching time spectrum II","author":"van Glabbeek R.J.","year":"1993"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"volume-title":"Functional safety of electrical\/electronic\/ programmable electronic safety-related systems","year":"1998","author":"International Electrotechnical Commission","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/832262.833357"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-004-0043-8"},{"key":"e_1_2_1_16_1","unstructured":"Papyrus UML. http:\/\/www.papyrusuml.org  Papyrus UML. http:\/\/www.papyrusuml.org"},{"volume-title":"August","year":"2005","key":"e_1_2_1_17_1"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2237796.2237814","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2237796.2237814","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:08:07Z","timestamp":1750273687000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2237796.2237814"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,16]]},"references-count":17,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,7,16]]}},"alternative-id":["10.1145\/2237796.2237814"],"URL":"https:\/\/doi.org\/10.1145\/2237796.2237814","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2012,7,16]]},"assertion":[{"value":"2012-07-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}