{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:08:04Z","timestamp":1748664484038,"version":"3.41.0"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242484"},{"type":"electronic","value":"9783319242491"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24249-1_23","type":"book-chapter","created":{"date-parts":[[2015,9,7]],"date-time":"2015-09-07T11:43:15Z","timestamp":1441626195000},"page":"264-276","source":"Crossref","is-referenced-by-count":15,"title":["Combining MILS with Contract-Based Design for Safety and Security Requirements"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"Rance","family":"DeLong","sequence":"additional","affiliation":[]},{"given":"Davide","family":"Marcantonio","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,12,9]]},"reference":[{"key":"23_CR1","unstructured":"D-MILS Project. http:\/\/www.d-mils.org\/"},{"key":"23_CR2","unstructured":"GSN community standard. Technical report, Origin Consulting (York) Limited (2011)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-11957-6_4","volume-title":"Programming Languages and Systems","author":"T Amtoft","year":"2010","unstructured":"Amtoft, T., Hatcliff, J., Rodr\u00edguez, E.: Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 43\u201363. Springer, Heidelberg (2010)"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Hatcliff, J., Rodr\u00edguez, E., Robby, Hoag, J., Greve, D.: Specification and checking of software contracts for conditional information flow. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 229\u2013245. Springer, New York (2010)","DOI":"10.1007\/978-1-4419-1539-9_12"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Anderson, M., North, C., Griffin, J., Milner, R., Yesberg, J., Yiu, K.: Starlight: interactive link. In: 12th Annual Computer Security Applications Conference, pp. 55\u201363 (1996)","DOI":"10.1109\/CSAC.1996.569669"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Boettcher, C., DeLong, R., Rushby, J., Sifre, W.: The MILS component integration approach to secure information sharing. In: 27thAIAA\/IEEE Digital Avionics Systems Conference, St. Paul, MN, October 2008","DOI":"10.1109\/DASC.2008.4702758"},{"key":"23_CR7","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M Bozzano","year":"2011","unstructured":"Bozzano, M., Cimatti, A., Katoen, J., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. Comput. J. 54, 754\u2013775 (2011)","journal-title":"Comput. J."},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-319-11936-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"M Bozzano","year":"2014","unstructured":"Bozzano, M., Cimatti, A., Mattarei, C., Tonetta, S.: Formal safety assessment via contract-based design. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 81\u201397. Springer, Heidelberg (2014)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Brunel, J., Rioux, L., Paul, S., Faucogney, A., Vall\u00e9e, F.: Formal safety and security assessment of an avionic architecture with alloy. In: ESSS, pp. 8\u201319 (2014)","DOI":"10.4204\/EPTCS.150.2"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014)"},{"key":"23_CR12","unstructured":"S. Chong and R. Van Der Meyden, Using architecture to reason about information security (2014). arXiv preprint arXiv:1409.0309"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: ASE, pp. 702\u2013705 (2013)","DOI":"10.1109\/ASE.2013.6693137"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-54862-8_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 46\u201361. Springer, Heidelberg (2014)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1007\/978-3-319-08867-9_28","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Verifying LTL properties of hybrid systems with K-liveness. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 424\u2013440. Springer, Heidelberg (2014)"},{"key":"23_CR16","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/j.scico.2014.06.011","volume":"97","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333\u2013348 (2015)","journal-title":"Sci. Comput. Program."},{"key":"23_CR17","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: FMCAD, pp. 52\u201359 (2012)"},{"key":"23_CR18","unstructured":"Specification of MILS-AADL. Technical report D2.1, Version 2.0, D-MILS Project, July 2014. http:\/\/www.d-mils.org\/page\/results"},{"key":"23_CR19","unstructured":"D2.2 translation of mils-aadl into formal architectural modeling framework. Technical report D2.2, Version 1.2, D-MILS Project, February 2014. http:\/\/www.d-mils.org\/page\/results"},{"key":"23_CR20","unstructured":"Intermediate languages and semantics transformations for distributed mils - part 1. Technical report D3.2, Version 1.2, D-MILS Project, February 2014. http:\/\/www.d-mils.org\/page\/results"},{"key":"23_CR21","unstructured":"Intermediate languages and semantics transformations for distributed mils - part 2. Technical report D3.3, Version 1.0, D-MILS Project, July 2014. http:\/\/www.d-mils.org\/page\/results"},{"key":"23_CR22","unstructured":"Compositional assurance cases and arguments for distributed mils. Technical report D4.2, Version 1.0, D-MILS Project, April 2014. http:\/\/www.d-mils.org\/page\/results"},{"key":"23_CR23","unstructured":"Integration of formal evidence and expression in mils assurance case. Technical report D4.3, Version 0.7, D-MILS Project, March 2015. http:\/\/www.d-mils.org\/page\/results"},{"key":"23_CR24","unstructured":"Compositional verification techniques and tools for distributed mils\u2013part 1. Technical report D4.4, Version 1.0, D-MILS Project, July 2014. http:\/\/www.d-mils.org\/page\/results"},{"key":"23_CR25","unstructured":"Distributed mils platform configuration compiler. Technical report D5.2, Version 0.2, D-MILS Project, March 2014. http:\/\/www.d-mils.org\/page\/results"},{"key":"23_CR26","unstructured":"Extended separation kernel capable of global exported resource addressing. Technical report D6.1, Version 2.0, D-MILS Project, March 2014. http:\/\/www.d-mils.org\/page\/results"},{"key":"23_CR27","unstructured":"Mils network system supporting TTEthernet. Technical report D6.3, Version 1.0, D-MILS Project, March 2014. http:\/\/www.d-mils.org\/page\/results"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"R. DeLong, Commentary on the MILS Network Subsystem Protection Profile. Technical report, Version 0.31, September 2011","DOI":"10.2172\/1026661"},{"key":"23_CR29","unstructured":"DeLong, R., Rushby, J.: Protection Profile for MILS Network Subsystems in Environments Requiring High Robustness, Version 0.31, September 2011"},{"key":"23_CR30","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1016\/j.cose.2009.06.005","volume":"28","author":"N Dragoni","year":"2009","unstructured":"Dragoni, N., Massacci, F., Walter, T., Schaefer, C.: What the heck is this application doing? - a security-by-contract architecture for pervasive services. Comput. Secur. 28, 566\u2013577 (2009)","journal-title":"Comput. Secur."},{"key":"23_CR31","unstructured":"Information Assurance Directorate, National Security Agency, U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, Fort George G. Meade, MD 20755\u20136000, Version 1.03, June 2007"},{"key":"23_CR32","unstructured":"Kopetz, H., Ademaj, A., Grillinger, P., Steinhammer, K.: The time-triggered ethernet (TTE) design. In: 8th IEEE International Symposium on Object-oriented Real-time distributed Computing (ISORC), Seattle, Washington (2005)"},{"key":"23_CR33","unstructured":"Rushby, J.: The design and verification of secure systems. In: Eighth ACM Symposium on Operating System Principles, Asilomar, CA, December 1981, pp. 12\u201321 (1981). (ACM Operating Systems Review, Vol. 15, No. 5)"},{"key":"23_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1007\/978-3-319-10506-2_21","volume-title":"Computer Safety, Reliability, and Security","author":"C Schmittner","year":"2014","unstructured":"Schmittner, C., Gruber, T., Puschner, P., Schoitsch, E.: Security application of failure mode and effect analysis (FMEA). In: Bondavalli, A., Di Giandomenico, F. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 310\u2013325. Springer, Heidelberg (2014)"},{"key":"23_CR35","doi-asserted-by":"crossref","unstructured":"Sojka, M., Krec, M., Hanz\u00e1lek, Z.: Case study on combined validation of safety & security requirements. In: SIES, pp. 244\u2013251 (2014)","DOI":"10.1109\/SIES.2014.6871210"},{"key":"23_CR36","unstructured":"Steiner, M., Liggesmeyer, P.: Combination of safety and security analysis - finding security problems that threaten the safety of a system. In: SAFECOMP Workshop DECS (2013)"},{"key":"23_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"MY Vardi","year":"1995","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) LC 1995. LNCS, vol. 1043, pp. 238\u2013266. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24249-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T13:23:19Z","timestamp":1748611399000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24249-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242484","9783319242491"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24249-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}