{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T22:23:08Z","timestamp":1743027788338,"version":"3.40.3"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031661488"},{"type":"electronic","value":"9783031661495"}],"license":[{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-66149-5_5","type":"book-chapter","created":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:01:54Z","timestamp":1728716514000},"page":"87-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Two Decades of Industrializing Formal Verification: The Reactis Story"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4952-5380","authenticated-orcid":false,"given":"Rance","family":"Cleaveland","sequence":"first","affiliation":[]},{"given":"David","family":"Hansel","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Sims","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7348-630X","authenticated-orcid":false,"given":"Scott","family":"A. Smolka","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,13]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Ammann, P., Black, P., Majurski, W.: Using model checking to generate tests from specifications. In: Second International Conference on Formal Engineering Methods, pp. 46\u201354 (1998). https:\/\/doi.org\/10.1109\/ICFEM.1998.730569","key":"5_CR1","DOI":"10.1109\/ICFEM.1998.730569"},{"unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)","key":"5_CR2"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"issue":"1","key":"5_CR4","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1109\/JPROC.2002.805826","volume":"91","author":"A Benveniste","year":"2003","unstructured":"Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Le Guernic, P., De Simone, R.: The synchronous languages 12 years later. Proc. IEEE 91(1), 64\u201383 (2003)","journal-title":"Proc. IEEE"},{"unstructured":"Bergstra, J.A., Ponse, A., Smolka, S.A.: Handbook of Process Algebra. Elsevier (2001)","key":"5_CR5"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-46419-0_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bharadwaj","year":"2000","unstructured":"Bharadwaj, R., Sims, S.: Salsa: combining constraint solvers with BDDS for automatic invariant checking. In: Graf, S., Schwartzbach, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 378\u2013395. Springer, Berlin, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46419-0_26"},{"doi-asserted-by":"crossref","unstructured":"Bhat, G., Cleaveland, R., Grumberg, O.: Efficient on-the-fly model checking for CTL. In: 10th Annual IEEE Symposium on Logic in Computer Science. pp. 388\u2013397. IEEE (1995)","key":"5_CR7","DOI":"10.1109\/LICS.1995.523273"},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-61042-1_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Bhat","year":"1996","unstructured":"Bhat, G., Cleaveland, R.: Efficient local model-checking for fragments of the modal $$\\mu $$-calculus. In: Margaria, T., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 107\u2013126. Springer, Berlin, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61042-1_41"},{"issue":"5","key":"5_CR9","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1049\/sej.1994.0025","volume":"9","author":"J Chilenski","year":"1994","unstructured":"Chilenski, J., Miller, S.: Applicability of modified condition\/decision coverage to software testing. Softw. Eng. J. 9(5), 193\u2013200 (1994)","journal-title":"Softw. Eng. J."},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 93\u2013107. Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"issue":"2","key":"5_CR11","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R Cleaveland","year":"1990","unstructured":"Cleaveland, R.: Tableau-based model checking in the propositional $$\\mu $$-calculus. Acta Informatica 27, 725\u2013747 (1990)","journal-title":"Acta Informatica"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-60630-0_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Cleaveland","year":"1995","unstructured":"Cleaveland, R., Madelaine, E., Sims, S.: A front-end generator for verification tools. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 153\u2013173. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60630-0_8"},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1090\/dimacs\/018\/06","volume":"18","author":"R Cleaveland","year":"1994","unstructured":"Cleaveland, R., Gada, J.N., Lewis, P.M., Smolka, S.A., Sokolsky, O., Zhang, S.: The concurrency factory - practical tools for specification, stimulation, verification, and implementation of concurrent systems. Specif. Parallel Algorithms 18, 75\u201390 (1994)","journal-title":"Specif. Parallel Algorithms"},{"issue":"1","key":"5_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01211314","volume":"5","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Hennessy, M.: Testing equivalence as a bisimulation equivalence. Formal Aspects Comput. 5(1), 1\u201320 (1993). https:\/\/doi.org\/10.1007\/BF01211314","journal-title":"Formal Aspects Comput."},{"issue":"1","key":"5_CR16","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36\u201372 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"unstructured":"Cleaveland, R., Sims, S.T., Hansel, D.: System and method for automatic test-case generation for software, US Patent 7,644,398 (2010)","key":"5_CR17"},{"doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Sims, S.T.: Generic tools for verifying concurrent systems, special issue on engineering automation for computer based systems. Sci. Comput. Program. 42(1), 39\u201347 (2002)","key":"5_CR18","DOI":"10.1016\/S0167-6423(01)00033-8"},{"unstructured":"Cleaveland, R., Smolka, S.A., Lewis, P.M., Ramakrishna, Y.: Specification and verification for concurrent systems with graphical and textual editors, US Patent 6,385,765 (2002)","key":"5_CR19"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-70930-5_6","volume-title":"Model-Driven Development of Reliable Automotive Services","author":"R Cleaveland","year":"2008","unstructured":"Cleaveland, R., Smolka, S.A., Sims, S.T.: An instrumentation-based approach to controller model validation. In: Broy, M., Kr\u00fcger, I.H., Meisinger, M. (eds.) Model-Driven Development of Reliable Automotive Services, pp. 84\u201397. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70930-5_6"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal $$\\mu $$-calculus. Formal Methods Syst. Des. 2, 121\u2013147 (1993)","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR22","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s100090050031","volume":"2","author":"X Du","year":"1999","unstructured":"Du, X., Smolka, S.A., Cleaveland, R.: Local model checking and protocol analysis. Int. J. Softw. Tools Technol. Transf. 2, 219\u2013241 (1999)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"5_CR23","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/S0164-1212(03)00074-8","volume":"70","author":"D Hansel","year":"2004","unstructured":"Hansel, D., Cleaveland, R., Smolka, S.A.: Distributed prototyping from validated specifications. J. Syst. Softw. 70(3), 275\u2013298 (2004)","journal-title":"J. Syst. Softw."},{"issue":"3","key":"5_CR24","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/234426.234431","volume":"5","author":"C Heitmeyer","year":"1996","unstructured":"Heitmeyer, C., Jeffords, R., Labaw, B.: Automated consistency checking of requirements specifications. ACM Trans. Softw. Eng. Methodol. 5(3), 231\u2013261 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"doi-asserted-by":"crossref","unstructured":"Henzinger, M., Henzinger, T., Kopke, P.: Computing simulations on finite and infinite graphs. In: IEEE 36th Annual Foundations of Computer Science, pp. 453\u2013462. IEEE (1995)","key":"5_CR25","DOI":"10.1109\/SFCS.1995.492576"},{"doi-asserted-by":"crossref","unstructured":"Holzmann, G.: On-the-fly model checking. ACM Comput. Surv. (CSUR) 28(4es), 120\u2013es (1996)","key":"5_CR26","DOI":"10.1145\/242224.242379"},{"issue":"5","key":"5_CR27","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"unstructured":"ISO 26262: Road vehicles - functional safety (2011)","key":"5_CR28"},{"doi-asserted-by":"crossref","unstructured":"Kanellakis, P., Smolka, S.: CCS expressions, finite state processes, and three problems of equivalence. In: Second Annual ACM Symposium on Principles of Distributed Computing, pp. 228\u2013240 (1983)","key":"5_CR29","DOI":"10.1145\/800221.806724"},{"issue":"1","key":"5_CR30","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P Kanellakis","year":"1990","unstructured":"Kanellakis, P., Smolka, S.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43\u201368 (1990)","journal-title":"Inf. Comput."},{"doi-asserted-by":"publisher","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus, special issue ninth international colloquium on automata, languages and programming (ICALP), Aarhus, Summer 1982. Theor. Comput. Sci. 27(3), 333\u2013354 (1983).https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","key":"5_CR31","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BFb0054161","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"X Liu","year":"1998","unstructured":"Liu, X., Ramakrishnan, C.R., Smolka, S.A.: Fully local and efficient evaluation of alternating fixed points. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 5\u201319. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054161"},{"key":"5_CR33","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/bfb0055040","volume-title":"Automata, Languages and Programming","author":"X Liu","year":"1998","unstructured":"Liu, X., Smolka, S.: Simple linear-time algorithms for minimal fixed points. In: Automata, Languages and Programming, pp. 53\u201366. Springer, Berlin, Heidelberg (1998). https:\/\/doi.org\/10.1007\/bfb0055040"},{"key":"5_CR34","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-1-4471-3534-0_7","volume-title":"Specification and Verification of Concurrent Systems","author":"J Malhotra","year":"1990","unstructured":"Malhotra, J., Smolka, S., Giacalone, A., Shapiro, R.: Winston: a tool for hierarchical design and simulation of concurrent systems. In: Rattray, C. (ed.) Specification and Verification of Concurrent Systems, pp. 140\u2013152. Springer, London (1990). https:\/\/doi.org\/10.1007\/978-1-4471-3534-0_7"},{"key":"5_CR35","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs, New Jersey (1989)"},{"key":"5_CR36","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.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"unstructured":"Myers, G., Badgett, T., Thomas, T., Sandler, C.: The Art of Software Testing. Wiley, USA (2004)","key":"5_CR37"},{"unstructured":"National Instruments. https:\/\/www.ni.com\/en\/shop\/labview.html","key":"5_CR38"},{"unstructured":"The While House, Office of the National Cybersecurity Director: Back to the Building Blocks: A Path Towards Secure and Measurable Software (2024)","key":"5_CR39"},{"unstructured":"Parnas, D.: Tabular representation of relations. Technical report\u00a0260, Communications Research Laboratory, McMaster University (1992)","key":"5_CR40"},{"doi-asserted-by":"publisher","unstructured":"Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 143\u2013154. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_16","key":"5_CR41","DOI":"10.1007\/3-540-63166-6_16"},{"doi-asserted-by":"publisher","unstructured":"Rayadurgam, S., Heimdahl, M.: Coverage based test-case generation using model checkers. In: Eighth Annual IEEE International Conference and Workshop On the Engineering of Computer-Based Systems\u2013ECBS 2001, pp. 83\u201391 (2001). https:\/\/doi.org\/10.1109\/ECBS.2001.922409","key":"5_CR42","DOI":"10.1109\/ECBS.2001.922409"},{"unstructured":"Reactive Systems Inc.: https:\/\/reactive-systems.com\/","key":"5_CR43"},{"unstructured":"RTCA DO-178B (EUROCAE ED-12B), Software Considerations in Airborne Systems and Equipment Certification, 2nd Edition (1992)","key":"5_CR44"},{"unstructured":"RTCA DO-178C, Software Considerations in Airborne Systems and Equipment Certification (2011)","key":"5_CR45"},{"doi-asserted-by":"crossref","unstructured":"Sims, S., Cleaveland, R., Butts, K., Ranville, S.: Automated validation of software models. In: 16th Annual International Conference on Automated Software Engineering (ASE 2001), pp. 91\u201396. IEEE (2001)","key":"5_CR46","DOI":"10.1109\/ASE.2001.989794"},{"key":"5_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-58179-0_67","volume-title":"Computer Aided Verification","author":"OV Sokolsky","year":"1994","unstructured":"Sokolsky, O.V., Smolka, S.A.: Incremental model checking in the modal $$\\mu $$-calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 351\u2013363. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_67"},{"issue":"1","key":"5_CR48","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C Stirling","year":"1991","unstructured":"Stirling, C., Walker, D.: Local model checking in the modal $$\\mu $$-calculus. Theoret. Comput. Sci. 89(1), 161\u2013177 (1991)","journal-title":"Theoret. Comput. Sci."},{"unstructured":"Zhang, S., Sokolsky, O., Smolka, S.: On the parallel complexity of model checking in the modal $$\\mu $$-calculus. In: Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 154\u2013163. IEEE (1994)","key":"5_CR49"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66149-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:06:26Z","timestamp":1728716786000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66149-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,13]]},"ISBN":["9783031661488","9783031661495"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66149-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,13]]},"assertion":[{"value":"13 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}