{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:57:52Z","timestamp":1725569872410},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642169007"},{"type":"electronic","value":"9783642169014"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16901-4_25","type":"book-chapter","created":{"date-parts":[[2010,11,8]],"date-time":"2010-11-08T12:40:06Z","timestamp":1289220006000},"page":"371-387","source":"Crossref","is-referenced-by-count":14,"title":["Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP"],"prefix":"10.1007","author":[{"given":"Islam","family":"Abdelhalim","sequence":"first","affiliation":[]},{"given":"James","family":"Sharp","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Helen","family":"Treharne","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"OMG: Semantics of a foundational subset for executable UML models (fUML) - (Beta 2) (November 2009), http:\/\/www.omg.org\/spec\/fuml\/1.0"},{"key":"25_CR2","volume-title":"Concurrent and Real-Time Systems: the CSP Approach","author":"S. Schneider","year":"1999","unstructured":"Schneider, S.: Concurrent and Real-Time Systems: the CSP Approach. Wiley, Chichester (1999)"},{"key":"25_CR3","unstructured":"Formal\u00a0Systems Oxford: FDR 2.83 manual (2007)"},{"key":"25_CR4","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":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-540-85762-4_25","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"E. Turner","year":"2008","unstructured":"Turner, E., Treharne, H., Schneider, S., Evans, N.: Automatic generation of CSP\u2225B skeletons from xUML models. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol.\u00a05160, pp. 364\u2013379. Springer, Heidelberg (2008)"},{"key":"25_CR6","unstructured":"Wilkie, I., King, A., Clarke, M., Weaver, C., Raistrick, C., Francis, P.: UML ASL Reference Guide (ASL language level 2.5). Kennedy Carter Ltd. (2003)"},{"key":"25_CR7","unstructured":"Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the tokeneer enclave protection software. In: 1st IEEE International Symposium on Secure Software Engineering (March 2006)"},{"key":"25_CR8","unstructured":"OMG: Unified modeling language (UML) superstructure (version 2.2) (2009)"},{"issue":"4","key":"25_CR9","first-page":"1","volume":"41","author":"C. Hoare","year":"2009","unstructured":"Hoare, C., Misra, J., Leavens, G.T., Shankar, N.: The verified software initiative: A manifesto. ACM Comput. Surv.\u00a041(4), 1\u20138 (2009)","journal-title":"ACM Comput. Surv."},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/11813040_43","volume-title":"FM 2006: Formal Methods","author":"D. Johnson","year":"2006","unstructured":"Johnson, D.: Cost effective software engineering for security. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 607\u2013611. Springer, Heidelberg (2006)"},{"issue":"4","key":"25_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J. Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Comput. Surv.\u00a041(4), 1\u201336 (2009)","journal-title":"ACM Comput. Surv."},{"key":"25_CR12","unstructured":"Praxis, A.: The Tokeneer Project, http:\/\/www.adacore.com\/tokeneer (cited August 2009)"},{"key":"25_CR13","unstructured":"Barnes, J., Cooper, D.: Tokeneer ID station: Formal Specification. Technical Report S.P1229.41.2, Altran Praxis (August 2008)"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Aydal, E.G.: A token experiment. Festschrifts in Computer Science, the BCS FAC Series, Festschrift for Tony Hoare (2009)","DOI":"10.1007\/978-1-84882-912-1_17"},{"key":"25_CR15","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1109\/ISCSCT.2008.379","volume-title":"ISCSCT 2008: Proceedings of the 2008 International Symposium on Computer Science and Computational Technology","author":"D. Xu","year":"2008","unstructured":"Xu, D., Philbert, N., Liu, Z., Liu, W.: Towards formalizing UML activity diagrams in CSP. In: ISCSCT 2008: Proceedings of the 2008 International Symposium on Computer Science and Computational Technology, Washington, DC, USA, pp. 450\u2013453. IEEE Computer Society, Los Alamitos (2008)"},{"key":"25_CR16","first-page":"1035","volume-title":"ICIS 2009: Proceedings of the 2009 Eigth IEEE\/ACIS International Conference on Computer and Information Science","author":"D. Xu","year":"2009","unstructured":"Xu, D., Miao, H., Philbert, N.: Model checking UML activity diagrams in FDR. In: ICIS 2009: Proceedings of the 2009 Eigth IEEE\/ACIS International Conference on Computer and Information Science, Washington, DC, USA, pp. 1035\u20131040. IEEE Computer Society, Los Alamitos (2009)"},{"key":"25_CR17","unstructured":"Goldsmith, M., Armstrong, P.: Personal communication (February 2010)"},{"key":"25_CR18","unstructured":"Zakiuddin, I., Moffat, N., O\u2019Halloran, C., Ryan, P.: Chasing events to certify a critical system. Technical report, UK DERA (1998)"},{"key":"25_CR19","unstructured":"Cooper, D., Barnes, J.: Tokeneer ID station: System Requirements Specification. Technical Report S.P1229.41.1, Altran Praxis (August 2008)"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-540-30482-1_35","volume-title":"Formal Methods and Software Engineering","author":"N. Amalio","year":"2004","unstructured":"Amalio, N., Stepney, S., Polack, F.: Formal proof from UML models. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 418\u2013433. Springer, Heidelberg (2004)"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/11901433_24","volume-title":"Formal Methods and Software Engineering","author":"X. Zhao","year":"2006","unstructured":"Zhao, X., Long, Q., Qiu, Z.: Model checking dynamic UML consistency. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 440\u2013459. Springer, Heidelberg (2006)"},{"issue":"3","key":"25_CR22","first-page":"259","volume":"4","author":"B.B. Ammar","year":"2008","unstructured":"Ammar, B.B., Bhiri, M.T., Souqui\u00e8res, J.: Incremental development of UML specifications using operation refinements. ISSE\u00a04(3), 259\u2013266 (2008)","journal-title":"ISSE"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-00255-7_4","volume-title":"Integrated Formal Methods","author":"J. Cabot","year":"2009","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verifying UML\/OCL operation contracts. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol.\u00a05423, pp. 40\u201355. Springer, Heidelberg (2009)"},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/11611257_44","volume-title":"SOFSEM 2006: Theory and Practice of Computer Science","author":"C. Pons","year":"2006","unstructured":"Pons, C.: Heuristics on the definition of UML refinement patterns. In: Wiedermann, J., Tel, G., Pokorn\u00fd, J., Bielikov\u00e1, M., \u0160tuller, J. (eds.) SOFSEM 2006. LNCS, vol.\u00a03831, pp. 461\u2013470. Springer, Heidelberg (2006)"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/3-540-36103-0_31","volume-title":"Formal Methods and Software Engineering","author":"M.Y. Ng","year":"2002","unstructured":"Ng, M.Y., Butler, M.J.: Tool support for visualizing CSP in UML. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol.\u00a02495, pp. 287\u2013298. Springer, Heidelberg (2002)"},{"key":"25_CR26","first-page":"138","volume-title":"1st IEEE International Conference on Software Engineering and Formal Methods","author":"M.Y. Ng","year":"2003","unstructured":"Ng, M.Y., Butler, M.: Towards formalizing UML state diagrams in CSP. In: Cerone, A., Lindsay, P. (eds.) 1st IEEE International Conference on Software Engineering and Formal Methods, pp. 138\u2013147. IEEE Computer Society, Los Alamitos (2003)"},{"issue":"3","key":"25_CR27","first-page":"293","volume":"4","author":"Y. Thierry-Mieg","year":"2008","unstructured":"Thierry-Mieg, Y., Hillah, L.M.: UML behavioral consistency checking using instantiable Petri nets. ISSE\u00a04(3), 293\u2013300 (2008)","journal-title":"ISSE"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Hansen, H.H., Ketema, J., Luttik, B., Mousavi, M., van de Pol, J.: Towards model checking Executable UML specifications in mCRL2. ISSE, 83\u201390 (2010)","DOI":"10.1007\/s11334-009-0116-1"},{"key":"25_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2004.09.006","volume":"101","author":"G. Graw","year":"2004","unstructured":"Graw, G., Herrmann, P.: Transformation and verification of Executable UML models. Electron. Notes Theor. Comput. Sci.\u00a0101, 3\u201324 (2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"25_CR30","first-page":"333","volume-title":"ASE 2001: Proceedings of the 16th IEEE International Conference on Automated Software Engineering","author":"F. Xie","year":"2001","unstructured":"Xie, F., Levin, V., Browne, J.C.: Model checking for an executable subset of UML. In: ASE 2001: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, p. 333. IEEE Computer Society, Los Alamitos (2001)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16901-4_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T00:12:25Z","timestamp":1559779945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16901-4_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642169007","9783642169014"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16901-4_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}