{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:13:24Z","timestamp":1761621204745},"reference-count":80,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2015,2,28]],"date-time":"2015-02-28T00:00:00Z","timestamp":1425081600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Computing"],"published-print":{"date-parts":[[2015,7]]},"DOI":"10.1007\/s00607-015-0445-x","type":"journal-article","created":{"date-parts":[[2015,2,27]],"date-time":"2015-02-27T04:41:03Z","timestamp":1425012063000},"page":"691-711","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Specification, verification, and quantification of security in model-based systems"],"prefix":"10.1007","volume":"97","author":[{"given":"Samir","family":"Ouchani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mourad","family":"Debbabi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,2,28]]},"reference":[{"key":"445_CR1","volume-title":"Hacking exposed VoIP: voice over IP security secrets & solutions","author":"D Endler","year":"2007","unstructured":"Endler D, Collier M (2007) Hacking exposed VoIP: voice over IP security secrets & solutions. McGraw-Hill, New York"},{"key":"445_CR2","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. The MIT Press, New York"},{"key":"445_CR3","unstructured":"Clarke Jr. EM, Grumberg O, Peled DA (1999) Model checking. The MIT Press, New York"},{"key":"445_CR4","doi-asserted-by":"crossref","unstructured":"Huang HSY, Cheng KTG (1998) Formal equivalence checking and design debugging. In: Frontiers in electronic testing, FRET 12. Kluwer Academic, New York","DOI":"10.1007\/978-1-4615-5693-0"},{"key":"445_CR5","doi-asserted-by":"crossref","unstructured":"Newborn M (2001) Automated theorem proving\u2014theory and practice. Springer, New York","DOI":"10.1007\/978-1-4613-0089-2"},{"key":"445_CR6","doi-asserted-by":"crossref","unstructured":"Lange CFJ, Chaudron MRV (2005) Managing model quality in UML-based software development. In: Software technology and engineering practice, pp 7\u201316","DOI":"10.1109\/STEP.2005.16"},{"key":"445_CR7","unstructured":"OMG (2007) OMG unified modeling language (OMG UML) superstructure, V2.1.2. Object Management Group. OMG available specification, Needham"},{"key":"445_CR8","doi-asserted-by":"crossref","unstructured":"Holt J, Perry S (2007) SysML for systems engineering. Institution of Engineering and Technology Press, London","DOI":"10.1049\/PBPC007E"},{"key":"445_CR9","unstructured":"OMG (2014) OMG systems modeling language (OMG SysML) specification. Object Management Group, OMG available specification, Needham"},{"key":"445_CR10","unstructured":"J\u00fcrjens J (2005) Secure systems development with UML. Springer, New York"},{"key":"445_CR11","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J, Shabalin P (2004) Tools for critical systems development with UML (tool demo). In: Nunes NJ, Selic B, Rodrigues da Silva A, Toval \u00c1lvarez JA (eds) UML modeling languages and applications, UML 2004 satellite activities, Lisbon, 11\u201315 October 2004. Revised selected papers, vol 3297 of Lecture notes in computer science, pp 250\u2013253. Springer, New York","DOI":"10.1007\/978-3-540-31797-5_27"},{"key":"445_CR12","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:527\u2013544","journal-title":"Int J Softw Tools Technol Transf"},{"key":"445_CR13","unstructured":"J\u00fcrjens J, Shabalin P, Alter E, Gilg A, H\u00f6hn S, Kopjev D, Lehrhuber M, Schwarzm\u00fcller S, Shen S (2004) UMLsec tool. http:\/\/inky.cs.tu-dortmund.de\/main2\/jj\/umlsectool\/index.html . Accessed June 2011"},{"key":"445_CR14","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J, Schreck J, Yu Y (2008) Automated analysis of permission-based security using UMLsec. In: Proceedings of the theory and practice of software, the 11th international conference on fundamental approaches to software engineering, FASE\u201908\/ETAPS\u201908, Heidelberg, pp 292\u2013295. Springer-Verlag, Berlin","DOI":"10.1007\/978-3-540-78743-3_21"},{"key":"445_CR15","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J, Shabalin P (2004) Automated verification of UMLsec models for security requirements. In: UML 2004\u2014the unified modeling language, vol 2460 of LNCS. Springer, New York, pp 412\u2013425","DOI":"10.1007\/978-3-540-30187-5_26"},{"key":"445_CR16","unstructured":"SPIN Team (2011) SPIN. http:\/\/spinroot.com . Accessed June 2011"},{"key":"445_CR17","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/1125808.1125810","volume":"15","author":"D Basin","year":"2006","unstructured":"Basin D, Doser J, Lodderstedt T (2006) Model driven security: from UML models to access control infrastructures. ACM Trans Softw Eng Methodol 15:39\u201391","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"445_CR18","doi-asserted-by":"crossref","unstructured":"Vardi MY (1996) An automata-theoretic approach to linear temporal logic. In: Logics for concurrency: structure versus automata, vol 1043 of Lecture notes in computer science, pp 238\u2013266. Springer-Verlag, New York","DOI":"10.1007\/3-540-60915-6_6"},{"key":"445_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE symposium on foundations of computer science, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"445_CR20","doi-asserted-by":"crossref","unstructured":"Jansen W, Jansen W, Gallagher PD, Deputy Director (2009) Directions in security metrics research","DOI":"10.6028\/NIST.IR.7564"},{"issue":"3","key":"445_CR21","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1109\/TSE.2010.60","volume":"37","author":"PK Manadhata","year":"2011","unstructured":"Manadhata PK, Wing JM (2011) An attack surface metric. IEEE Trans Softw Eng 37(3):371\u2013386","journal-title":"IEEE Trans Softw Eng"},{"key":"445_CR22","doi-asserted-by":"crossref","unstructured":"Mauw S, Oostdijk M (2005) Foundations of attack trees. In: International conference on information security and cryptology, ICISC 2005. LNCS, vol 3935, pp 186\u2013198. Springer, New York","DOI":"10.1007\/11734727_17"},{"key":"445_CR23","unstructured":"Sawilla R, Defence R&D Canada Ottawa (2007) Googling attack graphs. Defence R&D Canada, Ottawa (technical memorandum)"},{"key":"445_CR24","unstructured":"Sheyner OM (2004) Scenario graphs and attack graphs. PhD thesis, Pittsburgh (AAI3126929)"},{"key":"445_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/b105236","volume-title":"Advanced formal verification","author":"R Drechsler","year":"2004","unstructured":"Drechsler R (2004) Advanced formal verification. Kluwer Academic Publishers, Norwell"},{"key":"445_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/1-4020-4223-X","volume-title":"Modern formal methods and applications","author":"HA Gabbar","year":"2006","unstructured":"Gabbar HA (2006) Modern formal methods and applications. Springer-Verlag, Secaucus"},{"issue":"4","key":"445_CR27","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4):541\u2013580","journal-title":"Proc IEEE"},{"key":"445_CR28","volume-title":"Handbook of process algebra","author":"JA Bergstra","year":"2001","unstructured":"Bergstra JA (2001) Handbook of process algebra. Elsevier, New York"},{"key":"445_CR29","unstructured":"NuSMV Team (2011) NuSMV. http:\/\/nusmv.fbk.eu\/ . Accessed June 2011"},{"key":"445_CR30","unstructured":"UPPAAL Team (2011) UPPAAL. http:\/\/www.uppaal.org . Accessed June 2011"},{"key":"445_CR31","unstructured":"PRISM Team (2011) PRISM\u2014probabilistic symbolic model checker. http:\/\/www.prismmodelchecker.org . Accessed June 2011"},{"key":"445_CR32","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EC Jeannette","year":"1996","unstructured":"Jeannette EC, Clarke EM, Wing JM et al (1996) Formal methods: state of the art and future directions. ACM Comput Surv 28:626\u2013643","journal-title":"ACM Comput Surv"},{"key":"445_CR33","unstructured":"Cheng BHC, Konrad S, Campbell LA, Wassermann R (2003) Using security patterns to model and analyze security. In: IEEE workshop on requirements for high assurance systems, pp 13\u201322"},{"key":"445_CR34","unstructured":"Wassermann R, Cheng BHC (2003) Security patterns. In: Technical report, Michigan State University, Computer Science and Engineering, East Lansing"},{"key":"445_CR35","unstructured":"Gamma E, Helm R, Johnson R, Vlissides J (1995) Design patterns: elements of reusable object-oriented software"},{"key":"445_CR36","unstructured":"Viega J, Mcgraw G (2002) Building secure software: how to avoid security problems the right way"},{"key":"445_CR37","doi-asserted-by":"crossref","unstructured":"McUmber WE, Cheng BHC (2001) A general framework for formalizing UML with formal languages. In: Proceedings of the 23rd international conference on software engineering, ICSE \u201901, pp 433\u2013442. IEEE Computer Society, Washington, DC","DOI":"10.1109\/ICSE.2001.919116"},{"key":"445_CR38","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/s007660200020","volume":"7","author":"LA Campbell","year":"2002","unstructured":"Campbell LA, Cheng BHC, Mcumber WE, Stirewalt K (2002) Automatically detecting and visualising errors in UML diagrams. Requir Eng 7:264\u2013287","journal-title":"Requir Eng"},{"key":"445_CR39","doi-asserted-by":"crossref","unstructured":"Siveroni I, Zisman A, Spanoudakis G (2008) Property specification and static verification of UML models. In: Proceedings of the 2008 third international conference on availability, pp 96\u2013103. IEEE Computer Society, Reliability and Security, Washington, DC","DOI":"10.1109\/ARES.2008.194"},{"key":"445_CR40","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s00766-009-0091-y","volume":"15","author":"I Siveroni","year":"2010","unstructured":"Siveroni I, Zisman A, Spanoudakis G (2010) A UML-based static verification framework for security. Requir Eng 15:95\u2013118","journal-title":"Requir Eng"},{"key":"445_CR41","doi-asserted-by":"crossref","unstructured":"Zisman A (2007) A Static verification framework for secure peer-to-peer applications. In: Proceedings of the 2nd international conference on internet and web applications and services, ICIW \u201907, p 8. IEEE Computer Society, Washington, DC","DOI":"10.1109\/ICIW.2007.11"},{"key":"445_CR42","doi-asserted-by":"crossref","unstructured":"Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: Proceedings of the 21st international conference on software engineering, ICSE \u201999, pp 411\u2013420. ACM, New York","DOI":"10.1145\/302405.302672"},{"key":"445_CR43","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s00766-009-0093-9","volume":"15","author":"SH Houmb","year":"2010","unstructured":"Houmb SH, Islam S, Knauss E, J\u00fcrjens J, Schneider K (2010) Eliciting security requirements and tracing them to design: an integration of common criteria, heuristics, and UMLsec. Requir Eng 15:63\u201393","journal-title":"Requir Eng"},{"key":"445_CR44","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J (2005) Sound methods and effective tools for model-based security engineering with UML. In: Proceedings of the 27th international conference on software engineering, ICSE \u201905, pp 322\u2013331. ACM, New York","DOI":"10.1145\/1062455.1062519"},{"key":"445_CR45","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/s10270-007-0076-6","volume":"8","author":"J Hassine","year":"2009","unstructured":"Hassine J, Rilling J, Dssouli R (2009) Use case maps as a property specification language. Softw Syst Model 8:205\u2013220. doi: 10.1007\/s10270-007-0076-6","journal-title":"Softw Syst Model"},{"key":"445_CR46","unstructured":"Gallegos I, Gates A, Tweedie C (2010) DaProS: a data property specification tool to capture scientific sensor data properties. In: Trujillo J, Dobbie G, Kangassalo H, Hartmann S, Kirchberg M, Rossi M, Reinhartz-Berger I, Zim\u00e1nyi E, Frasincar F (eds) Advances in conceptual modeling\u2014applications and challenges, vol 6413 of Lecture notes in computer science, Springer, Berlin, pp 232\u2013241. doi: 10.1007\/978-3-642-16385-2-29"},{"key":"445_CR47","doi-asserted-by":"crossref","unstructured":"Goldsby HJ, Cheng BHC (2010) Automatically discovering properties that specify the latent behavior of UML models. In: Proceedings of the 13th international conference on model driven engineering languages and systems: part I, MODELS\u201910, Heidelberg, pp 316\u2013330. Springer-Verlag, Berlin","DOI":"10.1007\/978-3-642-16145-2_22"},{"issue":"3","key":"445_CR48","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1109\/TSE.2004.1271174","volume":"30","author":"RB France","year":"2004","unstructured":"France RB, Kim D-K, Ghosh Sudipto, Song E (2004) A UML-based pattern specification technique. IEEE Trans Softw Eng 30(3):193\u2013206","journal-title":"IEEE Trans Softw Eng"},{"key":"445_CR49","unstructured":"OMG (2006) Object constraint language, V2.0. OMG available specification. Object Management Group"},{"key":"445_CR50","unstructured":"Ziemann P, Gogolla M (2002) An extension of OCL with temporal logic. In: Critical systems development with UML, pp 53\u201362"},{"key":"445_CR51","unstructured":"Flake S, M\u00fcller W (2003) Expressing property specification patterns with OCL. In: Software engineering research and practice, pp 595\u2013603"},{"key":"445_CR52","doi-asserted-by":"crossref","unstructured":"van Lamsweerde A (2004) Elaborating security requirements by construction of intentional anti-models. In: Proceedings of the 26th international conference on software engineering, ICSE 2004, pp 148\u2013157","DOI":"10.1109\/ICSE.2004.1317437"},{"key":"445_CR53","unstructured":"Preda S, Cuppens-Boulahia N, Cuppens F, Garcia-Alfaro J, Toutain L (2010) Model-driven security policy deployment: property oriented approach. In: Massacci F, Wallach D, Zannone N (eds) Engineering secure software and systems, vol 5965 of Lecture notes in computer science, pp 123\u2013139. Springer, Berlin. doi: 10.1007\/978-3-642-11747-3-10"},{"key":"445_CR54","doi-asserted-by":"crossref","unstructured":"Kalam AAE, Baida RE, Balbiani P, Benferhat S, Cuppens F, Deswarte Y, Miege A, Saurel C, Trouessin G (2003) Organization based access control. In: Proceedings IEEE 4th international workshop on policies for distributed systems and networks, POLICY 2003, pp 120\u2013131","DOI":"10.1109\/POLICY.2003.1206966"},{"key":"445_CR55","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial J-R (1996) The B-book: assigning programs to meanings. Cambridge University Press, New York"},{"key":"445_CR56","doi-asserted-by":"crossref","unstructured":"Ouchani S, Mohamed OA, Debbabi M (2013) A security risk assessment framework for SysML activity diagrams. In: 2013 IEEE 7th international conference on software security and reliability (SERE), pp 227\u2013236","DOI":"10.1109\/SERE.2013.11"},{"key":"445_CR57","doi-asserted-by":"crossref","unstructured":"Jha S, Sheyner O, Wing J (2002) Two formal analyses of attack graphs. In: Proceedings of the 15th computer security foundation workshop, pp 49\u201363. IEEE, London","DOI":"10.1109\/CSFW.2002.1021806"},{"key":"445_CR58","doi-asserted-by":"crossref","unstructured":"Pamula J, Jajodia S, Ammann P, Swarup V (2006) A Weakest\u2013Adversary security metric for network configuration security analysis. In: Proceedings of the 2nd ACM workshop on quality of protection, QoP\u201906, pp 31\u201338, New York","DOI":"10.1145\/1179494.1179502"},{"key":"445_CR59","doi-asserted-by":"crossref","unstructured":"Frigault M, Wang L (2008) Measuring network security using Bayesian network-based attack graphs. In: 32nd annual IEEE international conference on computer software and applications, COMPSAC \u201908, pp 698\u2013703","DOI":"10.1109\/COMPSAC.2008.88"},{"key":"445_CR60","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/j.infsof.2006.06.002","volume":"49","author":"M Gegick","year":"2007","unstructured":"Gegick M, Williams L (2007) On the design of more secure software-intensive systems by use of attack patterns. Inf Softw Technol 49:381\u2013397","journal-title":"Inf Softw Technol"},{"key":"445_CR61","doi-asserted-by":"crossref","first-page":"1327","DOI":"10.1016\/j.jss.2007.11.716","volume":"81","author":"L Grunske","year":"2008","unstructured":"Grunske L, Joyce D (2008) Quantitative risk-based security prediction for component-based systems with explicitly modeled attack profiles. J Syst Softw 81:1327\u20131345","journal-title":"J Syst Softw"},{"key":"445_CR62","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s11334-010-0122-3","volume":"6","author":"P Saqui-Sannes","year":"2010","unstructured":"Saqui-Sannes P, Villemur T, Fontan B, Mota S, Bouassida MS, Chridi N, Chrisment I, Vigneron L (2010) Formal verification of secure group communication protocols modelled in UML. Innov Syst Softw Eng 6:125\u2013133","journal-title":"Innov Syst Softw Eng"},{"key":"445_CR63","doi-asserted-by":"crossref","unstructured":"Ray A (2003) Security check: a formal yet practical framework for secure software architecture. In: Proceedings of the 2003 workshop on new security paradigms, NSPW \u201903, pp 59\u201365. ACM, New York","DOI":"10.1145\/986655.986665"},{"key":"445_CR64","doi-asserted-by":"crossref","unstructured":"Thapa V, Song E, Kim H (2010) An approach to verifying security and timing properties in UML models. In: 15th IEEE international conference on engineering of complex computer systems (ICECCS), pp 193\u2013202","DOI":"10.1109\/ICECCS.2010.10"},{"key":"445_CR65","unstructured":"OMG (2008) A UML profile for MARTE: modeling and analysis of real-time embedded systems, beta 2 (convenience document without change bars). Object Management Group, OMG adopted specification, Needham"},{"key":"445_CR66","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1016\/j.infsof.2009.10.001","volume":"52","author":"J Dong","year":"2010","unstructured":"Dong J, Peng T, Zhao Y (2010) Automated verification of security pattern compositions. Inf Softw Technol 52:274\u2013295","journal-title":"Inf Softw Technol"},{"key":"445_CR67","volume-title":"A calculus of communicating systems","author":"R Milner","year":"1982","unstructured":"Milner R (1982) A calculus of communicating systems. Springer-Verlag, Secaucus"},{"key":"445_CR68","unstructured":"Moebius N, Stenzel K, Reif W (2010) Formal verification of application-specific security properties in a model-driven approach. In Massacci F, Wallach D, Zannone N (eds) Engineering secure software and systems, vol 5965 of Lecture notes in computer science, pp 166\u2013181. Springer, Berlin. doi: 10.1007\/978-3-642-11747-3-13"},{"key":"445_CR69","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1093\/comjnl\/bxq042","volume":"54","author":"A Bauer","year":"2011","unstructured":"Bauer A, J\u00fcrjens J, Yu Y (2011) Run-time security traceability for evolving systems. Comput J 54:58\u201387","journal-title":"Comput J"},{"key":"445_CR70","unstructured":"Ghosh SK, Rajkumar PV, Dasgupta P (2009) Application specific usage control implementation verification. Int J Netw Secur Appl (IJNSA) 01(03)"},{"key":"445_CR71","doi-asserted-by":"crossref","unstructured":"Ouchani S, Mohamed OA, Debbabi M, Pourzandi M (2010) Verification of the correctness in composed UML behavioural diagrams. In: SERA (selected papers), pp 163\u2013177","DOI":"10.1007\/978-3-642-13273-5_11"},{"key":"445_CR72","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/j.entcs.2009.09.064","volume":"254","author":"V Lima","year":"2009","unstructured":"Lima V, Talhi C, Mouheb D, Debbabi M, Wang L, Pourzandi M (2009) Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages. Electron Notes Theor Comput Sci 254:143\u2013160","journal-title":"Electron Notes Theor Comput Sci"},{"key":"445_CR73","doi-asserted-by":"crossref","unstructured":"Alalfi MH, Cordy JR, Dean TR (2009) A verification framework for access control in dynamic web applications. In: Canadian conference on computer science and software engineering, pp 109\u2013113","DOI":"10.1145\/1557626.1557643"},{"key":"445_CR74","doi-asserted-by":"crossref","unstructured":"Ahmed Khan MU, Zulkernine M (2008) Quantifying security in secure software development phases. In: Proceedings of the 2008 32nd annual IEEE international computer software and applications conference, pp 955\u2013960. IEEE Computer Society, Washington, DC","DOI":"10.1109\/COMPSAC.2008.173"},{"key":"445_CR75","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1109\/TSE.2010.36","volume":"36","author":"G Georg","year":"2010","unstructured":"Georg G, Anastasakis K, Bordbar B, Houmb SH, Ray I, Toahchoodee M (2010) Verification and trade-off analysis of security properties in UML system models. IEEE Trans Softw Eng 36:338\u2013356","journal-title":"IEEE Trans Softw Eng"},{"key":"445_CR76","unstructured":"Chen Y, Boehm B, Sheppard L (2003) Measuring security investment benefit for off the shelf software systems\u2014a stakeholder value driven approach"},{"key":"445_CR77","unstructured":"Liu MY, Traore I (2004) UML-based security measures of software products. In: International workshop on methodologies for pervasive and embedded software (MOMPES\u201904), 4th international conference on application of concurrency to system design (ACSD-04), Hamilton"},{"key":"445_CR78","unstructured":"Liu MY, Traore I (2005) Measurement framework for software privilege protection based on user interaction analysis. In: Proceedings of the 11th IEEE international software metrics symposium, p 10. IEEE Computer Society, Washington, DC"},{"key":"445_CR79","unstructured":"Buchholtz M, Gilmore S, Haenel V, Montangero C (2005) Endto-end integrated security and performance analysis on the DEGAS choreographer platform. In: Proceedings of the international symposium of formal methods Europe (FM 2005), vol 3582 in LNCS. Springer-Verlag, New York, pp 286\u2013301"},{"key":"445_CR80","doi-asserted-by":"crossref","unstructured":"Ouchani S, Jarraya Y, A\u00eft-Mohamed O (2011) Model-based systems security quantification. In: PST, pp 142\u2013149","DOI":"10.1109\/PST.2011.5971976"}],"container-title":["Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-015-0445-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00607-015-0445-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00607-015-0445-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,30]],"date-time":"2022-04-30T23:20:05Z","timestamp":1651360805000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00607-015-0445-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,28]]},"references-count":80,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2015,7]]}},"alternative-id":["445"],"URL":"https:\/\/doi.org\/10.1007\/s00607-015-0445-x","relation":{},"ISSN":["0010-485X","1436-5057"],"issn-type":[{"value":"0010-485X","type":"print"},{"value":"1436-5057","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,28]]}}}