{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T18:26:05Z","timestamp":1761675965013},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T00:00:00Z","timestamp":1340841600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1007\/s10009-012-0243-0","type":"journal-article","created":{"date-parts":[[2012,7,8]],"date-time":"2012-07-08T21:34:26Z","timestamp":1341783266000},"page":"375-396","source":"Crossref","is-referenced-by-count":13,"title":["An integrated framework for checking the behaviour of fUML models using CSP"],"prefix":"10.1007","volume":"15","author":[{"given":"Islam","family":"Abdelhalim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Schneider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helen","family":"Treharne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,28]]},"reference":[{"key":"243_CR1","doi-asserted-by":"crossref","unstructured":"Abdelhalim, I., Sharp, J., Schneider, S.A., Treharne, H.: Formal verification of tokeneer behaviours modelled in fUML using CSP. In: Dong, J.S., Zhu, H., (eds.) Formal Methods and Software Engineering. 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17\u201319, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6447, pp. 371\u2013387. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16901-4_25"},{"key":"243_CR2","unstructured":"Altran Praxis: The Tokeneer Project. http:\/\/www.adacore.com\/tokeneer (cited August 2009)"},{"key":"243_CR3","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 (2006)"},{"key":"243_CR4","unstructured":"Barnes, J., Cooper, D.: Tokeneer ID station: formal specification. Tech. Rep. S.P1229.41.2, Altran Praxis (2008)"},{"key":"243_CR5","unstructured":"Bisztray, D., Ehrig, K., Heckel, R.: Case study: UML to CSP transformation. In: Applications of Graph Transformation with Industrial Relevance (2007)"},{"key":"243_CR6","doi-asserted-by":"crossref","unstructured":"Cabot, J., Claris\u00f3, R., Riera, D.: Verifying UML\/OCL operation contracts. In: IFM \u201909: Proceedings of the 7th International Conference on Integrated Formal Methods, pp. 40\u201355. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-00255-7_4"},{"key":"243_CR7","unstructured":"Cooper, D., Barnes, J.: Tokeneer ID station: system requirements specification. Tech. Rep. S.P1229.41.1, Altran Praxis (2008)"},{"issue":"4","key":"243_CR8","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/235321.235322","volume":"5","author":"H. David","year":"1996","unstructured":"David H., Amnon N.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293\u2013333 (1996). doi: 10.1145\/235321.235322","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"243_CR9","doi-asserted-by":"crossref","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. 101, 3\u201324 (2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"243_CR10","unstructured":"Groote, J.F., Mathijssen, A., Reniers, M., Usenko, Y., van Weerdenburg, M.: The formal specification language mCRL2. In: Brinksma, E., Harel, D., Mader, A., Stevens, P., Wieringa, R. (eds.) Methods for Modelling Software Systems (MMOSS), no. 06351 in Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany, Dagstuhl, Germany (2007)"},{"issue":"3","key":"243_CR11","first-page":"63","volume":"24","author":"M. Gruninger","year":"2003","unstructured":"Gruninger M., Menzel C.: Process specification language: principles and applications.. AI Mag. 24(3), 63\u201374 (2003)","journal-title":"AI Mag."},{"key":"243_CR12","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, pp. 83\u201390 (2010)","DOI":"10.1007\/s11334-009-0116-1"},{"key":"243_CR13","doi-asserted-by":"crossref","unstructured":"Hardin, R.H., Har\u2019El, Z., Kurshan, R.P.: COSPAN 1102 (1996)","DOI":"10.1007\/3-540-61474-5_94"},{"key":"243_CR14","unstructured":"Hoare, C.: Communicating Sequential Processes. Prentice Hall International Series in Computing Science, Englewood (1985)"},{"issue":"4","key":"243_CR15","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. 41(4), 1\u20138 (2009)","journal-title":"ACM Comput. Surv."},{"key":"243_CR16","doi-asserted-by":"crossref","unstructured":"Johnson, D.: Cost effective software engineering for security. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods, Lecture Notes in Computer Science, vol. 4085, pp. 607\u2013611. Springer, Berlin (2006)","DOI":"10.1007\/11813040_43"},{"key":"243_CR17","unstructured":"Kolovos, D., Rose, L., Paige, R.: The Epsilon Book. http:\/\/www.eclipse.org\/gmt\/epsilon\/doc\/book\/ (last viewed 4th of October 2011)"},{"key":"243_CR18","unstructured":"Mellor, S.J., Balcer, M.J.: Executable UML, A Foundation for Model-Driven Architecture. Addison-Wesley, Reading (2002)"},{"key":"243_CR19","unstructured":"ModelDriven.Org: fUML Reference Implementation. http:\/\/portal.modeldriven.org (last viewed 4th of October 2011)"},{"key":"243_CR20","unstructured":"Mrugalla, C., Robbe, O., Schinz, I., Toben, T., Westphal, B.: Formal verification of a sensor voting and monitoring UML model. In: Houmb, S.H., J\u00fcrjens, J., France, R. (eds.) Proceedings of the 4th International Workshop on Critical Systems Development Using Modeling Languages (CSDUML 2005). Technische Universit\u00e4t M\u00fcnchen, Fredrikstad, Norway (2005)"},{"issue":"4","key":"243_CR21","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T. Murata","year":"1989","unstructured":"Murata T.: Petri nets: Properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"key":"243_CR22","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, Washington, DC (2003)"},{"key":"243_CR23","unstructured":"OMG: XML Metadata Interchange (XMI) (Version 2.1.1)"},{"key":"243_CR24","unstructured":"OMG: Unified modeling language (UML) superstructure (version 2.3) (2010)"},{"key":"243_CR25","unstructured":"OMG: Semantics of a foundational subset for executable UML models (fUML)-Version 1.0 (2011)"},{"key":"243_CR26","doi-asserted-by":"crossref","unstructured":"Planas, E., Cabot, J., G\u00f3mez, C.: Verifying action semantics specifications in UML behavioral models. In: CAiSE \u201909: Proceedings of the 21st International Conference on Advanced Information Systems Engineering, pp. 125\u2013140. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02144-2_14"},{"key":"243_CR27","unstructured":"Quick Sequence Diagram Editor-v3.1. http:\/\/sdedit.sourceforge.net\/ (last viewed 4th of October 2011)"},{"key":"243_CR28","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Wu, Z.: Verifying statemate statecharts using CSP and FDR. In: ICFEM, pp. 324\u2013341 (2006)","DOI":"10.1007\/11901433_18"},{"issue":"4","key":"243_CR29","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/s00165-005-0076-7","volume":"17","author":"S. Schneider","year":"2005","unstructured":"Schneider S., Treharne H.: CSP theorems for communicating B machines. Formal Asp. Comput. 17(4), 390\u2013422 (2005)","journal-title":"Formal Asp. Comput."},{"key":"243_CR30","doi-asserted-by":"crossref","unstructured":"Shah, S.M.A., Anastasakis, K., Bordbar, B.: From UML to alloy and back again. In: MoDeVVa \u201909: Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation, pp. 1\u201310. ACM, New York (2009)","DOI":"10.1145\/1656485.1656489"},{"issue":"3","key":"243_CR31","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 4(3), 293\u2013300 (2008)","journal-title":"ISSE"},{"key":"243_CR32","doi-asserted-by":"crossref","unstructured":"Treharne, H., Turner, E., Paige, R.F., Kolovos, D.S.: Automatic generation of integrated formal models corresponding to UML system Models. In: TOOLS, vol. 47, pp. 357\u2013367 (2009)","DOI":"10.1007\/978-3-642-02571-6_21"},{"key":"243_CR33","doi-asserted-by":"crossref","unstructured":"Turner, E., Treharne, H., Schneider, S., Evans, N.: Automatic generation of CSP $${\\parallel}$$ B skeletons from xUML models. In: Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing, pp. 364\u2013379. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-85762-4_25"},{"key":"243_CR34","unstructured":"UML2 Project: http:\/\/www.eclipse.org\/modeling\/mdt\/? project=uml2 (last viewed 4th of October 2011)"},{"key":"243_CR35","doi-asserted-by":"crossref","unstructured":"Varr\u00f3, D., Asztalos, M., Bisztray, D., Boronat, A., Dang, D.H., Gei\u00a0 R., Greenyer, J., Van Gorp, P., Kniemeyer, O., Narayanan, A., Rencis, E., Weinell, E.: Transformation of UML Models to CSP: A Case Study for Graph Transformation Tools. Applications of Graph Transformations with Industrial Relevance. pp. 540\u2013565 (2008)","DOI":"10.1007\/978-3-540-89020-1_36"},{"key":"243_CR36","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"},{"issue":"4","key":"243_CR37","doi-asserted-by":"crossref","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. 41(4), 1\u201336 (2009)","journal-title":"ACM Comput. Surv."},{"key":"243_CR38","unstructured":"Xie, F., Levin, V., Browne, J.C.: Model checking for an executable subset of UML. In: ASE \u201901: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, p. 333. IEEE Computer Society, Washington, DC (2001)"},{"key":"243_CR39","doi-asserted-by":"crossref","unstructured":"Xu, D., Miao, H., Philbert, N.: Model checking UML activity diagrams in FDR. In: ICIS \u201909: Proceedings of the 2009 Eigth IEEE\/ACIS International Conference on Computer and Information Science, pp. 1035\u20131040. IEEE Computer Society, Washington, DC (2009)","DOI":"10.1109\/ICIS.2009.107"},{"key":"243_CR40","doi-asserted-by":"crossref","unstructured":"Xu, D., Philbert, N., Liu, Z., Liu, W.: Towards formalizing UML activity diagrams in CSP. In: ISCSCT \u201908: Proceedings of the 2008 International Symposium on Computer Science and Computational Technology, pp. 450\u2013453. IEEE Computer Society, Washington, DC (2008)","DOI":"10.1109\/ISCSCT.2008.379"},{"key":"243_CR41","unstructured":"Zakiuddin, I., Moffat, N., O\u2019Halloran, C., P.Ryan: Chasing events to certify a critical system. Tech. rep., UK DERA (1998)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0243-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0243-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0243-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,30]],"date-time":"2019-06-30T14:21:24Z","timestamp":1561904484000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0243-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,28]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["243"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0243-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,28]]}}}