{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:26:36Z","timestamp":1759332396752,"version":"3.37.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030349677"},{"type":"electronic","value":"9783030349684"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-34968-4_4","type":"book-chapter","created":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T19:14:54Z","timestamp":1574363694000},"page":"65-82","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Using Ontologies in Formal Developments Targeting Certification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6355-1200","authenticated-orcid":false,"given":"Achim D.","family":"Brucker","sequence":"first","affiliation":[]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,22]]},"reference":[{"key":"4_CR1","unstructured":"Fluent editor (2018). \nhttp:\/\/www.cognitum.eu\/Semantics\/FluentEditor\/"},{"key":"4_CR2","unstructured":"The neon toolkit (2018). \nhttp:\/\/neon-toolkit.org"},{"key":"4_CR3","unstructured":"Owlgred (2018). \nhttp:\/\/owlgred.lumii.lv\/"},{"key":"4_CR4","unstructured":"Prot\u00e9g\u00e9 (2018). \nhttps:\/\/protege.stanford.edu"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-39320-4_29","volume-title":"Intelligent Computer Mathematics","author":"B Barras","year":"2013","unstructured":"Barras, B., et al.: Pervasive parallelism in highly-trustable interactive theorem proving systems. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 359\u2013363. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39320-4_29"},{"key":"4_CR6","unstructured":"Bezzecchi, S., Crisafulli, P., Pichot, C., Wolff, B.: Making agile development processes fit for V-style certification procedures. In: ERTS Conference Proceedings (2018)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-38601-5_7","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2013","author":"I Bicchierai","year":"2013","unstructured":"Bicchierai, I., Bucci, G., Nocentini, C., Vicario, E.: Using ontologies in the integration of structural, functional, and process perspectives in the development of safety critical systems. In: Keller, H.B., Pl\u00f6dereder, E., Dencker, P., Klenk, H. (eds.) Ada-Europe 2013. LNCS, vol. 7896, pp. 95\u2013108. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-38601-5_7"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-96812-4_3","volume-title":"Intelligent Computer Mathematics","author":"AD Brucker","year":"2018","unstructured":"Brucker, A.D., Ait-Sadoune, I., Crisafulli, P., Wolff, B.: Using the isabelle ontology framework. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) CICM 2018. LNCS (LNAI), vol. 11006, pp. 23\u201338. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-96812-4_3"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Brucker, A.D., Wolff, B.: Isabelle\/DOF (2019).\nhttps:\/\/doi.org\/10.5281\/zenodo.3370483","DOI":"10.5281\/zenodo.3370483"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-030-30446-1_15","volume-title":"Software Engineering and Formal Methods","author":"AD Brucker","year":"2019","unstructured":"Brucker, A.D., Wolff, B.: Isabelle\/DOF: design and implementation. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 275\u2013292. Springer, Cham (2019b). \nhttps:\/\/doi.org\/10.1007\/978-3-030-30446-1_15"},{"key":"4_CR11","unstructured":"BS EN 50128:2011: Bs en 50128:2011: Railway applications - communication, signalling and processing systems - software for railway control and protecting systems. Standard, Britisch Standards Institute (BSI) (2014)"},{"key":"4_CR12","unstructured":"Common Criteria: Common criteria for information technology security evaluation (version 3.1), Part 3: Security assurance components (2006). \nCCMB-2006-09-003"},{"issue":"2","key":"4_CR13","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s10817-009-9119-8","volume":"42","author":"M Daum","year":"2009","unstructured":"Daum, M., D\u00f6rrenb\u00e4cher, J., Wolff, B.: Proving fairness and implementation correctness of a microkernel scheduler. J. Autom. Reasoning 42(2), 349\u2013388 (2009). \nhttps:\/\/doi.org\/10.1007\/s10817-009-9119-8","journal-title":"J. Autom. Reasoning"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Denney, E., Pai, G.: Evidence arguments for using formal methods in software certification. In: IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 375\u2013380 (2013). \nhttps:\/\/doi.org\/10.1109\/ISSREW.2013.6688924","DOI":"10.1109\/ISSREW.2013.6688924"},{"key":"4_CR15","series-title":"IFIP International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-0-387-72367-9_8","volume-title":"New Approaches for Security, Privacy and Trust in Complex Environments","author":"A Ekclhart","year":"2007","unstructured":"Ekclhart, A., Fenz, S., Goluch, G., Weippl, E.: Ontological mapping of common criteria\u2019s security assurance requirements. In: Venter, H., Eloff, M., Labuschagne, L., Eloff, J., von Solms, R. (eds.) SEC 2007. IIFIP, vol. 232, pp. 85\u201395. Springer, Boston, MA (2007). \nhttps:\/\/doi.org\/10.1007\/978-0-387-72367-9_8"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Gleirscher, M., Ratiu, D., Schatz, B.: Incremental integration of heterogeneous systems views. In: 2007 International Conference on Systems Engineering and Modeling, pp. 50\u201359 (2007). \nhttps:\/\/doi.org\/10.1109\/ICSEM.2007.373334","DOI":"10.1109\/ICSEM.2007.373334"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-32347-8_8","volume-title":"Interactive Theorem Proving","author":"D Greenaway","year":"2012","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: automatic verified abstraction of C. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 99\u2013115. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32347-8_8"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-319-09770-1_12","volume-title":"Trust, Privacy, and Security in Digital Business","author":"SP Kaluvuri","year":"2014","unstructured":"Kaluvuri, S.P., Bezzi, M., Roudier, Y.: A quantitative analysis of common criteria certification practice. In: Eckert, C., Katsikas, S.K., Pernul, G. (eds.) TrustBus 2014. LNCS, vol. 8647, pp. 132\u2013143. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-09770-1_12"},{"key":"4_CR19","unstructured":"Kelly, T., Weaver, R.: The goal structuring notation - a safety argument notation. In: Dependable Systems and Networks (2004)"},{"issue":"1","key":"4_CR20","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s12046-009-0002-4","volume":"34","author":"G Klein","year":"2009","unstructured":"Klein, G.: Operating system verification \u2013 an overview. S\u0101dhan\u0101 34(1), 27\u201369 (2009)","journal-title":"S\u0101dhan\u0101"},{"issue":"1","key":"4_CR21","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., et al.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2:1\u20132:70 (2014). \nhttps:\/\/doi.org\/10.1145\/2560537","journal-title":"ACM Trans. Comput. Syst."},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"4_CR23","unstructured":"Rushby, J.: Formal methods and the certification of critical systems. Technical report SRI-CSL-93-7, Computer Science Laboratory, SRI International, Menlo Park, CA (1993). Also issued under the title Formal Methods and Digital Systems Validation for Airborne Systems as NASA Contractor Report 4551, December 1993"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-319-08970-6_33","volume-title":"Interactive Theorem Proving","author":"M Wenzel","year":"2014","unstructured":"Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle\/PIDE. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 515\u2013530. Springer, Cham (2014a). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08970-6_33"},{"key":"4_CR25","doi-asserted-by":"publisher","first-page":"84","DOI":"10.4204\/EPTCS.167.10","volume":"167","author":"Makarius Wenzel","year":"2014","unstructured":"Wenzel, M.: System description: Isabelle\/jEdit in 2014. In: Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, UITP 2014, Vienna, Austria, 17th July 2014, pp. 84\u201394 (2014b). \nhttps:\/\/doi.org\/10.4204\/EPTCS.167.10","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"4","key":"4_CR26","doi-asserted-by":"publisher","first-page":"1321","DOI":"10.1109\/TII.2016.2569414","volume":"12","author":"Y Zhao","year":"2016","unstructured":"Zhao, Y., San\u00e1n, D., Zhang, F., Liu, Y.: Formal specification and analysis of partitioning operating systems by integrating ontology and refinement. IEEE Trans. Ind. Inf. 12(4), 1321\u20131331 (2016)","journal-title":"IEEE Trans. Ind. Inf."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34968-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T19:16:54Z","timestamp":1574363814000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34968-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030349677","9783030349684"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34968-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"22 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ifm2019.hvl.no\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}