{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:02:51Z","timestamp":1743022971433,"version":"3.40.3"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030614690"},{"type":"electronic","value":"9783030614706"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-61470-6_25","type":"book-chapter","created":{"date-parts":[[2020,10,26]],"date-time":"2020-10-26T18:03:12Z","timestamp":1603735392000},"page":"416-439","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification"],"prefix":"10.1007","author":[{"given":"Rasha","family":"Faqeh","sequence":"first","affiliation":[]},{"given":"Christof","family":"Fetzer","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]},{"given":"J\u00f6rg","family":"Hoffmann","sequence":"additional","affiliation":[]},{"given":"Michaela","family":"Klauck","sequence":"additional","affiliation":[]},{"given":"Maximilian A.","family":"K\u00f6hl","sequence":"additional","affiliation":[]},{"given":"Marcel","family":"Steinmetz","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,10,27]]},"reference":[{"issue":"2","key":"25_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.3390\/safety2020009","volume":"2","author":"J Aizpurua","year":"2016","unstructured":"Aizpurua, J., Muxika, E., Papadopoulos, Y., Chiacchio, F., Manno, G.: Application of the D3H2 methodology for the cost-effective design of dependable systems. Safety 2(2), 9 (2016). https:\/\/doi.org\/10.3390\/safety2020009","journal-title":"Safety"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-662-49498-1_2","volume-title":"Programming Languages and Systems","author":"R Alur","year":"2016","unstructured":"Alur, R., Fisman, D., Raghothaman, M.: Regular programming for quantitative properties of data streams. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 15\u201340. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_2"},{"key":"25_CR3","unstructured":"Alvaro, A., de Almeida, E.S., de Lemos Meira, S.R.: Software component certification: a survey. In: 31st EUROMICRO Conference on Software Engineering and Advanced Applications, pp. 106\u2013113 (2005)"},{"key":"25_CR4","unstructured":"Araya, M., Buffet, O., Thomas, V., Charpillet, F.: A POMDP extension with belief-dependent rewards. In: Lafferty, J.D., Williams, C.K.I., Shawe-Taylor, J., Zemel, R.S., Culotta, A. (eds.) Advances in Neural Information Processing Systems 23, pp. 64\u201372. Curran Associates, Inc. (2010)"},{"key":"25_CR5","unstructured":"Arnautov, S., Trach, B., Gregor, F., Knauth, T., Martin, A., Priebe, C., Lind, J., Muthukumaran, D., O\u2019Keeffe, D., Stillwell, M.L., Goltzsche, D., Eyers, D., Kapitza, R., Pietzuch, P., Fetzer, C.: SCONE: secure Linux containers with intel SGX. In: 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2016), Savannah, GA, pp. 689\u2013703. USENIX Association (2016). https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/arnautov"},{"issue":"1","key":"25_CR6","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/TDSC.2004.2","volume":"1","author":"A Avizienis","year":"2004","unstructured":"Avizienis, A., Laprie, J.C., Randell, B., Landwehr, C.: Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secur. Comput. 1(1), 11\u201333 (2004). https:\/\/doi.org\/10.1109\/TDSC.2004.2","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"25_CR7","unstructured":"Avizienis, A., Laprie, J.C., Randell, B., et al.: Fundamental concepts of dependability. University of Newcastle upon Tyne, Computing Science (2001)"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11944836_25","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"A Bauer","year":"2006","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260\u2013272. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11944836_25"},{"key":"25_CR9","doi-asserted-by":"publisher","unstructured":"Bishop, P., Bloomfield, R.: A methodology for safety case development, February 1998. https:\/\/doi.org\/10.1007\/978-1-4471-1534-2_14","DOI":"10.1007\/978-1-4471-1534-2_14"},{"key":"25_CR10","volume-title":"Introduction to Discrete Event Systems","author":"CG Cassandras","year":"2010","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer, Heidelberg (2010)","edition":"2"},{"issue":"1","key":"25_CR11","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1109\/69.43410","volume":"1","author":"S Ceri","year":"1989","unstructured":"Ceri, S., Gottlob, G., Tanca, L.: What you always wanted to know about datalog (and never dared to ask). IEEE Trans. Knowl. Data Eng. 1(1), 146\u2013166 (1989)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"25_CR12","doi-asserted-by":"publisher","unstructured":"Council, N.R.: Software for Dependable Systems: Sufficient Evidence? The National Academies Press, Washington, DC (2007). https:\/\/doi.org\/10.17226\/11923 . https:\/\/www.nap.edu\/catalog\/11923\/software-for-dependable-systems-sufficient-evidence","DOI":"10.17226\/11923"},{"issue":"1","key":"25_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/TSE.1986.6312914","volume":"SE\u201312","author":"PA Currit","year":"1986","unstructured":"Currit, P.A., Dyer, M., Mills, H.D.: Certifying the reliability of software. IEEE Trans. Softw. Eng. SE\u201312(1), 3\u201311 (1986)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"25_CR14","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166\u2013174 (2005)"},{"key":"25_CR15","series-title":"IFIP \u2013 The International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-0-387-72258-0_33","volume-title":"Embedded System Design: Topics, Techniques and Trends","author":"M Felser","year":"2007","unstructured":"Felser, M., Kapitza, R., Klein\u00f6der, J., Schr\u00f6der-Preikschat, W.: Dynamic software update of resource-constrained distributed embedded systems. In: Rettberg, A., Zanella, M.C., D\u00f6mer, R., Gerstlauer, A., Rammig, F.J. (eds.) IESS 2007. ITIFIP, vol. 231, pp. 387\u2013400. Springer, Boston, MA (2007). https:\/\/doi.org\/10.1007\/978-0-387-72258-0_33"},{"key":"25_CR16","unstructured":"Fiori, A., Weidenbach, C.: SCL with theory constraints. CoRR abs\/2003.04627 (2020). https:\/\/arxiv.org\/abs\/2003.04627"},{"key":"25_CR17","unstructured":"Fleury, M.: Formalization of logical calculi in Isabelle\/HOL. Ph.D. thesis, Saarland University, Saarbr\u00fccken, Germany (2020)"},{"key":"25_CR18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139583923","volume-title":"Automated Planning and Acting","author":"M Ghallab","year":"2016","unstructured":"Ghallab, M., Nau, D., Traverso, P.: Automated Planning and Acting. Cambridge University Press, Cambridge (2016)"},{"key":"25_CR19","doi-asserted-by":"publisher","unstructured":"Giro, S., D\u2019Argenio, P.R., Fioriti, L.M.F.: Distributed probabilistic input\/output automata: expressiveness, (un)decidability and algorithms. Theoret. Comput. Sci. 538, 84\u2013102 (2014). Quantitative Aspects of Programming Languages and Systems (2011\u20132012). https:\/\/doi.org\/10.1016\/j.tcs.2013.07.017 . http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397513005203","DOI":"10.1016\/j.tcs.2013.07.017"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Heck, H., Rudolph, S., Gruhl, C., Wacker, A., H\u00e4hner, J., Sick, B., Tomforde, S.: Towards autonomous self-tests at runtime. In: 2016 IEEE 1st International Workshops on Foundations and Applications of Self* Systems (FAS*W), pp. 98\u201399 (2016)","DOI":"10.1109\/FAS-W.2016.32"},{"key":"25_CR21","unstructured":"Heimerdinger, W., Weinstock, C.: A conceptual framework for system fault tolerance. Technical report CMU\/SEI-92-TR-033, Software Engineering Institute, Carnegie Mellon University, Pittsburgh, PA (1992). http:\/\/resources.sei.cmu.edu\/library\/asset-view.cfm?AssetID=11747"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-319-63046-5_6","volume-title":"Automated Deduction \u2013 CADE 26","author":"M Horbach","year":"2017","unstructured":"Horbach, M., Voigt, M., Weidenbach, C.: On the combination of the Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey fragment with simple linear integer arithmetic. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 77\u201394. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_6"},{"key":"25_CR23","unstructured":"Horbach, M., Voigt, M., Weidenbach, C.: The universal fragment of Presburger arithmetic with unary uninterpreted predicates is undecidable. CoRR abs\/1703.01212 (2017)"},{"key":"25_CR24","unstructured":"Kessler, A.M.: Elon musk says self-driving tesla cars will be in the US by summer. The New York Times 19, 1 (2015). https:\/\/www.nytimes.com\/2015\/03\/20\/business\/elon-musk-says-self-driving-tesla-cars-will-be-in-the-us-by-summer.html"},{"key":"25_CR25","doi-asserted-by":"publisher","unstructured":"Kuvaiskii, D., Faqeh, R., Bhatotia, P., Felber, P., Fetzer, C.: HAFT: hardware-assisted fault tolerance. In: Proceedings of the Eleventh European Conference on Computer Systems, EuroSys 2016. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2901318.2901339","DOI":"10.1145\/2901318.2901339"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Kuvaiskii, D., Fetzer, C.: $$\\delta $$-encoding: Practical encoded processing (2015)","DOI":"10.1109\/DSN.2015.20"},{"key":"25_CR27","doi-asserted-by":"publisher","unstructured":"Kuvaiskii, D., Oleksenko, O., Arnautov, S., Trach, B., Bhatotia, P., Felber, P., Fetzer, C.: SGXBOUNDS: memory safety for shielded execution. In: Proceedings of the Twelfth European Conference on Computer Systems, EuroSys 2017, pp. 205\u2013221. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3064176.3064192","DOI":"10.1145\/3064176.3064192"},{"key":"25_CR28","doi-asserted-by":"publisher","unstructured":"Kuvaiskii, D., Oleksenko, O., Bhatotia, P., Felber, P., Fetzer, C.: ELZAR: triple modular redundancy using intel AVX (practical experience report). In: 2016 46th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), June 2016. https:\/\/doi.org\/10.1109\/dsn.2016.65","DOI":"10.1109\/dsn.2016.65"},{"issue":"3","key":"25_CR29","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s10817-019-09525-z","volume":"64","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513\u2013532 (2020)","journal-title":"J. Autom. Reason."},{"key":"25_CR30","series-title":"Dependable Computing and Fault-Tolerant Systems","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-7091-9170-5_1","volume-title":"Dependability: Basic Concepts and Terminology","author":"JC Laprie","year":"1992","unstructured":"Laprie, J.C.: Dependability: basic concepts and terminology. In: Laprie, J.C. (ed.) Dependability: Basic Concepts and Terminology. DEPENDABLECOMP, vol. 5, pp. 3\u2013245. Springer, Vienna (1992). https:\/\/doi.org\/10.1007\/978-3-7091-9170-5_1"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Leucker, M., S\u00e1nchez, C., Scheffel, T., Schmitz, M., Schramm, A.: TeSSLa: runtime verification of non-synchronized real-time streams. In: ACM Symposium on Applied Computing (SAC), France. ACM, April 2018","DOI":"10.1145\/3167132.3167338"},{"issue":"5","key":"25_CR32","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78(5), 293\u2013303 (2009). The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS \u201907)","journal-title":"J. Logic Algebraic Program."},{"key":"25_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-540-45187-7_12","volume-title":"CONCUR 2003 - Concurrency Theory","author":"N Lynch","year":"2003","unstructured":"Lynch, N.: Input\/output automata: basic, timed, hybrid, probabilistic, dynamic, In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 191\u2013192. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45187-7_12"},{"key":"25_CR34","unstructured":"Lyyra, A.K., Koskinen, K.M.: With software updates, Tesla upends product life cycle in the car industry. LSE Bus. Rev. (2017)"},{"key":"25_CR35","first-page":"129","volume":"34","author":"EF Moore","year":"1956","unstructured":"Moore, E.F., et al.: Gedanken-experiments on sequential machines. Automata Stud. 34, 129\u2013153 (1956)","journal-title":"Automata Stud."},{"key":"25_CR36","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53, 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"25_CR37","doi-asserted-by":"publisher","unstructured":"Palin, R., Ward, D., Habli, I., Rivett, R.: ISO 26262 safety cases: Compliance and assurance, vol. 2011, September 2011. https:\/\/doi.org\/10.1049\/cp.2011.0251","DOI":"10.1049\/cp.2011.0251"},{"key":"25_CR38","doi-asserted-by":"publisher","unstructured":"Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes, 25, 206\u2013230 (1987). https:\/\/doi.org\/10.1007\/BFb0006306","DOI":"10.1007\/BFb0006306"},{"key":"25_CR39","volume-title":"Artificial Intelligence: A Modern Approach","author":"S Russell","year":"2010","unstructured":"Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 3rd edn. Prentice Hall, Upper Saddle River (2010)","edition":"3"},{"key":"25_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-17245-8_8","volume-title":"Architecting Dependable Systems VII","author":"F Salfner","year":"2010","unstructured":"Salfner, F., Malek, M.: Architecting dependable systems with proactive fault management. In: Casimiro, A., de Lemos, R., Gacek, C. (eds.) WADS 2009. LNCS, vol. 6420, pp. 171\u2013200. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17245-8_8"},{"issue":"4","key":"25_CR41","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1145\/357401.357402","volume":"2","author":"JH Saltzer","year":"1984","unstructured":"Saltzer, J.H., Reed, D.P., Clark, D.D.: End-to-end arguments in system design. ACM Trans. Comput. Syst. 2(4), 277\u201388 (1984). https:\/\/doi.org\/10.1145\/357401.357402","journal-title":"ACM Trans. Comput. Syst."},{"issue":"4","key":"25_CR42","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1145\/98163.98167","volume":"22","author":"FB Schneider","year":"1990","unstructured":"Schneider, F.B.: Implementing fault-tolerant services using the state machine approach: a tutorial. ACM Comput. Surv. (CSUR) 22(4), 299\u2013319 (1990)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"25_CR43","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-319-66167-4_14","volume-title":"Frontiers of Combining Systems","author":"M Voigt","year":"2017","unstructured":"Voigt, M.: The Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey fragment with bounded difference constraints over the reals is decidable. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 244\u2013261. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_14"},{"key":"25_CR44","unstructured":"Wu, W., Kelly, T.: Safety tactics for software architecture design. In: Proceedings of the 28th Annual International Computer Software and Applications Conference 2004, COMPSAC 2004, vol. 1, pp. 368\u2013375 (2004)"},{"issue":"1","key":"25_CR45","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1016\/0022-247X(65)90154-X","volume":"10","author":"K \u00c5str\u00f6m","year":"1965","unstructured":"\u00c5str\u00f6m, K.: Optimal control of Markov processes with incomplete state information. J. Math. Anal. Appl. 10(1), 174\u2013205 (1965). https:\/\/doi.org\/10.1016\/0022-247X(65)90154-X","journal-title":"J. Math. Anal. Appl."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61470-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,24]],"date-time":"2022-11-24T20:40:12Z","timestamp":1669322412000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61470-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030614690","9783030614706"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61470-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"27 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}