{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:29:34Z","timestamp":1743006574477,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642023507"},{"type":"electronic","value":"9783642023514"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02351-4_7","type":"book-chapter","created":{"date-parts":[[2009,6,17]],"date-time":"2009-06-17T07:16:01Z","timestamp":1245222961000},"page":"101-115","source":"Crossref","is-referenced-by-count":3,"title":["Timed Simulation of Extended AADL-Based Architecture Specifications with Timed Abstract State Machines"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Bj\u00f6rnander","sequence":"first","affiliation":[]},{"given":"Lars","family":"Grunske","sequence":"additional","affiliation":[]},{"given":"Kristina","family":"Lundqvist","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1109\/LICS.1990.113766","volume-title":"Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science","author":"R. Alur","year":"1990","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 414\u2013425. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"678","DOI":"10.1016\/j.jss.2006.08.014","volume":"80","author":"L. Grunske","year":"2007","unstructured":"Grunske, L.: Early quality prediction of component-based systems - A generic framework. Journal of Systems and Software\u00a080, 678\u2013686 (2007)","journal-title":"Journal of Systems and Software"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-65193-4_20","volume-title":"Lectures on Embedded Systems","author":"S. Yovine","year":"1998","unstructured":"Yovine, S.: Model checking timed automata. In: Rozenberg, G. (ed.) EEF School 1996. LNCS, vol.\u00a01494, pp. 114\u2013124. Springer, Heidelberg (1998)"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Feiler, P.H., Gluch, D.P., Hudak, J.J.: The Architecture Analysis and Design Language (AADL): An Introduction. Technical Report CMU\/SEI-2006-TN-011, Society of Automotive Engineers (2006)","DOI":"10.21236\/ADA455842"},{"key":"7_CR5","unstructured":"Feiler, P., Lewis, B.: SAE Architecture Analysis and Design Language (AADL) Annex Volume 1. Technical Report AS5506\/1, Society of Automobile Engineers (2006)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-73368-3_15","volume-title":"Computer Aided Verification","author":"M. Ouimet","year":"2007","unstructured":"Ouimet, M., Lundqvist, K.: The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 126\u2013130. Springer, Heidelberg (2007)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/BFb0020967","volume-title":"Hybrid Systems III","author":"N. Lynch","year":"1996","unstructured":"Lynch, N.: Modeling and verification of automated transit systems, using timed automata, invariants, and simulations. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 449\u2013459. Springer, Heidelberg (1996)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-58867-1_47","volume-title":"Formal Development of Reactive Systems","author":"C. Lewerentz","year":"1995","unstructured":"Lewerentz, C., Lindner, T.: Formal development of reactive systems, case study production cell. In: Lewerentz, C., Lindner, T. (eds.) Formal Development of Reactive Systems. LNCS, vol.\u00a0891, pp. 21\u201354. Springer, Heidelberg (1995)"},{"key":"7_CR9","unstructured":"Ouimet, M., Lundqvist, K.: Modeling the Production Cell System in the TASM Language. Technical Report ESL-TIK-00209, Embedded Systems Laboratory, Massachusetts Institute of Technology, Cambridge, MA, 02139, USA (2007)"},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1109\/RTTAS.2000.852458","volume-title":"Proceedings of the Sixth IEEE Real-Time Technology and Applications Symposium (RTAS 2000)","author":"S. Vestal","year":"2000","unstructured":"Vestal, S.: Formal verification of the metaH executive using linear hybrid automata. In: Proceedings of the Sixth IEEE Real-Time Technology and Applications Symposium (RTAS 2000), pp. 134\u2013144. IEEE, Washington (2000)"},{"key":"7_CR11","volume-title":"Learning UML 2.0.","author":"R. Miles","year":"2006","unstructured":"Miles, R., Hamilton, K.: Learning UML 2.0. O\u2019Reilly Media, Sebastopol (2006)"},{"key":"7_CR12","volume-title":"UML 2.0 in a Nutshell","author":"D. Pilone","year":"2005","unstructured":"Pilone, D., Pitman, N.: UML 2.0 in a Nutshell, 2nd edn. O\u2019Reilly Media, Sebastopol (2005)","edition":"2"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Ouimet, M., Lundqvist, K.: The TASM Language and the Hi-Five Framework: Specification, Validation, and Verification of Embedded Real-Time Systems. In: Asia-Pacific Software Engineering Conference (2007)","DOI":"10.1109\/ASPEC.2007.117"},{"key":"7_CR14","unstructured":"Ouimet, M., Lundqvist, K.: The TASM Language Reference Manual, Version 1.1, Massachusetts Institute of Technology, Cambridge, MA, 02139, USA (2006)"},{"key":"7_CR15","first-page":"377","volume-title":"ICECCS","author":"R.B. Fran\u00e7a","year":"2007","unstructured":"Fran\u00e7a, R.B., Bodeveix, J.P., Filali, M., Rolland, J.F., Chemouil, D., Thomas, D.: The AADL behaviour annex - experiments and roadmap. In: ICECCS, pp. 377\u2013382. IEEE Computer Society, Los Alamitos (2007)"},{"key":"7_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines - A Method for High-level System Design and Analysis","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines - A Method for High-level System Design and Analysis. Springer, Heidelberg (2003)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A Tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"7_CR18","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J. Bengtsson","year":"2004","unstructured":"Bengtsson, J., Wang, Y.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol.\u00a03098, pp. 87\u2013124. Springer, Heidelberg (2004)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Winkowski, J.: Processes of Timed Petri Nets. TCS: Theoretical Computer Science\u00a0243 (2000)","DOI":"10.1016\/S0304-3975(98)00188-1"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-540-73210-5_9","volume-title":"Integrated Formal Methods","author":"R. Colvin","year":"2007","unstructured":"Colvin, R., Grunske, L., Winter, K.: Probabilistic timed behavior trees. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 156\u2013175. Springer, Heidelberg (2007)"},{"key":"7_CR22","doi-asserted-by":"publisher","first-page":"2163","DOI":"10.1016\/j.jss.2008.04.035","volume":"81","author":"R. Colvin","year":"2008","unstructured":"Colvin, R., Grunske, L., Winter, K.: Timed behavior trees for failure mode and effects analysis of time-critical systems. Journal of Systems and Software\u00a081, 2163\u20132182 (2008)","journal-title":"Journal of Systems and Software"},{"key":"7_CR23","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1109\/ASWEC.2007.49","volume-title":"Proceedings of the 18th Australian Conference on Software Engineering (ASWEC 2007)","author":"L. Grunske","year":"2007","unstructured":"Grunske, L., Winter, K., Colvin, R.: Timed Behavior Trees and their Application to Verifying Real-time Systems. In: Proceedings of the 18th Australian Conference on Software Engineering (ASWEC 2007), pp. 211\u2013220. IEEE Computer Society, Los Alamitos (2007)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-540-30482-1_39","volume-title":"Formal Methods and Software Engineering","author":"J.S. Dong","year":"2004","unstructured":"Dong, J.S., Hao, P., Qin, S.C., Sun, J., Wang, Y.: Timed patterns: Tcoz to timed automata. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 483\u2013498. Springer, Heidelberg (2004)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III","author":"C. Daws","year":"1996","unstructured":"Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The Tool KRONOS. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol.\u00a01066, pp. 208\u2013219. Springer, Heidelberg (1996)"},{"key":"7_CR26","unstructured":"Ouimet, M., Lundqvist, K.: A Mapping between the Timed Abstract State Machine Language and UPPAAL\u2019s Timed Automata. Technical Report ESL-TIK-00212, Embedded Systems Laboratory, Massachusetts Institute of Technology, Cambridge, MA, 02139, USA (2007)"},{"key":"7_CR27","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1995.1014","volume":"116","author":"S. Schneider","year":"1995","unstructured":"Schneider, S.: An operational semantics for timed CSP. Information and Computation\u00a0116, 193\u2013213 (1995)","journal-title":"Information and Computation"},{"key":"7_CR28","first-page":"488","volume-title":"Int. Conference on Engineering of Complex Computer Systems (ICECCS 2005)","author":"J.S. Dong","year":"2005","unstructured":"Dong, J.S., Duke, R., Hao, P.: Integrating object-z with timed automata. In: Int. Conference on Engineering of Complex Computer Systems (ICECCS 2005), pp. 488\u2013497. IEEE Computer Society, Los Alamitos (2005)"},{"key":"7_CR29","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/s001650200003","volume":"13","author":"G. Smith","year":"2002","unstructured":"Smith, G., Hayes, I.: An introduction to real-time object-z. Formal Aspects of Computing\u00a013, 128\u2013141 (2002)","journal-title":"Formal Aspects of Computing"},{"key":"7_CR30","unstructured":"Feiler, P.H., Gluch, D.P., Hudak, J.J., Lewis, B.A.: Embedded Systems Architecture Analysis Using SAE AADL. Technical report, CMU\/SEI-2004-TN-005 (2004)"},{"key":"7_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1104011.1103847","volume":"25","author":"F. Singhoff","year":"2005","unstructured":"Singhoff, F., Legrand, J., Nana, L., Marc\u00e9, L.: Scheduling and memory requirements analysis with AADL. ACM SIGADA Ada Letters\u00a025, 1\u201310 (2005)","journal-title":"ACM SIGADA Ada Letters"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Feiler, P., Rugina, A.: Dependability modeling with the architecture analysis and design language (AADL). Technical Report CMU\/SEI-2007-TN-043, Carnegie Mellon University (2007)","DOI":"10.21236\/ADA455842"},{"key":"7_CR33","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1109\/HASE.2008.32","volume-title":"11th IEEE High Assurance Systems Engineering Symposium, HASE 2008","author":"L. Grunske","year":"2008","unstructured":"Grunske, L., Han, J.: A Comparative Study into Architecture-Based Safety Evaluation Methodologies Using AADL\u2019s Error Annex and Failure Propagation Models. In: 11th IEEE High Assurance Systems Engineering Symposium, HASE 2008, pp. 283\u2013292. IEEE Computer Society, Los Alamitos (2008)"}],"container-title":["Lecture Notes in Computer Science","Architectures for Adaptive Software Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02351-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T19:30:05Z","timestamp":1558380605000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02351-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642023507","9783642023514"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02351-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}