{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:08:19Z","timestamp":1760044099549,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418634"},{"type":"electronic","value":"9783540453147"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45314-8_23","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T17:01:23Z","timestamp":1194973283000},"page":"318-332","source":"Crossref","is-referenced-by-count":20,"title":["A Formal Object-Oriented Analysis for Software Reliability: Design for Verification"],"prefix":"10.1007","author":[{"given":"Natasha","family":"Sharygina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James C.","family":"Browne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert P.","family":"Kurshan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"23_CR1","unstructured":"Booch, G., Object-Oriented Analysis and Design with Applications, Benjamin\/Cummings, Redwood City, CA (1994)"},{"key":"23_CR2","unstructured":"Bounimova, E., Levin, V., Basbugoglu, O., and Inan, K., AVerification Engine for SDL Spec. Of Comm. Protocols, In Proc. of the 1st Symp. on Computer Networks, Istanbul, Turkey, (1996) 16\u201325"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Bosnacki, D., Damm, D., Holenderski, L.,and Sidorova, N., Model checking SDL with Spin, In Proc. of TACAS2000, Berlin, Germany, (2000) 363\u2013377","DOI":"10.1007\/3-540-46419-0_25"},{"key":"23_CR4","series-title":"Lect Notes Comput Sci","first-page":"52","volume-title":"Workshop on Logic of Programs,Yorktown Heights,NY","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., and Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic,Workshop on Logic of Programs,Yorktown Heights,NY. LNCS, Vol. 131, (1981) 52\u201371"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Bandera: Extracting finite-state models for Java source code, In Proc. of 22nd ICSE (2000)","DOI":"10.1145\/337180.337234"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Chan, W., Anderson, R., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J., Model Checking Large Software Specifications, In Proc. of IEEE Transaction on Software Engineering (1998) 498\u2013519","DOI":"10.1109\/32.708566"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Gnesi, S., Lenzini, G., Abbaneo, C., Latella, D., Amendola, A., Marmo, P.,AnAutomatic SPIN Validation of a Safety Critical Railway Control System, In Proc. of Int. Conf. on Dependable Systems and Networks, (2000) 119\u2013124","DOI":"10.1109\/ICDSN.2000.857524"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Gunter, E., and Peled D., Path Exploration Tool, In Proc. of TACAS 1999, Amsterdam, The Netherlands (1999) 405\u2013419","DOI":"10.1007\/3-540-49059-0_28"},{"key":"23_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"In Proc., CAV\u201996","author":"R. Hardin","year":"1996","unstructured":"Hardin R., Har\u2019El, Z., and Kurshan, R.P., COSPAN, In Proc., CAV\u201996, LNCS, Vol. 1102, (1996) 423\u2013427"},{"key":"23_CR10","unstructured":"Havelund, K., and Pressburger, T., Model Checking Java Programs Using Java PathFinder, In Proc. 4\u2019th SPIN workshop (1998)"},{"issue":"2","key":"23_CR11","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1002\/bltj.2223","volume":"5","author":"G. Holzmann","year":"2000","unstructured":"Holzmann, G., and Smith, M., Feaver: Automating software feature verification, Bell Labs Technical Journal, Vol. 5, 2, (2000) 72\u201387","journal-title":"Bell Labs Technical Journal"},{"issue":"23","key":"23_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"5","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G., The Model Checker SPIN, IEEE Trans. on Software Engineering, Vol. 5(23), (1997) 279\u2013295","journal-title":"IEEE Trans. on Software Engineering"},{"key":"23_CR13","unstructured":"Kapoor, C., and Tesar, D.: A Reusable Operational Software Architecture for Advanced Robotics (OSCAR), The University of Texas at Austin, Report to DOE, Grant No. DE-FG01 94EW37966 and NASA Grant No. NAG 9\u2013809 (1998)"},{"key":"23_CR14","volume-title":"Computer-Aided Verification of Coordinating Processes-The Automata-Theoretic Approach","author":"R. Kurshan","year":"1994","unstructured":"Kurshan, R., Computer-Aided Verification of Coordinating Processes-The Automata-Theoretic Approach, Princeton University Press, Princeton, NJ (1994)"},{"key":"23_CR15","unstructured":"Lano, K., Formal Object-Oriented Development, Springer (1997)"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Lind-Nielsen, J, Andersen H., R., etc., Verification of large State\/Event Systems using Compositionality and Depenedency Analysis, In Proc. of TACAS\u201998, Portugal (1998) 201\u2013216","DOI":"10.1007\/BFb0054173"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Liskov, B., Data Abstraction and Hierarchy, In Proc. of OOPSLA conference (1987)","DOI":"10.1145\/62138.62141"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"McMillan, K. Symbolic Model Checking, Kluwer (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"Moors, T., Protocol Organs: Modularity should reflect function, not timing, In Proc. OPENARCH98, (1998) 91\u2013100","DOI":"10.1109\/OPNARC.1998.662046"},{"key":"23_CR20","unstructured":"Object Management Group (OMG), Action Semantic for the UML, OMG (2000)"},{"key":"23_CR21","unstructured":"Rumbaugh, J., Jacobson, I. and Booch, G., The Unified Modeling Language Reference Manual, Object Technology Series, Addison-Wesley (1999)"},{"key":"23_CR22","unstructured":"Sharygina, N., and Browne, J., Automated Rob. Decision Support Software Reverse Engineering, Tech. Rep., The Univ. of Texas at Austin, Robotics Research Croup (1999)"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Sharygina, N., and Peled, D., A Combined Testing and Verification Approach for Software Reliability, In Proc. of FME2001 (to appear), Berlin (2001)","DOI":"10.1007\/3-540-45251-6_35"},{"key":"23_CR24","unstructured":"SES Inc., CodeGenesis User Reference Manual, SES Inc. (1998)"},{"key":"23_CR25","unstructured":"SES inc., ObjectBench Technical Reference, SES Inc. (1998)"},{"key":"23_CR26","volume-title":"Object Lifecycles: Modeling theWorld in States","author":"S. Shlaer","year":"1992","unstructured":"Shlaer, S., and Mellor, S., Object Lifecycles: Modeling theWorld in States, Prentice-Hall, NJ (1992)"},{"key":"23_CR27","unstructured":"Xie, F., Levin, V., Browne, J., Integrating model checking into object-oriented software development process, Techn.Rep., University of Texas at Austin, Comp. Science Dept. (2000)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45314-8_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T07:54:01Z","timestamp":1737532441000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45314-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418634","9783540453147"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-45314-8_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}