{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T03:34:29Z","timestamp":1770348869502,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288906","type":"print"},{"value":"9783642288913","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_13","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T12:53:01Z","timestamp":1333111981000},"page":"126-140","source":"Crossref","is-referenced-by-count":91,"title":["Compositional Verification of Architectural Models"],"prefix":"10.1007","author":[{"given":"Darren","family":"Cofer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brian","family":"LaValley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lui","family":"Sha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Cofer, D.D., Miller, S.P., Gacek, A.J., Whalen, M.W., LaValley, B., Sha, L., Al-Nayeem, A.: Complexity-Reducing Design Patterns for Cyber-Physical Systems. Air Force Research Laboratory Technical Report AFRL-RZ-WP-TR-2011-2098 (2011)"},{"key":"13_CR2","unstructured":"Kamp, J.A.W.: Tense Logic and the Theory of Order. Ph.D. Thesis, UCLA (1968)"},{"key":"13_CR3","unstructured":"The NuSMV Toolset Users Manual (2005), \n                  \n                    http:\/\/nusmv.irst.itc.it\/"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Circular Compositional Reasoning about Liveness. Technical Report 1999-02, Cadence Berkeley Labs, Berkeley CA (1999)","DOI":"10.1007\/3-540-48153-2_30"},{"key":"13_CR5","unstructured":"IEEE Standard for Property Specification Language (PSL). IEEE Std 1850-2005 (2005)"},{"key":"13_CR6","unstructured":"Whalen, M., Gacek, A., Cofer, D.: Circular Hierarchical\u00a0Reasoning using Past Time LTL. Technical Report 2011-1, University of Minnesota Software Engineering Center (2011), \n                  \n                    http:\/\/www.umsec.umn.edu\/publications"},{"key":"13_CR7","unstructured":"The Mathworks Inc. Simulink Product Web Site, \n                  \n                    http:\/\/www.mathworks.com\/products\/simulink"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Nam, M.-Y., Pellizzoni, R., Sha, L., Bradford, R.M.: ASIIST: Application Specific I\/O Integration Support Tool for Real-Time Bus Architecture Designs. In: 2009 14th IEEE International Conference on Engineering of Complex Computer Systems (June 2009)","DOI":"10.1109\/ICECCS.2009.31"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic Symbolic Model Checking with PRISM: A Hybrid Approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 52\u201366. Springer, Heidelberg (2002)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Gilles, O., Hugues, J.: Expressing and Enforcing User-Defined Constraints of AADL Models. In: Engineering of Complex Computer Systems (ICECCS), pp. 337\u2013342 (2010)","DOI":"10.1109\/ICECCS.2010.26"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-13464-7_5","volume-title":"Formal Techniques for Distributed Systems","author":"P.C. \u00d6lveczky","year":"2010","unstructured":"\u00d6lveczky, P.C., Boronat, A., Meseguer, J.: Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude. In: Hatcliff, J., Zucca, E. (eds.) FMOODS\/FORTE 2010. LNCS, vol.\u00a06117, pp. 47\u201362. Springer, Heidelberg (2010)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Jahier, E., Halbwachs, N., Raymond, P., Nicollin, X., Lesens, D.: Virtual Integration of AADL models by a translation into synchronous programs. In: EMSOFT 2007. ACM (2007)","DOI":"10.1145\/1289927.1289951"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:14:14Z","timestamp":1620126854000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}