{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T18:53:01Z","timestamp":1743015181604,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319152004"},{"type":"electronic","value":"9783319152011"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15201-1_7","type":"book-chapter","created":{"date-parts":[[2015,1,31]],"date-time":"2015-01-31T14:31:11Z","timestamp":1422714671000},"page":"101-115","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Model-Based Verification of Safety Contracts"],"prefix":"10.1007","author":[{"given":"Elena","family":"G\u00f3mez-Mart\u00ednez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ricardo J.","family":"Rodr\u00edguez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leire Etxeberria","family":"Elorza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miren Illarramendi","family":"Rezabal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clara Benac","family":"Earle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,2,1]]},"reference":[{"key":"7_CR1","unstructured":"nSafeCer project: Safety Certification of Software-Intensive Systems with Reusable Components. Project Grant Agreement n$$^{o}$$ 295373. More information at: http:\/\/safecer.eu\/"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Damm, W., Hungar, H., Josko, B., Peikenkamp, T., Stierand, I.: Using contract-based component specifications for virtual integration testing and architecture design. In: Proceedings of the Design, Automation Test in Europe Conference Exhibition (DATE), pp. 1\u20136, March 2011","DOI":"10.1109\/DATE.2011.5763167"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Tonetta, S.: A property-based proof system for contract-based design. In: Proceedings of the 38th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA), pp. 21\u201328, September 2012","DOI":"10.1109\/SEAA.2012.68"},{"key":"7_CR4","unstructured":"Kath, O., Schreiner, R., Favaro, J.: Safety, security, and software reuse: a model-based approach. In: Proceedings of the Fourth International Workshop in Software Reuse and Safety (2009)"},{"key":"7_CR5","unstructured":"OMG: Unified Modeling Language (UML). Version 2.4.1, August 2011. Specification available at: http:\/\/www.omg.org\/spec\/UML\/2.4.1\/"},{"key":"7_CR6","unstructured":"OMG: Object Constraint Language (OCL). Object Management Group, v2.2, formal\/2010-02-01, February 2010"},{"key":"7_CR7","unstructured":"OMG: UML Profile for Modeling Quality of Service and Fault Tolerance Characteristics and Mechanisms (QoS & FT). Version 1.1 (2008). Specification available at: http:\/\/www.omg.org\/spec\/QFTP\/"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez, R.J., G\u00f3mez-Mart\u00ednez, E.: Model-based safety assessment using OCL and Petri Nets. In: Proceedings of the 40th Euromicro Conference on Software Engineering and Advanced Applications (SEAA), pp. 56\u201359 (2014)","DOI":"10.1109\/SEAA.2014.36"},{"issue":"4","key":"7_CR9","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/1530873.1530876","volume":"36","author":"S Baarir","year":"2009","unstructured":"Baarir, S., Beccuti, M., Cerotti, D., De Pierro, M., Donatelli, S., Franceschinis, G.: The GreatSPN tool: recent enhancements. SIGMETRICS Perform. Eval. Rev. 36(4), 4\u20139 (2009)","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"key":"7_CR10","unstructured":"ISO\/IEC: 19505\u20131:2012-Information technology-Object Management Group Unified Modeling Language (OMG UML)-Part 1: Infrastructure (2012)"},{"key":"7_CR11","unstructured":"OMG: A UML profile for Modeling and Analysis of Real Time Embedded Systems (MARTE). Version 1.1 (2011). Specification available at: http:\/\/www.omgmarte.org\/"},{"issue":"1","key":"7_CR12","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/2379776.2379778","volume":"45","author":"S Bernardi","year":"2012","unstructured":"Bernardi, S., Merseguer, J., Petriu, D.C.: Dependability modeling and analysis of software systems specified with UML. ACM Comput. Surv. 45(1), 2 (2012)","journal-title":"ACM Comput. Surv."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez, R.J., Merseguer, J., Bernardi, S.: Modelling and analysing resilience as a security issue within UML. In: Proceedings of the 2nd International Workshop on Software Engineering for Resilient Systems, SERENE 2010, pp. 42\u201351. ACM, New York (2010)","DOI":"10.1145\/2401736.2401741"},{"issue":"4","key":"7_CR14","doi-asserted-by":"publisher","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":"7_CR15","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"M Ajmone Marsan","year":"1995","unstructured":"Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley Series in Parallel Computing, Chichester (1995)"},{"issue":"11","key":"7_CR16","doi-asserted-by":"publisher","first-page":"1843","DOI":"10.1016\/j.jss.2007.02.029","volume":"80","author":"S Bernardi","year":"2007","unstructured":"Bernardi, S., Merseguer, J.: Performance evaluation of UML design with Stochastic Well-formed Nets. J. Syst. Softw. 80(11), 1843\u20131865 (2007)","journal-title":"J. Syst. Softw."},{"issue":"3","key":"7_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.3166\/ejc.18.217-238","volume":"18","author":"A Sangiovanni-Vincentelli","year":"2012","unstructured":"Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur. J. Control 18(3), 217\u2013238 (2012)","journal-title":"Eur. J. Control"},{"key":"7_CR18","unstructured":"Bate, I., Hawkins, R., McDermid, J.: A contract-based approach to designing safe systems. In: Proceedings of the 8th Australian Workshop on Safety Critical Systems and Software, SCS 2003, vol. 33, pp. 25\u201336. Australian Computer Society, Inc. (2003)"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"S\u00f6derberg, A., Johansson, R.: Safety contract based design of software components. In: IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 365\u2013370 (2013)","DOI":"10.1109\/ISSREW.2013.6688922"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/11767589_23","volume-title":"Petri Nets and Other Models of Concurrency - ICATPN 2006","author":"E G\u00f3mez-Mart\u00ednez","year":"2006","unstructured":"G\u00f3mez-Mart\u00ednez, E., Merseguer, J.: ArgoSPE: model-based software performance engineering. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 401\u2013410. Springer, Heidelberg (2006)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/3-540-45614-7_22","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"MV Cengarle","year":"2002","unstructured":"Cengarle, M.V., Knapp, A.: Towards OCL\/RT. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 390\u2013409. Springer, Heidelberg (2002)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-28872-2_3","volume-title":"Fundamental Approaches to Software Engineering","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., David, A., Hennicker, R., Guldstrand Larsen, K., Legay, A., Nyman, U., W\u0105sowski, A.: Moving from specifications to contracts in component-based design. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 43\u201358. Springer, Heidelberg (2012)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 702\u2013705. IEEE (2013)","DOI":"10.1109\/ASE.2013.6693137"},{"issue":"1","key":"7_CR24","first-page":"7","volume":"5","author":"T Bouabana-Tebibel","year":"2008","unstructured":"Bouabana-Tebibel, T., Belmesk, M.: Integration of the association ends within UML state diagrams. Int. Arab. J. Inf. Technol. 5(1), 7\u201315 (2008)","journal-title":"Int. Arab. J. Inf. Technol."},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Sljivo, I., Gallina, B., Carlson, J., Hansson, H.: Strong and weak contract formalism for third-party component reuse. In: IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 359\u2013364, November 2013","DOI":"10.1109\/ISSREW.2013.6688921"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15201-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T06:09:46Z","timestamp":1676009386000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-15201-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319152004","9783319152011"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15201-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"1 February 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}