{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:50:25Z","timestamp":1742388625516,"version":"3.32.0"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T00:00:00Z","timestamp":1153958400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2006,11]]},"DOI":"10.1007\/s10009-006-0025-7","type":"journal-article","created":{"date-parts":[[2006,7,26]],"date-time":"2006-07-26T12:28:01Z","timestamp":1153916881000},"page":"633-647","source":"Crossref","is-referenced-by-count":13,"title":["Model checker aided design of a controller for a wafer scanner"],"prefix":"10.1007","volume":"8","author":[{"given":"Martijn","family":"Hendriks","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barend","family":"van den Nieuwelaar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,7,27]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur R., Courcoubetis C., Dill D.L. (1993). Model checking in dense real time. Inform. Comput. 104: 2\u201334","journal-title":"Inform. Comput."},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: ICALP\u201990, pp. 322\u2013335 (1990)","DOI":"10.1007\/BFb0032042"},{"key":"25_CR3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur R., Dill D.L. (1994). A theory of timed automata. Theor. Comput. Sci. 126: 183\u2013235","journal-title":"Theor. Comput. Sci."},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Brinksma, E., Hendriks, M., Mader, A.: Scheduling lacquer production by reachability analysis \u2013 a case study. In: Workshop on parallel and distributed real-time systems 2005. IEEE Computer Society Press (2005, to appear)","DOI":"10.3182\/20050703-6-CZ-1902.01433"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: SFM\u201904, LNCS, vol. 3185, pp. 200\u2013236. Springer, Berlin Heidelberg New York (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Bohnenkamp, H.C., Hermanns, H., Klaren, R., Mader, A., Usenko, Y.S.: Synthesis and stochastic assessment of schedules for lacquer production. In: Proceedings of 1st international conference on quantitative evaluation of systems (QEST 2004), 27-30 September 2004, Enschede, pp. 28\u201337. IEEE Computer Society (2004)","DOI":"10.1109\/QEST.2004.1348013"},{"key":"25_CR7","unstructured":"Braspenning, N.C.W.M.: Scheduling and behavior verification of machines based on task-resource models. Master\u2019s thesis, Department of Mechanical Engineering, Eindhoven University of Technology, The Netherlands (2003)"},{"issue":"1,2","key":"25_CR8","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"Browne M.C., Clarke E.M., Grumberg O. (1988). Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59(1,2): 115\u2013131","journal-title":"Theor. Comput. Sci."},{"issue":"8","key":"25_CR9","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant R.E. (1986). Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8): 677\u2013691","journal-title":"IEEE Trans. Comput. C-"},{"key":"25_CR10","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke E.M., Grumberg O., Peled D.A. (2000). Model Checking. The MIT Press, Cambridge"},{"key":"25_CR11","volume-title":"Cooperating sequential processes","author":"E.W. Dijkstra","year":"1965","unstructured":"Dijkstra E.W. (1965). Cooperating sequential processes. Technical report. Eindhoven University of Technology, The Netherlands"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Fehnker, A.: Scheduling a steel plant with timed automata. In: RTCSA\u201999. IEEE Computer Society Press (1999)","DOI":"10.1109\/RTCSA.1999.811256"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Gebremichael, B., Vaandrager, F.W.: Control synthesis for a smart card personalization system using symbolic model checking. In: Larsen, K.G., Niebert P. (eds) FORMATS\u201903, no. 2791 in LNCS, pp. 189\u2013203. Springer, Berlin Heidelberg New York (2004)","DOI":"10.1007\/978-3-540-40903-8_16"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Hartonas-Garmhausen, V., Clarke, E.M., Campos, S.: Deadlock prevention in flexible manufacturing systems using symbolic model checking. In: IEEE conference on robotics and automation. vol. 1, pp. 527\u2013532 (1996)","DOI":"10.1109\/ROBOT.1996.503829"},{"issue":"4","key":"25_CR15","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1023\/A:1012203214611","volume":"13","author":"M. Lawley","year":"2001","unstructured":"Lawley M., Reveliotis S.A. (2001). Deadlock avoidance for sequential resource allocation systems: hard and easy cases. Int. J. Flex. Manuf. Sys. 13(4): 385\u2013404","journal-title":"Int. J. Flex. Manuf. Sys."},{"issue":"1","key":"25_CR16","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1007937925728","volume":"9","author":"M. Lawley","year":"1997","unstructured":"Lawley M., Reveliotis S.A., Ferreira P. (1997). Design guidelines for deadlock handling strategies in flexible manufacturing systems. Int. J. Flex. Manuf. Sys. 9(1): 5\u201330","journal-title":"Int. J. Flex. Manuf. Sys."},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic model checking. Ph.D. thesis, Carnegie Mellon University (1992)","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"4","key":"25_CR18","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T. Murata","year":"1989","unstructured":"Murata T. (1989). Petri nets: properties, analysis, and applications. P. IEEE 77(4): 541\u2013580","journal-title":"P. IEEE"},{"key":"25_CR19","unstructured":"Niebert, P., Yovine, S.: Computing optimal operation schemes for chemical plants in multi-batch mode. In: HSCC, LNCS, vol. 1790, pp. 338\u2013351. Springer, Berlin Heidelberg New York, (2000)"},{"issue":"10","key":"25_CR20","doi-asserted-by":"crossref","first-page":"1572","DOI":"10.1109\/9.956052","volume":"46","author":"J. Park","year":"2001","unstructured":"Park J., Reveliotis S.A. (2001). Deadlock avoidance in sequential resource allocation systems with multiple resource acquisitions and flexible routings. IEEE T. Automat. Contr. 46(10): 1572\u20131583","journal-title":"IEEE T. Automat. Contr."},{"issue":"10","key":"25_CR21","doi-asserted-by":"crossref","first-page":"1344","DOI":"10.1109\/9.633824","volume":"42","author":"S.A. Reveliotis","year":"1997","unstructured":"Reveliotis S.A., Lawley M., Ferreira P. (1997). Polynomial-complexity deadlock avoidance policies for sequential resource allocation systems. IEEE T. Automat. Contr. 42(10): 1344\u20131357","journal-title":"IEEE T. Automat. Contr."},{"key":"25_CR22","unstructured":"Stallings, W.: Operating Systems. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Wang, Y., Wu, Z.: Deadlock avoidance control synthesis in manufacturing systems using model checking. In: IEEE American Control Conference, vol. 2, pp. 1702\u20131704 (2003)","DOI":"10.1109\/ACC.2003.1239839"},{"issue":"1\/2","key":"25_CR24","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine S. (1997). Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf. 1(1\/2): 123\u2013133","journal-title":"Int. J. Softw. Tools Technol. Transf."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0025-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-006-0025-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0025-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T02:44:32Z","timestamp":1736477072000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-006-0025-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7,27]]},"references-count":24,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2006,11]]}},"alternative-id":["25"],"URL":"https:\/\/doi.org\/10.1007\/s10009-006-0025-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2006,7,27]]}}}