{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T05:00:35Z","timestamp":1648616435071},"reference-count":7,"publisher":"World Scientific Pub Co Pte Lt","issue":"04","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2006,8]]},"abstract":"<jats:p> Though model checking itself is a fully automated process, verifying correctness of a hybrid system design using model checking is not. This paper describes the necessary steps, and choices to be made, to go from an informal description of the problem to the final verification result for a formal model and requirement. It uses an automotive control system for illustration. <\/jats:p>","DOI":"10.1142\/s0129054106004169","type":"journal-article","created":{"date-parts":[[2006,8,4]],"date-time":"2006-08-04T18:37:04Z","timestamp":1154716624000},"page":"885-901","source":"Crossref","is-referenced-by-count":1,"title":["HYBRID SYSTEM VERIFICATION IS NOT A SINECURE \u2014 THE ELECTRONIC THROTTLE CONTROL CASE STUDY"],"prefix":"10.1142","volume":"17","author":[{"given":"ANSGAR","family":"FEHNKER","sequence":"first","affiliation":[{"name":"National ICT Australia (National ICT Australia is funded through the Australian Government's Backing Australia's Ability initiative, in part through the Australian Research Council.) and University of New South Wales, Sydney, NSW 2052, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"BRUCE","family":"KROGH","sequence":"additional","affiliation":[{"name":"Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA 15213, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"reference":[{"key":"rf1","volume":"109","author":"Agrawal A.","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"rf3","volume-title":"Model Checking","author":"Clarke E. M.","year":"2000"},{"key":"rf10","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1109\/9.664156"},{"key":"rf14","series-title":"LNCIS","volume-title":"Modelling, Analysis and Design of Hybrid Systems","volume":"279","author":"Huuck R.","year":"2002"},{"key":"rf15","volume-title":"Computer-Aided Control System Design","author":"Kapinski J.","year":"2002"},{"key":"rf22","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1109\/TAC.1977.1101446","volume":"22","author":"Utkin V.","journal-title":"IEEE Transactions on Automatic Control"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054106004169","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T20:40:31Z","timestamp":1565124031000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054106004169"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,8]]},"references-count":7,"journal-issue":{"issue":"04","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[2006,8]]}},"alternative-id":["10.1142\/S0129054106004169"],"URL":"https:\/\/doi.org\/10.1142\/s0129054106004169","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,8]]}}}