{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:40:06Z","timestamp":1750189206237,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662545799"},{"type":"electronic","value":"9783662545805"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54580-5_10","type":"book-chapter","created":{"date-parts":[[2017,3,30]],"date-time":"2017-03-30T06:50:09Z","timestamp":1490856609000},"page":"169-187","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults"],"prefix":"10.1007","author":[{"given":"Guy","family":"Avni","sequence":"first","affiliation":[]},{"given":"Shubham","family":"Goel","sequence":"additional","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Guillermo","family":"Rodriguez-Navas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-22944-2_28","volume-title":"Algebra and Coalgebra in Computer Science","author":"M AlTurki","year":"2011","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386\u2013392. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22944-2_28"},{"key":"10_CR2","unstructured":"Avni, G., Goel, S., Henzinger, T.A., Rodriguez-Navas, G.: Computing scores of forwarding schemes in switched networks with probabilistic faults. coRR, abs\/0902.0885 (2017). http:\/\/arxiv.org\/abs\/1701.03519"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Avni, G., Guha, S., Rodriguez-Navas, G.: Synthesizing time-triggered schedules for switched networks with faulty links. In: Proceedings of the 16th IEEE\/ACM International Conference on Embedded Software (2016)","DOI":"10.1145\/2968478.2968499"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-662-48057-1_7","volume-title":"Mathematical Foundations of Computer Science 2015","author":"G Avni","year":"2015","unstructured":"Avni, G., Kupferman, O.: Stochastization of weighted automata. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 89\u2013102. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-48057-1_7"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bauer, G., Kopetz, H.: Transparent redundancy in the time-triggered architecture. In: Proceedings International Conference on Dependable Systems and Networks, DSN, pp. 5\u201313. IEEE (2000)","DOI":"10.1109\/ICDSN.2000.857508"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., Vardi, M.Y.: Distribution-aware sampling and weighted model counting for SAT. In: Proceedings of the 28th Conference on Artificial Intelligence, pp. 1722\u20131730 (2014)","DOI":"10.1609\/aaai.v28i1.8990"},{"key":"10_CR7","unstructured":"Chakraborty, S., Fried, D., Meel, K.S., Vardi, M.Y.: From weighted to unweighted model counting. In: Proceedings of the 31th International Joint Conference on Artificial Intelligence, pp. 689\u2013695 (2015)"},{"key":"10_CR8","unstructured":"Chiesa, M., Gurtov, A.V., Madry, A., Mitrovic, S., Nikolaevskiy, I., Schapira, M., Shenker, S.: On the resiliency of randomized routing against multiple edge failures. In: 43rd International Colloquium on Automata, Languages, and Programming, pp. 134:1\u2013134:15 (2016)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-662-46681-0_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Chistikov","year":"2015","unstructured":"Chistikov, D., Dimitrova, R., Majumdar, R.: Approximate counting in SMT and value estimation for probabilistic programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 320\u2013334. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_26"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"10_CR11","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1109\/TII.2005.875508","volume":"2","author":"J Ferreira","year":"2006","unstructured":"Ferreira, J., Almeida, L., Fonseca, A., Pedreiras, P., Martins, E., Rodriguez-Navas, G., Rigo, J., Proenza, J.: Combining operational flexibility and dependability in FTT-CAN. IEEE Trans. Industr. Inf. 2(2), 95\u2013102 (2006)","journal-title":"IEEE Trans. Industr. Inf."},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Guti\u00c8rrez, M., Steiner, W., Dobrin, R., Punnekkat, S.: A configuration agent based on the time-triggered paradigm for real-time networks. In: 2015 IEEE World Conference on Factory Communication Systems (WFCS), pp. 1\u20134, May 2015","DOI":"10.1109\/WFCS.2015.7160584"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Hagberg, A.A., Schult, D.A., Swart, P.J.: Exploring network structure, dynamics, and function using NetworkX. In: Proceedings of the 7th Python in Science Conference (SciPy 2008), Pasadena, CA, USA, pp. 11\u201315, August 2008","DOI":"10.25080\/TCWV9851"},{"key":"10_CR14","unstructured":"Harks, T., Peis, B., Schmand, D., Koch, L.V.: Competitive packet routing with priority lists. In: 41st International Symposium on Mathematical Foundations of Computer Science, pp. 49:1\u201349:14 (2016)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/978-3-642-28756-5_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking \u2013 PLASMA. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 498\u2013503. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-28756-5_37"},{"key":"10_CR16","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(86)90174-X","volume":"43","author":"M Jerrum","year":"1986","unstructured":"Jerrum, M., Valiant, L.G., Vazirani, V.V.: Random generation of combinatorial structures from a uniform distribution. Theor. Comput. Sci. 43, 169\u2013188 (1986)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10_CR17","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/JPROC.2014.2371999","volume":"103","author":"D Kreutz","year":"2015","unstructured":"Kreutz, D., Ramos, F.M.V., Ver\u00edssimo, P.E., Rothenberg, C.E., Azodolmolky, S., Uhlig, S.: Software-defined networking: a comprehensive survey. Proc. IEEE 103(1), 14\u201376 (2015)","journal-title":"Proc. IEEE"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22110-1_47"},{"issue":"1\u20132","key":"10_CR19","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. STTT 1(1\u20132), 134\u2013152 (1997)","journal-title":"STTT"},{"key":"10_CR20","unstructured":"Liu, V., Halperin, D., Krishnamurthy, A., Anderson, T.: F10: a fault-tolerant engineered network. Presented as Part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2013), pp. 399\u2013412 (2013)"},{"key":"10_CR21","unstructured":"Meel, K.S., Vardi, M.Y., Chakraborty, S., Fremont, D.J., Seshia, S.A., Fried, D., Ivrii, A., Malik, S.: Constrained sampling and counting: universal hashing meets SAT solving. In: Beyond NP, Papers from the 2016 AAAI Workshop (2016)"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Pozo, F., Rodriguez-Navas, G., Hansson, H., Steiner, W.: SMT-based synthesis of TTEthernet schedules: a performance study. In: 2015 10th IEEE International Symposium on Industrial Embedded Systems (SIES), pp. 1\u20134. IEEE (2015)","DOI":"10.1109\/SIES.2015.7185055"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Pozo, F., Steiner, W., Rodriguez-Navas, G., Hansson, H.: A decomposition approach for SMT-based synthesis for time-triggered networks. In: IEEE 20th Conference on Emerging Technologies and Factory Automation (ETFA), pp. 1\u20138. IEEE (2015)","DOI":"10.1109\/ETFA.2015.7301436"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Reitblatt, M., Canini, M., Guha, A., Foster, N.: FatTire: declarative fault tolerance for software-defined networks. In: Proceedings of the Second ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking, pp. 109\u2013114 (2013)","DOI":"10.1145\/2491185.2491187"},{"key":"10_CR25","volume-title":"Simulation and the Monte Carlo Method","author":"RY Rubinstein","year":"2011","unstructured":"Rubinstein, R.Y., Kroese, D.P.: Simulation and the Monte Carlo Method, vol. 707. Wiley, Hoboken (2011)"},{"issue":"1","key":"10_CR26","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1109\/LES.2013.2243698","volume":"5","author":"S Shreejith","year":"2013","unstructured":"Shreejith, S., Fahmy, S.A., Lukasiewycz, M.: Reconfigurable computing in next-generation automotive networks. IEEE Embed. Syst. Lett. 5(1), 12\u201315 (2013)","journal-title":"IEEE Embed. Syst. Lett."},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Steiner, W.: An evaluation of SMT-based schedule synthesis for time-triggered multi-hop networks. In: IEEE 31st Real-Time Systems Symposium (RTSS), pp. 375\u2013384. IEEE (2010)","DOI":"10.1109\/RTSS.2010.25"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Steiner, W., Bonomi, F., Kopetz, H.: Towards synchronous deterministic channels for the internet of things. In: IEEE World Forum on Internet of Things (WF-IoT), pp. 433\u2013436. IEEE (2014)","DOI":"10.1109\/WF-IoT.2014.6803205"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11814948_38","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"M Thurley","year":"2006","unstructured":"Thurley, M.: sharpSAT \u2013 counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424\u2013429. Springer, Heidelberg (2006). doi:10.1007\/11814948_38"},{"issue":"1","key":"10_CR30","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1109\/TII.2012.2198662","volume":"9","author":"MG Valls","year":"2013","unstructured":"Valls, M.G., Lopez, I.R., Villar, L.F.: iLAND: an enhanced middleware for real-time reconfiguration of service oriented distributed real-time systems. IEEE Trans. Industr. Inf. 9(1), 228\u2013236 (2013)","journal-title":"IEEE Trans. Industr. Inf."},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: 26th Annual Symposium on Foundations of Computer Science, Portland, pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Wei, Y., Kim, D.-S.: Exploiting real-time switched ethernet for enhanced network recovery scheme in naval combat system. In: International Conference on Information and Communication Technology Convergence (ICTC), pp. 595\u2013600. IEEE (2014)","DOI":"10.1109\/ICTC.2014.6983220"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Yang, B., Liu, J., Shenker, S., Li, J., Zheng, K.: Keep forwarding: towards k-link failure resilient routing. In: 2014 IEEE Conference on Computer Communications, pp. 1617\u20131625 (2014)","DOI":"10.1109\/INFOCOM.2014.6848098"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54580-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:27:04Z","timestamp":1750188424000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54580-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662545799","9783662545805"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54580-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"31 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}