{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:21:48Z","timestamp":1725560508786},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540213055"},{"type":"electronic","value":"9783540247210"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24721-0_24","type":"book-chapter","created":{"date-parts":[[2010,7,27]],"date-time":"2010-07-27T20:15:12Z","timestamp":1280261712000},"page":"324-338","source":"Crossref","is-referenced-by-count":9,"title":["Translating Software Designs for Model Checking"],"prefix":"10.1007","author":[{"given":"Fei","family":"Xie","sequence":"first","affiliation":[]},{"given":"Vladimir","family":"Levin","sequence":"additional","affiliation":[]},{"given":"Robert P.","family":"Kurshan","sequence":"additional","affiliation":[]},{"given":"James C.","family":"Browne","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Logic of Programs Workshop (1981)"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: 5th International Symposium on Programming (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL (2002)","DOI":"10.1145\/503272.503274"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Roby: Bandera: a source-level interface for model checking Java programs. In: ICSE (2000)","DOI":"10.1145\/337180.337625"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-48234-2_17","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"K. Havelund","year":"1999","unstructured":"Havelund, K., Skakkeb\u00e6k, J.U.: Applying Model Checking in Java Verification. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, p. 216. Springer, Heidelberg (1999)"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Smith, M.H.: An automated verification method for distributed systems software based on model extraction. IEEE TSE\u00a028 (2002)","DOI":"10.1109\/TSE.2002.995426"},{"key":"24_CR7","unstructured":"Lilius, J., Porres, I.: vUML: a tool for verifying UML models. In: ASE (1999)"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-45923-5_24","volume-title":"Fundamental Approaches to Software Engineering","author":"F. Xie","year":"2002","unstructured":"Xie, F., Levin, V., Browne, J.C.: ObjectCheck: a model checking tool for executable objectoriented software system designs. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, p. 331. Springer, Heidelberg (2002)"},{"key":"24_CR9","volume-title":"Executable UML: A Foundation for Model Driven Architecture","author":"S.J. Mellor","year":"2002","unstructured":"Mellor, S.J., Balcer, M.J.: Executable UML: A Foundation for Model Driven Architecture. Addison-Wesley, Reading (2002)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019El, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-44585-4_36","volume-title":"Computer Aided Verification","author":"V. Levin","year":"2001","unstructured":"Levin, V., Yenig\u00fcn, H.: SDLCheck: A model checking tool. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 378. Springer, Heidelberg (2001)"},{"key":"24_CR12","unstructured":"ITU: ITU-T Recommendation Z.100 (03\/93) - Specification and Description Language (SDL). ITU (1993)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-36578-8_23","volume-title":"Fundamental Approaches to Software Engineering","author":"N. Sharygina","year":"2003","unstructured":"Sharygina, N., Browne, J.C.: Model checking software via abstraction of loop transitions. In: Pezz\u00e9, M. (ed.) FASE 2003. LNCS, vol.\u00a02621, pp. 325\u2013340. Springer, Heidelberg (2003)"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/BFb0054182","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R.P. Kurshan","year":"1998","unstructured":"Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenig\u00fcn, H.: Static partial order reduction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, p. 345. Springer, Heidelberg (1998)"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The model checker SPIN. TSE\u00a023(5) (1997)","DOI":"10.1109\/32.588521"},{"key":"24_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"K. Namjoshi","year":"2000","unstructured":"Namjoshi, K., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"24_CR18","unstructured":"Kurshan, R.P.: FormalCheck User\u2019s Manual (1998)"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. Formal Methods in Software Practice (1998)","DOI":"10.1145\/298595.298598"},{"key":"24_CR20","volume-title":"Concurrency Verification: Introduction to Compositional and Non-compositional Proof Methods","author":"W.P. Rover de","year":"2001","unstructured":"de Rover, W.P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Non-compositional Proof Methods. Cambridge Univ. Press, Cambridge (2001)"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1007\/3-540-45657-0_48","volume-title":"Computer Aided Verification","author":"R.P. Kurshan","year":"2002","unstructured":"Kurshan, R.P., Levin, V., Yenig\u00fcn, H.: Compressing transitions for model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 569. Springer, Heidelberg (2002)"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"1993","unstructured":"Godefroid, P., Pirottin, D.: Refining dependencies improves partial-order verification methods. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697. Springer, Heidelberg (1993)"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: FMSD (1996)","DOI":"10.1007\/BF00121262"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0023729","volume-title":"Computer-Aided Verification","author":"A. Valmari","year":"1991","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531. Springer, Heidelberg (1991)"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"24_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45236-2_32","volume-title":"FME 2003: Formal Methods","author":"F. Xie","year":"2003","unstructured":"Xie, F., Browne, J.C., Kurshan, R.P.: Translation-based compositional reasoning for software systems. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805. Springer, Heidelberg (2003)"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M.D., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, p. 151. Springer, Heidelberg (1998)"},{"key":"24_CR28","unstructured":"Kapoor, C., Tesar, D.: A reusable operational software architecture for advanced robotics (OSCAR). The University of Texas at Austin, Report to U.S. Dept. of Energy, Grant No. DE-FG01 94EW37966 and NASA Grant No. NAG 9-809 (1998)"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Wang, W., Hidvegi, Z., Bailey, A.D., Whinston, A.B.: E-processes design and assurance using model checking. IEEE Computer\u00a033 (2000)","DOI":"10.1109\/2.876292"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. In: ASPLOS-IX (2000)","DOI":"10.1145\/378993.379006"},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"Sharygina, N., Browne, J.C., Kurshan, R.P.: Formal object-oriented analysis for software reliability design for verification. In: FASE (2001)","DOI":"10.1007\/3-540-45314-8_23"},{"key":"24_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/3-540-45923-5_5","volume-title":"Fundamental Approaches to Software Engineering","author":"F. Xie","year":"2002","unstructured":"Xie, F., Browne, J.C.: Integrated state space reduction for model checking executable object-oriented software system designs. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, p. 64. Springer, Heidelberg (2002)"},{"key":"24_CR33","doi-asserted-by":"crossref","unstructured":"Xie, F., Browne, J.C.: Verified systems by composition from verified components. In: ESEC\/FSE (2003)","DOI":"10.1145\/940071.940109"},{"key":"24_CR34","doi-asserted-by":"crossref","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems\u00a014 (1988)","DOI":"10.1016\/0169-7552(87)90085-7"},{"key":"24_CR35","doi-asserted-by":"crossref","unstructured":"Gnesi, S., Latella, D., Massink, M.: Model checking UML statechart diagrams using JACK. In: HASE (1999)","DOI":"10.1109\/HASE.1999.809474"},{"key":"24_CR36","unstructured":"Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.: Implementing statecharts in Promela\/Spin. In: Industrial Strength Formal Specification Technologies (1993)"},{"key":"24_CR37","unstructured":"Garavel, H., Sifakis, J.: Compilation and verification of LOTOS specifications. PSTV (1990)"},{"key":"24_CR38","doi-asserted-by":"crossref","unstructured":"Bozga, M., Graf, S., Mounier, L.: Automated validation of distributed software using the IF environment. In: CAV (2001)","DOI":"10.1109\/NCA.2001.962542"},{"key":"24_CR39","doi-asserted-by":"crossref","unstructured":"Bozga, M., Fernandez, J.C., Ghirvu, L., Graf, S., Krimm, J., Mounier, L., Sifakis, J.: IF: An intermediate representation for SDL and its applications. In: SDL-Forum 1999 (1999)","DOI":"10.1016\/B978-044450228-5\/50028-X"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24721-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T15:31:24Z","timestamp":1559316684000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24721-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213055","9783540247210"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24721-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}