{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:46:53Z","timestamp":1760586413636,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540457725"},{"type":"electronic","value":"9783540457732"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11880240_49","type":"book-chapter","created":{"date-parts":[[2006,11,22]],"date-time":"2006-11-22T09:14:47Z","timestamp":1164186887000},"page":"707-721","source":"Crossref","is-referenced-by-count":17,"title":["A Visualization Framework for the Modeling and Formal Analysis of High Assurance Systems"],"prefix":"10.1007","author":[{"given":"Heather","family":"Goldsby","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Betty H. C.","family":"Cheng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sascha","family":"Konrad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephane","family":"Kamdoum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"49_CR1","volume-title":"Real-Time Design Patterns","author":"B.P. Douglass","year":"2003","unstructured":"Douglass, B.P.: Real-Time Design Patterns. Addison-Wesley, Reading (2003)"},{"key":"49_CR2","unstructured":"Object Management Group, http:\/\/www.omg.org"},{"key":"49_CR3","doi-asserted-by":"crossref","unstructured":"McUmber, W.E., Cheng, B.H.C.: A general framework for formalizing UML with formal languages. In: Proc. of the IEEE Int. Conf. on Software Engineering (ICSE 2001), Toronto, Canada (2001)","DOI":"10.1109\/ICSE.2001.919116"},{"key":"49_CR4","doi-asserted-by":"crossref","unstructured":"Lilius, J., Paltor, I.P.: vUML: A tool for verifying UML models. In: Proc. of the 14th IEEE Int. Conf. on Automated Software Engineering, Washington (1999)","DOI":"10.1109\/ASE.1999.802301"},{"key":"49_CR5","unstructured":"Tanuan, M.C.: Automated Analysis of Unifed Modeling Language (UML) Specifications. Master\u2019s thesis, University of Waterloo, Canada (2001)"},{"key":"49_CR6","doi-asserted-by":"crossref","unstructured":"Inverardi, P., Muccini, H., Pelliccione, P.: CHARMY: An Extensible Tool for Architectural Analysis. In: ESEC\/FSE-13: Proc. of the 10th European Software Engineering Conf. held jointly with 13th ACM SIGSOFT Int. Symposium on Foundations of Software Engineering (2005)","DOI":"10.1145\/1081706.1081726"},{"key":"49_CR7","unstructured":"Holzmann, G.: The Spin Model Checker (2003)"},{"key":"49_CR8","unstructured":"McMillan, K.L.: Getting started with SMV (1999)"},{"key":"49_CR9","unstructured":"IBM: Rational Rose XDE Developer (2005), http:\/\/www-306.ibm.com\/software\/awdtools\/developer\/rosexde\/"},{"key":"49_CR10","unstructured":"Telelogic: ObjectGEODE (2005), http:\/\/www.telelogic.com\/"},{"key":"49_CR11","unstructured":"I-logix (2005), http:\/\/www.ilogix.com\/"},{"key":"49_CR12","unstructured":"ARTiSAN Software: Real-time Studio (2005), http:\/\/www.artisansw.com"},{"key":"49_CR13","unstructured":"Ho, W.M., J\u00e9z\u00e9quel, J.M., Guennec, A.L., Pennaneac, F.: UMLAUT: an extendible UML transformation framework. In: Proc. of the Automated Software Engineering Conf., Florida (1999)"},{"key":"49_CR14","first-page":"742","volume-title":"Proc. of the 22nd Int. Conf. on Software Engineering","author":"U. Nickel","year":"2000","unstructured":"Nickel, U., Niere, J., Z\u00fcndorf, A.: The FUJABA environment. In: Proc. of the 22nd Int. Conf. on Software Engineering, pp. 742\u2013745. ACM Press, New York (2000)"},{"issue":"12","key":"49_CR15","doi-asserted-by":"publisher","first-page":"970","DOI":"10.1109\/TSE.2004.102","volume":"30","author":"S. Konrad","year":"2004","unstructured":"Konrad, S., Cheng, B.H.C., Campbell, L.A.: Object Analysis Patterns for Embedded Systems. IEEE Trans. on Software Engineering\u00a030(12), 970\u2013992 (2004)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"49_CR16","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.H.C.: Facilitating the construction of specification pattern-based properties. In: Proc. of the IEEE Int. Requirements Engineering Conf (RE 2005), Paris, France (2005)","DOI":"10.1109\/RE.2005.29"},{"key":"49_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11663430_6","volume-title":"Satellite Events at the MoDELS 2005 Conference","author":"S. Konrad","year":"2006","unstructured":"Konrad, S., Cheng, B.H.C.: Automated analysis of natural language properties for UML models. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol.\u00a03844, pp. 48\u201357. Springer, Heidelberg (2006)"},{"key":"49_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, New York (1992)"},{"key":"49_CR19","unstructured":"Tigris.org: ArgoUML: The project home (2005), http:\/\/argouml.tigris.org"},{"key":"49_CR20","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E. Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1994)"},{"key":"49_CR21","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Proc. of the Int. Conf. on Software Engineering (ICSE 2005), St Louis, MO, USA (2005)","DOI":"10.1145\/1062455.1062526"},{"key":"49_CR22","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1145\/302405.302672","volume-title":"Proc. of the 21st Int. Conf. on Software Engineering","author":"M.B. Dwyer","year":"1999","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proc. of the 21st Int. Conf. on Software Engineering, pp. 411\u2013420. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"49_CR23","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. PhD thesis, Carnegie Mellon University (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"49_CR24","unstructured":"Kamdoum, S.: Facilitating the roundtrip engineering of model-driven software architecture. Master\u2019s thesis, Michigan State University (2006)"},{"key":"49_CR25","first-page":"40","volume":"70","author":"P. Pettersson","year":"2000","unstructured":"Pettersson, P., Larsen, K.G.: Uppaal2k. Bulletin of the European Association for Theoretical Computer Science\u00a070, 40\u201344 (2000)","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"49_CR26","doi-asserted-by":"crossref","unstructured":"Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.J.: Implementing statecharts in promela\/spin. In: WIFT 1998: Proc. of the Second IEEE Workshop on Industrial Strength Formal Specification Techniques, p. 90 (1998)","DOI":"10.1109\/WIFT.1998.766303"},{"key":"49_CR27","doi-asserted-by":"crossref","unstructured":"Crane, M.L., Dingel, J.: UML vs. classical vs. Rhapsody statecharts: Not all models are created equal. In: Proc. of the ACM\/IEEE 8th Int. Conf. on Model Driven Engineering Languages and Systems (2005)","DOI":"10.1007\/11557432_8"},{"key":"49_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-45739-9_23","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"A. Knapp","year":"2002","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model checking timed UML state machines and collaborations. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 395\u2013414. Springer, Heidelberg (2002)"},{"key":"49_CR29","doi-asserted-by":"crossref","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Proc. of the 10th Conference on Computer-Aided Verification (1998)","DOI":"10.1007\/BFb0028779"}],"container-title":["Lecture Notes in Computer Science","Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11880240_49.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T01:27:39Z","timestamp":1736645259000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11880240_49"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540457725","9783540457732"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/11880240_49","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}