{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:14:25Z","timestamp":1743124465808,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031150074"},{"type":"electronic","value":"9783031150081"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-15008-1_13","type":"book-chapter","created":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T23:02:47Z","timestamp":1662332567000},"page":"193-210","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formally Verifying Decompositions of\u00a0Stochastic Specifications"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3939-3919","authenticated-orcid":false,"given":"Anton","family":"Hampus","sequence":"first","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Mattias","family":"Nyberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,9,5]]},"reference":[{"key":"13_CR1","unstructured":"Linear optimization. https:\/\/online-optimizer.appspot.com. Accessed 27 May 2022"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1990","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322\u2013335. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032042"},{"issue":"2","key":"13_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269\u2013276. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_75"},{"issue":"1","key":"13_CR5","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic (TOCL) 1(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"issue":"2","key":"13_CR6","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.ic.2005.03.001","volume":"200","author":"C Baier","year":"2005","unstructured":"Baier, C., Katoen, J.P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149\u2013214 (2005)","journal-title":"Inf. Comput."},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-92188-2_9","volume-title":"Formal Methods for Components and Objects","author":"A Benveniste","year":"2008","unstructured":"Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 200\u2013225. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-92188-2_9"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Compositional design methodology with constraint Markov chains. In: 2010 Seventh International Conference on the Quantitative Evaluation of Systems, pp. 123\u2013132. IEEE (2010)","DOI":"10.1109\/QEST.2010.23"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/3-540-51237-3_7","volume-title":"Logic at Botik \u201989","author":"EM Clarke","year":"1989","unstructured":"Clarke, E.M., Grumberg, O., Kurshan, R.P.: A synthesis of two approaches for verifying finite state concurrent systems. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 81\u201390. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/3-540-51237-3_7"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Dantzig, G.B.: Origins of the simplex method. In: A History of Scientific Computing, pp. 141\u2013151 (1990)","DOI":"10.1145\/87252.88081"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I\/O automata: a complete specification theory for real-time systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 91\u2013100 (2010)","DOI":"10.1145\/1755952.1755967"},{"issue":"1","key":"13_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-010-0107-8","volume":"38","author":"B Delahaye","year":"2011","unstructured":"Delahaye, B., Caillaud, B., Legay, A.: Probabilistic contracts: a compositional reasoning methodology for the design of systems with stochastic and\/or non-deterministic aspects. Form. Methods Syst. Des. 38(1), 1\u201332 (2011)","journal-title":"Form. Methods Syst. Des."},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-18275-4_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Delahaye","year":"2011","unstructured":"Delahaye, B., et al.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324\u2013339. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_23"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL$$^\\wedge $$$$\\{\\rm TA\\}$$. IEEE Trans. Softw. Eng. 35(2), 224\u2013240 (2008)","DOI":"10.1109\/TSE.2008.108"},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/s10703-012-0162-4","volume":"41","author":"G G\u00f6ssler","year":"2012","unstructured":"G\u00f6ssler, G., Xu, D.N., Girault, A.: Probabilistic contracts for component-based design. Form. Methods Syst. Des. 41(2), 211\u2013231 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Grunske, L.: Specification patterns for probabilistic quality properties. In: 2008 ACM\/IEEE 30th International Conference on Software Engineering, pp. 31\u201340. IEEE (2008)","DOI":"10.1145\/1368088.1368094"},{"key":"13_CR18","unstructured":"Hampus, A., Nyberg, M.: Formally verifying decompositions of stochastic specifications (with proofs). Technical report (2022). http:\/\/urn.kb.se\/resolve?urn=urn:nbn:se:kth:diva-315290. oai:DiVA.org:kth-315290"},{"key":"13_CR19","unstructured":"ISO 21434: Road vehicles - Cybersecurity engineering (2021)"},{"key":"13_CR20","unstructured":"ISO 26262: Road vehicles - Functional safety (2018)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proceedings 1991 Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 266\u2013267. IEEE Computer Society (1991)","DOI":"10.1109\/LICS.1991.151651"},{"issue":"1","key":"13_CR22","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/S0304-3975(01)00044-5","volume":"282","author":"B Jonsson","year":"2002","unstructured":"Jonsson, B., Yi, W.: Testing preorders for probabilistic processes can be characterized by simulations. Theoret. Comput. Sci. 282(1), 33\u201351 (2002)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"13_CR23","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C Kern","year":"1999","unstructured":"Kern, C., Greenstreet, M.R.: Formal verification in hardware design: a survey. ACM Trans. Des. Autom. Electron. Syst. (TODAES) 4(2), 123\u2013193 (1999)","journal-title":"ACM Trans. Des. Autom. Electron. Syst. (TODAES)"},{"issue":"1","key":"13_CR24","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s00165-006-0015-2","volume":"19","author":"R Lanotte","year":"2007","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Formal Aspects Comput. 19(1), 93\u2013109 (2007)","journal-title":"Formal Aspects Comput."},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Mereacre, A., Katoen, J.P., Han, T., Chen, T.: Model checking of continuous-time Markov chains against timed automata specifications. Log. Methods Comput. Sci. 7 (2011)","DOI":"10.2168\/LMCS-7(1:12)2011"},{"issue":"10","key":"13_CR26","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u2018design by contract\u2019. Computer 25(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"13_CR27","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 de Moura","year":"2008","unstructured":"de 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). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"1","key":"13_CR28","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1109\/5992.814654","volume":"2","author":"JC Nash","year":"2000","unstructured":"Nash, J.C.: The (Dantzig) simplex method for linear programming. Comput. Sci. Eng. 2(1), 29\u201331 (2000)","journal-title":"Comput. Sci. Eng."},{"issue":"1","key":"13_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3243216","volume":"18","author":"P Nuzzo","year":"2019","unstructured":"Nuzzo, P., Li, J., Sangiovanni-Vincentelli, A.L., Xi, Y., Li, D.: Stochastic assume-guarantee contracts for cyber-physical system design. ACM Trans. Embed. Comput. Syst. (TECS) 18(1), 1\u201326 (2019)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-030-61467-6_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"M Nyberg","year":"2020","unstructured":"Nyberg, M., Westman, J., Gurov, D.: Formally proving compositionality in industrial systems with informal specifications. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 348\u2013365. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_22"},{"issue":"2","key":"13_CR31","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1109\/TSE.2015.2468717","volume":"42","author":"M Paolieri","year":"2015","unstructured":"Paolieri, M., Horv\u00e1th, A., Vicario, E.: Probabilistic model checking of regenerative concurrent systems. IEEE Trans. Software Eng. 42(2), 153\u2013169 (2015)","journal-title":"IEEE Trans. Software Eng."},{"key":"13_CR32","unstructured":"Resnick, S.: A Probability Path. Birkh\u00e4user Boston (2019)"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-49213-5_1","volume-title":"Compositionality: The Significant Difference","author":"W-P Roever","year":"1998","unstructured":"Roever, W.-P.: The need for compositional proof systems: a survey. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 1\u201322. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49213-5_1"},{"key":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-540-48654-1_35","volume-title":"CONCUR \u201994: Concurrency Theory","author":"R Segala","year":"1994","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481\u2013496. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/978-3-540-48654-1_35"},{"key":"13_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"issue":"1","key":"13_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"issue":"2","key":"13_CR37","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/s10703-017-0294-7","volume":"52","author":"J Westman","year":"2017","unstructured":"Westman, J., Nyberg, M.: Conditions of contracts for separating responsibilities in heterogeneous systems. Form. Methods Syst. Des. 52(2), 147\u2013192 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0294-7","journal-title":"Form. Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15008-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,3]],"date-time":"2024-10-03T05:51:21Z","timestamp":1727934681000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15008-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031150074","9783031150081"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15008-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"5 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Warsaw","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fmics2022.fsa.win.tue.nl\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"13","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"59% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2.5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}