{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:25:47Z","timestamp":1725488747824},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421245"},{"type":"electronic","value":"9783540451396"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45139-0_19","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T14:39:56Z","timestamp":1186756796000},"page":"296-303","source":"Crossref","is-referenced-by-count":4,"title":["Applications of model checking at honeywell laboratories"],"prefix":"10.1007","author":[{"given":"Darren","family":"Cofer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric","family":"Engstrom","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Goldman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Musliner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Vestal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,5,2]]},"reference":[{"key":"19_CR1","unstructured":"P. Binns. Scheduling Slack in MetaH. Real-Time Systems Symposium, December 1996."},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"P. Binns. Incremental Rate Monotonic Scheduling for Improved Control System Performance. Real-Time Applications Symposium, 1997.","DOI":"10.1109\/RTTAS.1997.601346"},{"key":"19_CR3","unstructured":"P. Binns. Design Document for Slack Scheduling in DEOS. Honeywell Technology Center Technical Report SST-R98-009, September 1998."},{"key":"19_CR4","unstructured":"T. Henzinger, P. Ho, H. Wong-Toi. A User Guide to HyTech. University of California at Berkeley, \n                    http:\/\/www.eecs.berkeley.edu\/~tah\/HyTech\n                    \n                  ."},{"key":"19_CR5","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann. The SPIN Model Checker. IEEE Transactions on Software Engineering, vol. 23, no. 5, May 1997, pp. 279\u2013295.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"D. Musliner, E. Durfee, and K. Shin. CIRCA: a cooperative intelligent real-time control architecture. IEEE Transactions on Systems, Man and Cybernetics 23(6):1561\u20131574.","DOI":"10.1109\/21.257754"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"J. Penix, W. Visser, E. Engstrom, A. Larson, and N. Weininger. Verification of time partitioning in the DEOS scheduler kernel. ICSE 2000.","DOI":"10.1145\/337180.337364"},{"key":"19_CR8","unstructured":"S. Vestal. An architectural approach for integrating real-time systems. Workshop on Languages, Compilers and Tools for Real-Time Systems, June 1997."},{"key":"19_CR9","unstructured":"S. Vestal. Modeling and verification of real-time software using extended linear hybrid automata. Fifth NASA Langley Formal Methods Workshop, June 2000 (see \n                    http:\/\/atb-www.larc.nasa.gov\/fm\/Lfm2000\/\n                    \n                  )."},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"N. Weininger, D. Cofer. Modeling the ASCB-D Synchronization Algorithm with Spin: A Case Study. 7th International Spin Workshop, September 2000.","DOI":"10.1007\/10722468_6"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"S. Yovine. Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer, vol. 1, no. 1\/2, Oct. 1997.","DOI":"10.1007\/s100090050009"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45139-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,21]],"date-time":"2019-02-21T06:49:46Z","timestamp":1550731786000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45139-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421245","9783540451396"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-45139-0_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}