{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T14:51:49Z","timestamp":1772549509574,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642142949","type":"print"},{"value":"9783642142956","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_48","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"562-565","source":"Crossref","is-referenced-by-count":17,"title":["A Model Checker for AADL"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bozzano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viet Yen","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Roveri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf","family":"Wimmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"48_CR1","unstructured":"The COMPASS project, \n                    \n                      http:\/\/compass.informatik.rwth-aachen.de\/"},{"key":"48_CR2","unstructured":"ADeS, a simulator for AADL, \n                    \n                      http:\/\/www.axlog.fr\/aadl\/ades_en.html"},{"issue":"6","key":"48_CR3","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. on Soft. Eng.\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. on Soft. Eng."},{"key":"48_CR4","unstructured":"Bozzano, M., Cavada, R., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Olive, X.: Formal Verification and Validation of AADL Models. In: Proc. ERTS 2010 (to be published, 2010)"},{"key":"48_CR5","first-page":"121","volume-title":"Proc. MEMOCODE\u201909","author":"M. Bozzano","year":"2009","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: Codesign of Dependable Systems: A Component-Based Modelling Language. In: Proc. MEMOCODE\u201909, pp. 121\u2013130. IEEE, Los Alamitos (2009)"},{"key":"48_CR6","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: Model-based codesign of critical embedded systems. In: Proc. ACES-MB\u201909, pp. 87\u201391 (2009)"},{"key":"48_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-04468-7_15","volume-title":"Computer Safety, Reliability, and Security","author":"M. Bozzano","year":"2009","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol.\u00a05775, pp. 173\u2013186. Springer, Heidelberg (2009)"},{"issue":"1","key":"48_CR8","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10009-006-0001-2","volume":"9","author":"M. Bozzano","year":"2007","unstructured":"Bozzano, M., Villafiorita, A.: The FSAP\/NuSMV-SA Safety Analysis Platform. Int. J. on Software Tools for Technology Transfer\u00a09(1), 5\u201324 (2007)","journal-title":"Int. J. on Software Tools for Technology Transfer"},{"key":"48_CR9","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability, and performance analysis of extended AADL models. The Computer Journal (March 2010) doi: 10.1093\/com"},{"key":"48_CR10","unstructured":"Cheddar: a free real time scheduling tool, \n                    \n                      https:\/\/wiki.sei.cmu.edu\/aadl\/index.php\/Cheddar"},{"key":"48_CR11","first-page":"39","volume-title":"Proc. ACES-MB\u201908","author":"M.Y. Chkouri","year":"2008","unstructured":"Chkouri, M.Y., Robert, A., Bozga, M., Sifakis, J.: Translating AADL into BIP \u2013 application to the verification of real-time systems. In: Proc. ACES-MB\u201908, pp. 39\u201353. Springer, Heidelberg (2008)"},{"key":"48_CR12","first-page":"411","volume-title":"Proc. ICSE\u201999","author":"M. Dwyer","year":"1999","unstructured":"Dwyer, M., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proc. ICSE\u201999, pp. 411\u2013420. IEEE, Los Alamitos (1999)"},{"key":"48_CR13","unstructured":"The FurnessTM Toolset, \n                    \n                      http:\/\/www.furnesstoolset.com\/"},{"key":"48_CR14","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/1368088.1368094","volume-title":"ICSE","author":"L. Grunske","year":"2008","unstructured":"Grunske, L.: Specification patterns for probabilistic quality properties. In: Sch\u00e4fer, W., Dwyer, M.B., Gruhn, V. (eds.) ICSE, pp. 31\u201340. ACM, New York (2008)"},{"key":"48_CR15","unstructured":"MRMC \u2013 Markov Reward Model Checker, \n                    \n                      http:\/\/www.mrmc-tool.org\/"},{"key":"48_CR16","unstructured":"The NuSMV Model Checker, \n                    \n                      http:\/\/nusmv.fbk.eu"},{"key":"48_CR17","unstructured":"RAT \u2013 Requirements Analysis Tool, \n                    \n                      http:\/\/rat.fbk.eu"},{"key":"48_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/11901914_35","volume-title":"Automated Technology for Verification and Analysis","author":"R. Wimmer","year":"2006","unstructured":"Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref \u2013 A Symbolic Bisimulation Tool Box. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 477\u2013492. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_48","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:50:32Z","timestamp":1558295432000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}