{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:38:46Z","timestamp":1694623126991},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2004,5,1]],"date-time":"2004-05-01T00:00:00Z","timestamp":1083369600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2004,5]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>We apply both model checking and logical reasoning to a real-time protocol for mutual exclusion. To this end we employ PLC-Automata, an abstract notion of programs for real-time systems. A logic-based semantics in terms of Duration Calculus is used to verify the correctness of the protocol by logical reasoning. An alternative but consistent operational semantics in terms of Timed Automata is used to verify the correctness by model checkers. Since model checking of the full model does not terminate in all cases within an acceptable time we examine abstractions and their influence on model-checking performance. We present two abstraction methods that can be applied successfully for the protocol presented.<\/jats:p>","DOI":"10.1007\/s00165-004-0034-9","type":"journal-article","created":{"date-parts":[[2004,4,27]],"date-time":"2004-04-27T06:58:17Z","timestamp":1083049097000},"page":"104-120","source":"Crossref","is-referenced-by-count":20,"title":["Comparing model checking and logical reasoning for real-time systems"],"prefix":"10.1145","volume":"16","author":[{"given":"Henning","family":"Dierks","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oldenburg, 2503, 26111, Oldenburg, Germany"}]}],"member":"320","reference":[{"key":"p_1","first-page":"414","volume-title":"Fifth annual IEEE symposium on logic in computer science","author":"Alur R","year":"1990"},{"issue":"1","key":"p_2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","article-title":"Model-checking in dense real-time","volume":"104","author":"Alur R","year":"1993","journal-title":"Inform Comput"},{"key":"p_3","first-page":"322","volume-title":"Paterson MS (ed) ICALP 90: automata, languages, and programming, vol 443 of lecture notes in computer science","author":"Alur R","year":"1990"},{"key":"p_4","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur R","year":"1994","journal-title":"Theor Comput Sci"},{"key":"p_5","volume-title":"Hybrid systems III-verification and control, vol 1066 of lecture notes in computer science","author":"Alur R","year":"1996"},{"key":"p_6","first-page":"232","volume-title":"A tool suite for automatic verification of real-time systems. In: [AHS96]","author":"Bengtsson J","year":"1996"},{"key":"p_7","first-page":"29","volume-title":"Operational and logical semantics for polling real-time systems. In: [RR98]","author":"Dierks H","year":"1998"},{"key":"p_9","first-page":"111","volume-title":"Bertran M, Rus T (eds) ARTS'97, vol 1231 of lecture notes in computer science, Mallorca, Spain","author":"Die H","year":"1997"},{"key":"p_11","first-page":"208","volume-title":"The tool kronos. In: [AHS96]","author":"Daws C","year":"1996"},{"key":"p_12","first-page":"222","volume-title":"Proceedings of the 10th euromicro workshop on real time systems, IEEE computer society","author":"Dierks H","year":"1998"},{"key":"p_13","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","article-title":"Symbolic model checking for real-time systems","volume":"111","author":"Henzinger T","year":"1994","journal-title":"Inform Comput"},{"key":"p_14","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/BF01211086","article-title":"Duration calculus: logical foundations","volume":"9","author":"Hansen MR","year":"1997","journal-title":"Formal Aspects Comput"},{"key":"p_15","first-page":"357","volume-title":"BMBF","author":"Krieg-Br\u00fcckner B","year":"1996"},{"issue":"1","key":"p_16","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"Uppaal in a nutshell","volume":"1","author":"Larsen KG","year":"1997","journal-title":"Int J Softw Tools Tech Trans"},{"issue":"1","key":"p_17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1996.0060","article-title":"Forward and backward simulations part II: timing-based systems","volume":"128","author":"Lynch N","year":"1996","journal-title":"Inform Comput"},{"issue":"2","key":"p_18","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","article-title":"A temporal logic for multilevel reasoning about hardware","volume":"18","author":"Mos B","year":"1985","journal-title":"IEEE Comput"},{"key":"p_19","first-page":"189","volume-title":"Proceedings CHARME'95","author":"Maler O","year":"1995"},{"key":"p_20","volume-title":"Proceedings 7th conference on computer-based systems and software engineering. IEEE Press","author":"Maler O","year":"1996"},{"issue":"9","key":"p_21","doi-asserted-by":"crossref","first-page":"794","DOI":"10.1109\/32.159837","article-title":"Compiling real-time specifications into extended automata","volume":"18","author":"Nicollin X","year":"1992","journal-title":"IEEE Trans Software Eng"},{"key":"p_22","volume-title":"Lyngby, Denmark","author":"Ravn AP","year":"1998"},{"key":"p_23","first-page":"311","volume-title":"MOBY\/PLC - graphical development of PLC-automata. In: [RR98]","author":"Tapken J","year":"1998"},{"issue":"1","key":"p_24","first-page":"123","article-title":"Kronos: a verification tool for real-time systems","volume":"1","author":"Yov S","year":"1997","journal-title":"Int J Softw Tools Tech Trans"},{"key":"p_25","first-page":"256","volume-title":"Bj\u00f8rner D, Broy M, Pottosin IV (eds) Formal methods in programming and their application, vol 735 of lecture notes in computer science","author":"Zho C","year":"1993"},{"issue":"5","key":"p_26","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","article-title":"A calculus of durations","volume":"40","author":"Zhou C","year":"1991","journal-title":"Inform Proc Lett"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-004-0034-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0034-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0034-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:34:45Z","timestamp":1641483285000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0034-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,5]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2004,5]]}},"alternative-id":["10.1007\/s00165-004-0034-9"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0034-9","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,5]]}}}