{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:23:04Z","timestamp":1745986984310,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642365621"},{"type":"electronic","value":"9783642365638"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-36563-8_6","type":"book-chapter","created":{"date-parts":[[2013,2,22]],"date-time":"2013-02-22T06:32:47Z","timestamp":1361514767000},"page":"75-90","source":"Crossref","is-referenced-by-count":9,"title":["Compositional Verification of Application-Level Security Properties"],"prefix":"10.1007","author":[{"given":"Linda Ariani","family":"Gunawan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Herrmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Iyer, R.K., Chen, S., Xu, J., Kalbarczyk, Z.: Security Vulnerabilities - from Data Analysis to Protection Mechanisms. In: Proceedings of the Ninth IEEE International Workshop on Object-Oriented Real-Time Dependable Systems, WORDS 2003, pp. 331\u2013338 (2003)","DOI":"10.1109\/WORDS.2003.1267548"},{"key":"6_CR2","unstructured":"Kraemer, F.A.: Engineering Reactive Systems: A Compositional and Model-Driven Method Based on Collaborative Building Blocks. PhD thesis, Norwegian University of Science and Technology (August 2008)"},{"issue":"12","key":"6_CR3","doi-asserted-by":"publisher","first-page":"2068","DOI":"10.1016\/j.jss.2009.06.057","volume":"82","author":"F.A. Kraemer","year":"2009","unstructured":"Kraemer, F.A., Sl\u00e5tten, V., Herrmann, P.: Tool Support for the Rapid Composition, Analysis and Implementation of Reactive Services. Journal of Systems and Software\u00a082(12), 2068\u20132080 (2009)","journal-title":"Journal of Systems and Software"},{"key":"6_CR4","series-title":"CCIS","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-10847-1_10","volume-title":"Security Technology","author":"L.A. Gunawan","year":"2009","unstructured":"Gunawan, L.A., Herrmann, P., Kraemer, F.A.: Towards the Integration of Security Aspects into System Development Using Collaboration-Oriented Models. In: \u015al\u0119zak, D., Kim, T.-H., Fang, W.-C., Arnett, K.P. (eds.) SecTech 2009. CCIS, vol.\u00a058, pp. 72\u201385. Springer, Heidelberg (2009)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-13464-7_3","volume-title":"Formal Techniques for Distributed Systems","author":"F.A. Kraemer","year":"2010","unstructured":"Kraemer, F.A., Herrmann, P.: Reactive Semantics for Distributed UML Activities. In: Hatcliff, J., Zucca, E. (eds.) FMOODS\/FORTE 2010, Part II. LNCS, vol.\u00a06117, pp. 17\u201331. Springer, Heidelberg (2010)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-19125-1_11","volume-title":"Engineering Secure Software and Systems","author":"L.A. Gunawan","year":"2011","unstructured":"Gunawan, L.A., Kraemer, F.A., Herrmann, P.: A Tool-Supported Method for the Design and Implementation of Secure Distributed Applications. In: Erlingsson, \u00da., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol.\u00a06542, pp. 142\u2013155. Springer, Heidelberg (2011)"},{"key":"6_CR7","unstructured":"McMillan, K.L.: Symbolic Model Checking: an Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA (1992)"},{"key":"6_CR8","volume-title":"Software Requirements: Objects, Functions and States","author":"A.M. Davis","year":"1993","unstructured":"Davis, A.M.: Software Requirements: Objects, Functions and States, 2nd edn. Prentice-Hall, Inc., Upper Saddle River (1993)","edition":"2"},{"key":"6_CR9","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/2047862.2047888","volume-title":"Proceedings of the 10th ACM International Conference on Generative Programming and Component Engineering","author":"V. Sl\u00e5tten","year":"2011","unstructured":"Sl\u00e5tten, V., Kraemer, F.A., Herrmann, P.: Towards Automatic Generation of Formal Specifications to Validate and Verify Reliable Distributed Systems: A Method Exemplified by an Industrial Case Study. In: Proceedings of the 10th ACM International Conference on Generative Programming and Component Engineering, pp. 147\u2013156. ACM, New York (2011)"},{"key":"6_CR10","unstructured":"Object Management Group: Unified Modeling Language: Superstructure, version 2.3 (May 2010) (formal\/2010-05-05)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/978-3-642-04425-0_44","volume-title":"Model Driven Engineering Languages and Systems","author":"F.A. Kraemer","year":"2009","unstructured":"Kraemer, F.A., Herrmann, P.: Automated Encapsulation of UML Activities for Incremental Development and Verification. In: Sch\u00fcrr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol.\u00a05795, pp. 571\u2013585. Springer, Heidelberg (2009)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-21461-5_20","volume-title":"Formal Techniques for Distributed Systems","author":"V. Sl\u00e5tten","year":"2011","unstructured":"Sl\u00e5tten, V., Herrmann, P.: Contracts for Multi-instance UML Activities. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE 2011. LNCS, vol.\u00a06722, pp. 304\u2013318. Springer, Heidelberg (2011)"},{"key":"6_CR13","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Professional (2002)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y. Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model Checking TLA+ Specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 54\u201366. Springer, Heidelberg (1999)"},{"issue":"2","key":"6_CR15","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/S1389-1286(00)00089-X","volume":"34","author":"P. Herrmann","year":"2000","unstructured":"Herrmann, P., Krumm, H.: A Framework for Modeling Transfer Protocols. Computer Networks\u00a034(2), 317\u2013337 (2000)","journal-title":"Computer Networks"},{"issue":"2","key":"6_CR16","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The Existence of Refinement Mappings. Theoretical Computer Science\u00a082(2), 253\u2013284 (1991)","journal-title":"Theoretical Computer Science"},{"key":"6_CR17","unstructured":"J\u00fcrjens, J.: Secure System Development with UML. Springer (2005)"},{"issue":"1","key":"6_CR18","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/1125808.1125810","volume":"15","author":"D. Basin","year":"2006","unstructured":"Basin, D., Doser, J., Lodderstedt, T.: Model Driven Security: From UML Models to Access Control Infrastructures. ACM Transactions on Software Engineering and Methodology\u00a015(1), 39\u201391 (2006)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"6_CR19","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/1029133.1029144","volume-title":"Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering, FMSE 2004","author":"T. Doan","year":"2004","unstructured":"Doan, T., Demurjian, S., Ting, T.C., Ketterl, A.: MAC and UML for Secure Software Design. In: Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering, FMSE 2004, pp. 75\u201385. ACM, New York (2004)"},{"issue":"5","key":"6_CR20","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1016\/j.infsof.2008.05.004","volume":"51","author":"G. Georg","year":"2009","unstructured":"Georg, G., Ray, I., Anastasakis, K., Bordbar, B., Toahchoodee, M., Houmb, S.H.: An Aspect-Oriented Methodology for Designing Secure Applications. Information and Software Technology\u00a051(5), 846\u2013864 (2009); Special Issue: Model-Driven Development for Secure Information Systems","journal-title":"Information and Software Technology"},{"key":"6_CR21","series-title":"SCI","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-13273-5_13","volume-title":"Software Engineering Research, Management and Applications 2010","author":"D. Mouheb","year":"2010","unstructured":"Mouheb, D., Talhi, C., Nouh, M., Lima, V., Debbabi, M., Wang, L., Pourzandi, M.: Aspect-Oriented Modeling for Representing and Integrating Security Concerns in UML. In: Lee, R., Ormandjieva, O., Abran, A., Constantinides, C. (eds.) SERA 2010. SCI, vol.\u00a0296, pp. 197\u2013213. Springer, Heidelberg (2010)"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/11557432_11","volume-title":"Model Driven Engineering Languages and Systems","author":"J. J\u00fcrjens","year":"2005","unstructured":"J\u00fcrjens, J., Houmb, S.H.: Dynamic Secure Aspect Modeling with UML: From Models to Code. In: Briand, L.C., Williams, C. (eds.) MoDELS 2005. LNCS, vol.\u00a03713, pp. 142\u2013155. Springer, Heidelberg (2005)"},{"issue":"2","key":"6_CR23","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10270-008-0080-5","volume":"7","author":"J.M. J\u00e9z\u00e9quel","year":"2008","unstructured":"J\u00e9z\u00e9quel, J.M.: Model Driven Design and Aspect Weaving. Software and System Modeling\u00a07(2), 209\u2013218 (2008)","journal-title":"Software and System Modeling"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Lund, M.S., Solhaug, B., St\u00f8len, K.: Model-Driven Risk Analysis - The CORAS Approach. Springer (2011)","DOI":"10.1007\/978-3-642-12323-8"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-11747-3_13","volume-title":"Engineering Secure Software and Systems","author":"N. Moebius","year":"2010","unstructured":"Moebius, N., Stenzel, K., Reif, W.: Formal Verification of Application-Specific Security Properties in a Model-Driven Approach. In: Massacci, F., Wallach, D., Zannone, N. (eds.) ESSoS 2010. LNCS, vol.\u00a05965, pp. 166\u2013181. Springer, Heidelberg (2010)"},{"key":"6_CR26","unstructured":"Moebius, N., Stenzel, K., Borek, M., Reif, W.: Incremental Development of Large, Secure Smart Card Applications. In: Proceedings of the 1st Model-Driven Security Workshop, MDSec 2012 (to appear, 2012)"},{"issue":"5","key":"6_CR27","doi-asserted-by":"publisher","first-page":"1099","DOI":"10.1109\/TKDE.2003.1232267","volume":"15","author":"D. Yi","year":"2003","unstructured":"Yi, D., Wang, J., Tsai, J.J., Beznosov, K.: An Approach for Modeling and Analysis of Security System Architectures. IEEE Transactions on Knowledge and Data Engineering\u00a015(5), 1099\u20131119 (2003)","journal-title":"IEEE Transactions on Knowledge and Data Engineering"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Khan, K., Han, J., Zheng, Y.: A Framework for an Active Interface to Characterise Compositional Security Contracts of Software Components. In: Proceedings of the 2001 Australian Software Engineering Conference, pp. 117\u2013126 (2001)","DOI":"10.1109\/ASWEC.2001.948505"},{"key":"6_CR29","first-page":"45","volume-title":"Proceedings of the 17th Annual Computer Security Applications Conference (ACSAC)","author":"P. Herrmann","year":"2001","unstructured":"Herrmann, P.: Information Flow Analysis of Component-Structured Applications. In: Proceedings of the 17th Annual Computer Security Applications Conference (ACSAC), pp. 45\u201354. ACM SIGSAC, IEEE Computer Society Press, New Orleans (2001)"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Mantel, H.: On the Composition of Secure Systems. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 88\u2013101. IEEE Computer Society (May 2002)","DOI":"10.1109\/SECPRI.2002.1004364"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11768869_1","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"M. Bartoletti","year":"2006","unstructured":"Bartoletti, M., Degano, P., Ferrari, G.L.: Security Issues in Service Composition. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol.\u00a04037, pp. 1\u201316. Springer, Heidelberg (2006)"},{"key":"6_CR32","unstructured":"Vasilevskaya, M., Gunawan, L.A., Nadjm-Tehrani, S., Herrmann, P.: Security Asset Elicitation for Collaborative Models. In: Proceedings of the 1st Model-Driven Security Workshop, MDSec 2012 (to appear, 2012)"}],"container-title":["Lecture Notes in Computer Science","Engineering Secure Software and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36563-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T21:57:58Z","timestamp":1745963878000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36563-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642365621","9783642365638"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36563-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}