{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T18:40:25Z","timestamp":1743619225334,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642307287"},{"type":"electronic","value":"9783642307294"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30729-4_22","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T08:49:46Z","timestamp":1340786986000},"page":"312-326","source":"Crossref","is-referenced-by-count":7,"title":["Specifying UML Protocol State Machines in Alloy"],"prefix":"10.1007","author":[{"given":"Ana","family":"Garis","sequence":"first","affiliation":[]},{"given":"Ana C. R.","family":"Paiva","sequence":"additional","affiliation":[]},{"given":"Alcino","family":"Cunha","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Riesco","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Anastasakis, K.: A Model Driven Approach for the Automated Analysis of UML Class Diagrams. Ph.D. thesis, University of Birmingham (2009)"},{"issue":"1","key":"22_CR2","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10270-008-0110-3","volume":"9","author":"K. Anastasakis","year":"2008","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. Software and Systems Modeling\u00a09(1), 69\u201386 (2008)","journal-title":"Software and Systems Modeling"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"de Andrade, F.R., Faria, J.P., Paiva, A.C.R.: Test generation from bounded algebraic specifications using alloy. In: ICSOFT (2), pp. 192\u2013200 (2011)","DOI":"10.5220\/0003528101920200"},{"key":"22_CR4","unstructured":"ATLAS: ATLAS Transformation Language, LINA&INRIA (2009)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-642-03741-2_25","volume-title":"Algebra and Coalgebra in Computer Science","author":"S.S. Bauer","year":"2009","unstructured":"Bauer, S.S., Hennicker, R.: Views on Behaviour Protocols and Their Semantic Foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 367\u2013382. Springer, Heidelberg (2009)"},{"issue":"1-2","key":"22_CR6","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/s11334-009-0120-5","volume":"6","author":"B.F.B. Braga","year":"2010","unstructured":"Braga, B.F.B., Almeida, J.P.A., Guizzardi, G., Benevides, A.B.: Transforming OntoUML into Alloy: towards conceptual model validation using a lightweight formal method. Innovations in Systems and Software Engineering\u00a06(1-2), 55\u201363 (2010)","journal-title":"Innovations in Systems and Software Engineering"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-642-24690-6_16","volume-title":"Software Engineering and Formal Methods","author":"A. Garis","year":"2011","unstructured":"Garis, A., Cunha, A., Riesco, D.: Translating Alloy Specifications to UML Class Diagrams Annotated with OCL. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol.\u00a07041, pp. 221\u2013236. Springer, Heidelberg (2011)"},{"issue":"3","key":"22_CR9","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1109\/TSE.2010.36","volume":"36","author":"G. Georg","year":"2010","unstructured":"Georg, G., Anastasakis, K., Bordbar, B., Houmb, S.H., Toahchoodee, I.R.M.: Verification and trade-off analysis of security properties in UML system models. IEEE Transactions on Software Engineering\u00a036(3), 338\u2013356 (2010)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR10","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2006)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"676","DOI":"10.1007\/11880240_47","volume-title":"Model Driven Engineering Languages and Systems","author":"P. Kosiuczenko","year":"2006","unstructured":"Kosiuczenko, P.: Specification of Invariability in OCL. In: Wang, J., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol.\u00a04199, pp. 676\u2013691. Springer, Heidelberg (2006)"},{"key":"22_CR12","unstructured":"Lanoix, A., Souqui\u00e8res, J.: Trustworthy Assembly of Components using B Refinement. e-Informatica Software Engineering Journal (ISEJ) 2(1) (2008)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-642-24485-8_44","volume-title":"Model Driven Engineering Languages and Systems","author":"S. Maoz","year":"2011","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: CD2Alloy: Class Diagrams Analysis Using Alloy Revisited. In: Whittle, J., Clark, T., K\u00fchne, T. (eds.) MODELS 2011. LNCS, vol.\u00a06981, pp. 592\u2013607. Springer, Heidelberg (2011)"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Mostefaoui, F., Vachon, J.: Verification of Aspect-UML models using Alloy. In: Proceedings of the 10th International Workshop on Aspect-Oriented Modeling, pp. 41\u201348. ACM (2007)","DOI":"10.1145\/1229375.1229382"},{"issue":"99","key":"22_CR15","first-page":"547","volume":"71","author":"A. Nimiya","year":"2010","unstructured":"Nimiya, A., Yokigawa, T., Miyazaki, H., Amasaki, S., Sato, Y., Hayase, M.: Model checking consistency of UML diagrams using Alloy. World Academy of Science, Engineering and Technology\u00a071(99), 547\u2013550 (2010)","journal-title":"World Academy of Science, Engineering and Technology"},{"key":"22_CR16","unstructured":"OMG: UML Superstructure, Version 2.4.1 (2011)"},{"key":"22_CR17","unstructured":"OMG: Object Constraint Language, Version 2.3.1 (2012)"},{"issue":"2","key":"22_CR18","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/j.entcs.2007.08.010","volume":"190","author":"A.C.R. Paiva","year":"2007","unstructured":"Paiva, A.C.R., Faria, J.C.P., Vidal, R.F.A.M.: Towards the integration of visual and formal models for GUI testing. Electronic Notes in Theoretical Computer Science\u00a0190(2), 99\u2013111 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Porres, I., Rauf, I.: Generating class contracts from UML protocol statemachines. In: Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation, MoDeVVa 2009. pp. 8:1\u20138:10. ACM (2009)","DOI":"10.1145\/1656485.1656493"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-39958-2_16","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"H. Rasch","year":"2003","unstructured":"Rasch, H., Wehrheim, H.: Checking Consistency in UML Diagrams: Classes and State Machines. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 229\u2013243. Springer, Heidelberg (2003)"},{"key":"22_CR21","unstructured":"Ries, B.: SESAME: A Model-Driven Process for the Test Selection of Small-Size Safety- Related Embebbed Software. Ph.D. thesis, Universit\u00e9 du Luxembourg (2009)"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Schinz, I., Toben, T., Mrugalla, C., Westphal, B.: The Rhapsody UML verification environment. In: Proceedings of the Software Engineering and Formal Methods, SEFM 2004. pp. 174\u2013183 (2004)","DOI":"10.1109\/SEFM.2004.1347518"},{"key":"22_CR23","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C. Snook","year":"2006","unstructured":"Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol.\u00a015, 92\u2013122 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"22_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-39979-7_16","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2003","author":"M. Taghdiri","year":"2003","unstructured":"Taghdiri, M., Jackson, D.: A Lightweight Formal Analysis of a Multicast Key Management Scheme. In: K\u00f6nig, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol.\u00a02767, pp. 240\u2013256. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30729-4_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T18:22:02Z","timestamp":1743618122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30729-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642307287","9783642307294"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30729-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}