{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:27Z","timestamp":1760202627944},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540222613"},{"type":"electronic","value":"9783540277552"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27755-2_22","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T23:48:13Z","timestamp":1284421693000},"page":"789-818","source":"Crossref","is-referenced-by-count":2,"title":["Communicating Transaction Processes: An MSC-Based Model of Computation for Reactive Embedded Systems"],"prefix":"10.1007","author":[{"given":"Abhik","family":"Roychoudhury","sequence":"first","affiliation":[]},{"given":"Pazhamaneri Subramaniam","family":"Thiagarajan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1007\/3-540-48224-5_65","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Realizability and verification of MSC graphs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, p. 797. Springer, Heidelberg (2001)"},{"key":"22_CR2","unstructured":"ARM Limited. AMBA On-chip Bus Specification (1999)"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Balarin, F., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A., Watanabe, Y., Yang, G.: Concurrent execution semantics and sequential simulation algorithms for the Metropolis Meta-Model. In: International symposium on Hardware\/software codesign (CODES) (2002)","DOI":"10.1145\/774790.774793"},{"key":"22_CR4","unstructured":"Cadence Berkeley Laboratories, California, USA. The SMV Model Checker (1999), www-cad.eecs.berkeley.edu\/~kenmcmil\/smv\/"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/3-540-45510-8_5","volume-title":"Modeling and Verification of Parallel Processes","author":"B. Caillaud","year":"2001","unstructured":"Caillaud, B., Darondeau, P., Helouet, L., Lesventes, G.: Hmscs as partial specifications.. with pns as completions. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol.\u00a02067, p. 125. Springer, Heidelberg (2001)"},{"key":"22_CR6","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Pele, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"22_CR7","unstructured":"Codesign, Simulation and Synthesis (COSY) project. Generic Interface Modules for PI-Bus (2001)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design\u00a019(1) (2001)","DOI":"10.1023\/A:1011227529550"},{"key":"22_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526558","volume-title":"Free Choice Petri Nets","author":"J. Desel","year":"1995","unstructured":"Desel, J., Esparza, J.: Free Choice Petri Nets. Cambridge University Press, Cambridge (1995)"},{"key":"22_CR10","volume-title":"Doing Hard Time: Developing Real-time Systems using UML, Objects, Frameworks and Patterns","author":"B.P. Douglass","year":"1999","unstructured":"Douglass, B.P.: Doing Hard Time: Developing Real-time Systems using UML, Objects, Frameworks and Patterns. Addison-Wesley, Reading (1999)"},{"key":"22_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-4515-6","volume-title":"SpecC: Specification Language and Methodology","author":"D.D. Gajski","year":"2000","unstructured":"Gajski, D.D., Zhu, J., Dmer, R., Gerstlauer, A., Zhao, S.: SpecC: Specification Language and Methodology. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"22_CR12","volume-title":"System Design with SystemC","author":"T. Grotker","year":"2002","unstructured":"Grotker, T., Liao, S., Martin, G., Swan, S.: System Design with SystemC. Kluwer Academic Publishers, Dordrecht (2002)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-46428-X_3","volume-title":"Fundamental Approaches to Software Engineering","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kugler, H.: From play-in scenarios to code: An achievable dream. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, p. 22. Springer, Heidelberg (2000)"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Harel, D., Kugler, H.: Synthesizing state-based object systems from LSC specifications. International Journal on Foundations of Computer Science\u00a013(1) (2002)","DOI":"10.1142\/S0129054102000935"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_23","volume-title":"Formal Methods in Computer-Aided Design","author":"D. Harel","year":"2002","unstructured":"Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behavioral requirements. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517. Springer, Heidelberg (2002)"},{"key":"22_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19029-2","volume-title":"Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine","author":"D. Harel","year":"2003","unstructured":"Harel, D., Marelly, R.: Come, Let\u2019s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Hendriksen, J.G., Mukund, M., Kumar, K.N., Thiagarajan, P.S.: Message sequence graphs and finitely generated regular MSC languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, p. 675. Springer, Heidelberg (2000)","DOI":"10.1007\/3-540-45022-X_57"},{"issue":"5","key":"22_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60794-3","volume-title":"Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use","author":"K. Jensen","year":"1997","unstructured":"Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use. Springer, Heidelberg (1997)"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Krueger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to statecharts. In: International Workshop on Distributed and Parallel Embedded Systesms (DIPES) (1998)","DOI":"10.1007\/978-0-387-35570-2_5"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains. Theoretical Computer Science (TCS)\u00a013 (1981)","DOI":"10.1016\/0304-3975(81)90112-2"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Roychoudhury, A., Thiagarajan, P.S.: Communicating transaction processes. In: IEEE International Conference on Applications of Concurrency in System Design (ACSD) (2003)","DOI":"10.1109\/CSD.2003.1207710"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-540-40007-3_15","volume-title":"Formal Methods at the Crossroads. From Panacea to Foundational Support","author":"A. Roychoudhury","year":"2003","unstructured":"Roychoudhury, A., Thiagarajan, P.S.: An executable specification language based on message sequence charts. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol.\u00a02757, pp. 226\u2013241. Springer, Heidelberg (2003)"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Sgroi, M., Lavagno, L.: Synthesis of embedded software using free-choice Petri nets. In: ACM Design Automation Conference (DAC) (1999)","DOI":"10.1145\/309847.310073"},{"key":"22_CR25","unstructured":"Thiagarajan, P.S., et al.: Communicating Transaction Processes (CTP) project (2003), http:\/\/www.comp.nus.edu.sg\/~ctp"},{"key":"22_CR26","unstructured":"Z. 120. Message Sequence Charts (MSC 1996) (1996)"}],"container-title":["Lecture Notes in Computer Science","Lectures on Concurrency and Petri Nets"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27755-2_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:19:16Z","timestamp":1605741556000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27755-2_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540222613","9783540277552"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27755-2_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}