{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,31]],"date-time":"2024-01-31T06:11:04Z","timestamp":1706681464954},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,12,3]],"date-time":"2009-12-03T00:00:00Z","timestamp":1259798400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Requirements Eng"],"published-print":{"date-parts":[[2010,3]]},"DOI":"10.1007\/s00766-009-0091-y","type":"journal-article","created":{"date-parts":[[2009,12,2]],"date-time":"2009-12-02T16:49:52Z","timestamp":1259772592000},"page":"95-118","source":"Crossref","is-referenced-by-count":21,"title":["A UML-based static verification framework for security"],"prefix":"10.1007","volume":"15","author":[{"given":"Igor","family":"Siveroni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Zisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George","family":"Spanoudakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,12,3]]},"reference":[{"key":"91_CR1","doi-asserted-by":"crossref","unstructured":"Mouratidis H, Giorgini P (2006) Integrating security and software engineering: advances and future vision. IGI Global","DOI":"10.4018\/978-1-59904-147-6"},{"key":"91_CR2","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1109\/MS.2003.1159030","volume":"20","author":"I Alexander","year":"2003","unstructured":"Alexander I (2003) Misuse cases: use cases with hostile intent. IEEE Softw 20:58\u201366","journal-title":"IEEE Softw"},{"key":"91_CR3","unstructured":"The Common Criteria. http:\/\/www.commoncriteriaportal.org"},{"key":"91_CR4","volume-title":"Building secure software: how to avoid security problems the right way","author":"J Viega","year":"2001","unstructured":"Viega J (2001) Building secure software: how to avoid security problems the right way. Addison-Wesley, Reading"},{"key":"91_CR5","doi-asserted-by":"crossref","unstructured":"Abadi M, Blanchet B, Fournet C (2004) Just fast keying in the pi calculus. In: 13th European symposium on programming (ESOPG04). Springer, pp 340\u2013354","DOI":"10.1007\/978-3-540-24725-8_24"},{"key":"91_CR6","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1016\/S0140-3664(99)00030-4","volume":"22","author":"S Gritzalis","year":"1999","unstructured":"Gritzalis S, Spinellis D, Georgiadis P (1999) Security protocols over open networks and distributed systems: formal methods for their analysis, design, and verification. Comput Commun 22:70\u201377","journal-title":"Comput Commun"},{"key":"91_CR7","unstructured":"Meadows C (1994) Formal verification of cryptographic protocols: a survey. In: ASIACRYPT, pp 135\u2013150"},{"key":"91_CR8","unstructured":"Jayaram KR, Mathur AP (2005) Software engineering for secure software\u2014state of the art: a survey. Tech. rep., Purdue University"},{"key":"91_CR9","volume-title":"Security engineering: a guide to building dependable distributed systems","author":"RJ Anderson","year":"2008","unstructured":"Anderson RJ (2008) Security engineering: a guide to building dependable distributed systems. Wiley, Chichester"},{"key":"91_CR10","doi-asserted-by":"crossref","unstructured":"Devanbu PT (2000) Software engineering for security: a roadmap. In: The future of software engineering. ACM Press, pp 227\u2013239","DOI":"10.1145\/336512.336559"},{"issue":"8","key":"91_CR11","doi-asserted-by":"crossref","first-page":"609","DOI":"10.1016\/j.is.2004.06.002","volume":"30","author":"H Mouratidis","year":"2005","unstructured":"Mouratidis H, Giorgini P, Manson G (2005) When security meets software engineering: a case of modelling secure information systems. Inf Syst 30(8):609\u2013629","journal-title":"Inf Syst"},{"key":"91_CR12","unstructured":"PEPERS project. http:\/\/www.pepers.org"},{"key":"91_CR13","unstructured":"Redwine S, Davis N (2004) Processes to produce secure software: towards more secure software. Software security subgroup of the task force on security across the software development cycle. National Cyber Security Summit"},{"key":"91_CR14","unstructured":"Gnesi S, Mazzanti F (2004) On the fly model checking of communicating UML state machines. In: ACIS. IEEE"},{"key":"91_CR15","unstructured":"Object Management Group. http:\/\/www.uml.org"},{"key":"91_CR16","volume-title":"Handbook of theoretical computer science, vol B: formal models and semantics","author":"E Emerson","year":"1990","unstructured":"Emerson E (1990) Temporal and modal logic. In: Leeuwen JV (ed) Handbook of theoretical computer science, vol B: formal models and semantics. MIT Press, Cambridge"},{"key":"91_CR17","volume-title":"The SPIN model checker: primer and reference manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann GJ (2003) The SPIN model checker: primer and reference manual. Addison-Wesley, Reading"},{"key":"91_CR18","volume-title":"Security in computing","author":"CP Pfleeger","year":"2006","unstructured":"Pfleeger CP, Pfleeger SL (2006) Security in computing. Prentice Hall PTR, Upper Saddle River"},{"key":"91_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The formal semantic of programming languages","author":"G Wynskel","year":"1993","unstructured":"Wynskel G (1993) The formal semantic of programming languages. MIT Press, Cambridge"},{"issue":"1","key":"91_CR20","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F Schneider","year":"2000","unstructured":"Schneider F (2000) Enforceable security policies. ACM Trans Inf Syst Secur 3(1):30\u201350","journal-title":"ACM Trans Inf Syst Secur"},{"key":"91_CR21","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J (2002) A UML statecharts semantics with message-passing. In: Applied Computing 2002. Proceedings of the 2002 ACM symposium of applied computing, Madrid, pp 1009\u20131013","DOI":"10.1145\/508791.508987"},{"key":"91_CR22","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J, Shabalin P (2004) Automated verification of UMLsec models for security requirements. In: Baar T, Strohmeier A, Moreira A, Mellor SJ (eds) UML 2004\u2014The unified modeling language. Model languages and applications. 7th International conference, Lisbon, Portugal, October 11\u201315, 2004, Proceedings, LNCS, vol 3273. Springer, pp 365\u2013379","DOI":"10.1007\/978-3-540-30187-5_26"},{"key":"91_CR23","unstructured":"Papyrus UML. http:\/\/www.papyrusuml.org"},{"key":"91_CR24","doi-asserted-by":"crossref","unstructured":"Siveroni I, Spanoudakis G, Zisman A (2008) Property specification and static verification of UML models. In: Proceedings of 3rd international conference on availability, reliability and security (ARES 2008). IEEE Computer Society, Barcelona","DOI":"10.1109\/ARES.2008.194"},{"key":"91_CR25","volume-title":"Secure systems development with UML","author":"J J\u00fcrjens","year":"2004","unstructured":"J\u00fcrjens J (2004) Secure systems development with UML. Springer, Berlin"},{"issue":"5","key":"91_CR26","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1007\/s10009-007-0048-8","volume":"9","author":"J J\u00fcrjens","year":"2007","unstructured":"J\u00fcrjens J, Shabalin P (2007) Tools for secure systems development with UML. Int J Softw Tools Technol Transf 9(5):527\u2013544","journal-title":"Int J Softw Tools Technol Transf"},{"key":"91_CR27","doi-asserted-by":"crossref","unstructured":"Lodderstedt T, Basin DA, Doser J (2002) Secureuml: a uml-based modeling language for model-driven security. In: UML \u201902: Proceedings of the 5th international conference on the unified modeling language. Springer, London, pp 426\u2013441","DOI":"10.1007\/3-540-45800-X_33"},{"key":"91_CR28","doi-asserted-by":"crossref","unstructured":"Mouratidis H, J\u00fcrjens J, Fox J (2006) Towards a comprehensive framework for secure systems development. In: Advanced information systems engineering, pp 48\u201362","DOI":"10.1007\/11767138_5"},{"key":"91_CR29","unstructured":"Evans A, Bruel JM, France R, Lano K, Rumpe B (1998) Making UML precise. In: Andrade L, Moreira A, Deshpande A, Kent S (eds) Proceedings of the OOPSLA\u201998 workshop on formalizing UML. Why? How?. http:\/\/www.citeseer.ist.psu.edu\/evans98making.html"},{"issue":"2","key":"91_CR30","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/s10270-002-0012-8","volume":"1","author":"M Beeck von der","year":"2002","unstructured":"von der Beeck M (2002) A structured operational semantics for uml-statecharts. Softw Syst Model 1(2):130\u2013141","journal-title":"Softw Syst Model"},{"key":"91_CR31","unstructured":"Paltor I, Lilius J (1999) Formalising uml state machines for model checking. In: France RB, Rumpe B (eds) UML 1999, Lecture Notes in Computer Science, vol 1723. Springer, pp 430\u2013445"},{"key":"91_CR32","unstructured":"Jussila T, Dubrovin J, Junttila T, Latvala T, Porres I (2006) Model checking dynamic and hierarchical UML state machines. In: Hearnden D, S+++ JG, Baudry B, Rapin N (eds) MoDeV-a: model development, validation and verification. University of Queensland, Le Commissariat + l\u2019Energie Atomique - CEA"},{"issue":"6","key":"91_CR33","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D Latella","year":"1999","unstructured":"Latella D, Majzik I, Massink M (1999) Automatic verification of a behavioural subset of uml statechart diagrams using the spin model-checker. Formal Asp Comput 11(6):637\u2013664","journal-title":"Formal Asp Comput"},{"key":"91_CR34","unstructured":"Paltor IP, Lilius J (1999) vUML: a tool for verifying UML models. In: Hall RJ, Tyugu E (eds) Proceedings of the 14th IEEE international conference on automated software engineering, ASE\u201999. IEEE"},{"issue":"3","key":"91_CR35","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/S1571-0661(04)00262-2","volume":"55","author":"T Sch\u00e4fer","year":"2001","unstructured":"Sch\u00e4fer T, Knapp A, Merz S (2001) Model checking UML state machines and collaborations. Electron Notes Theor Comput Sci 55(3):13","journal-title":"Electron Notes Theor Comput Sci"},{"key":"91_CR36","doi-asserted-by":"crossref","unstructured":"Latella D, Majzik I, Massink M (1999) Towards a formal operational semantics of uml statechart diagrams. In: Proceedings of the IFIP TC6\/WG6.1 3rd international conference on formal methods for open object-based distributed systems (FMOODS). Kluwer, Deventer, p 465","DOI":"10.1007\/978-0-387-35562-7_25"},{"issue":"1","key":"91_CR37","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/S1567-8326(01)00012-1","volume":"51","author":"S Gnesi","year":"2002","unstructured":"Gnesi S, Latella D, Massink M (2002) Modular semantics for a UML statechart diagrams kernel and its extension to multicharts and branching time model-checking. J Logic Algebraic Program 51(1):43\u201375","journal-title":"J Logic Algebraic Program"},{"key":"91_CR38","doi-asserted-by":"crossref","unstructured":"Kuske S (2001) A formal semantics of UML state machines based on structured graph transformation. In: UML 2001: Proceedings of the 4th international conference on the unified modeling language, modeling languages, concepts, and tools. Springer, London, pp 241\u2013256","DOI":"10.1007\/3-540-45441-1_19"},{"key":"91_CR39","unstructured":"Xie F, Levin V, Browne JC (2001) Model checking for an executable subset of uml. Automated Software Engineering, ASE 2001, p 333"},{"key":"91_CR40","doi-asserted-by":"crossref","unstructured":"M\u00f6ller M, Olderog ER, Rasch H, Wehrheim H (2008) Integrating a formal method into a software engineering process with UML and Java. Formal Aspects Comput 20(2):161\u2013204. http:\/\/www.dx.doi.org\/10.1007\/s00165-007-0042-7","DOI":"10.1007\/s00165-007-0042-7"},{"key":"91_CR41","unstructured":"ter Beek MH, Fantechi A, Gnesi S, Mazzanti F (2007) An action\/state-based model-checking approach for the analysis of communication protocols for service-oriented applications. In: FMICS, pp 133\u2013148"},{"issue":"4","key":"91_CR42","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1023\/A:1026599015809","volume":"13","author":"J Hatcliff","year":"2000","unstructured":"Hatcliff J, Dwyer M, Zheng H (2000) Slicing software for model construction. High Order Symb Comput 13(4):315\u2013353","journal-title":"High Order Symb Comput"},{"key":"91_CR43","doi-asserted-by":"crossref","unstructured":"Kloukinas C, Spanoudakis G (2007) A pattern-driven framework for monitoring security and dependability. In: TrustBus, pp 210\u2013218","DOI":"10.1007\/978-3-540-74409-2_23"},{"key":"91_CR44","doi-asserted-by":"crossref","unstructured":"Spanoudakis G, Kloukinas C, Androutsopoulos K (2007) Towards security monitoring patterns. In: SAC, pp 1518\u20131525","DOI":"10.1145\/1244002.1244327"}],"container-title":["Requirements Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-009-0091-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00766-009-0091-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00766-009-0091-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,24]],"date-time":"2020-05-24T01:13:18Z","timestamp":1590282798000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00766-009-0091-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,12,3]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["91"],"URL":"https:\/\/doi.org\/10.1007\/s00766-009-0091-y","relation":{},"ISSN":["0947-3602","1432-010X"],"issn-type":[{"value":"0947-3602","type":"print"},{"value":"1432-010X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,12,3]]}}}