{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:52:57Z","timestamp":1694623977028},"reference-count":23,"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>Linear temporal logic (LTL) has been widely used for specification and verification of reactive systems. Its standard model is sequences of states (or state transitions), and formulas describe sequencing of state transitions. When LTL is used to model real-time systems, a state is extended with a time stamp to record when a state transition takes place. Duration calculus (DC) is another well studied approach for real-time systems development. DC models behaviours of a system by functions from the domain of reals representing time to the system states. This paper extends this time domain to the Cartesian product of the real and the natural numbers. With the extended time domain, we provide the chop modality with a non-overlapping interpretation. This allows some linear temporal operators explicitly dealing with the discrete dimension of time to be derivable from the chop modality in essentially the same way that their continuous-time counterparts are in the classical DC. This provides a nice embedding of some timed LTL (TLTL) modalities into DC to unify the methods from DC and LTL for real-time systems development: Requirements and high level design decisions are interval properties and are therefore specified and reasoned about in DC, while properties of an implementation, as well as the refinement relation between two implementations, are specified and verified compositionally and inductively in LTL. Implementation properties are related to requirement and design properties by rules for lifting LTL formulas to DC formulas.<\/jats:p>","DOI":"10.1007\/s00165-004-0036-7","type":"journal-article","created":{"date-parts":[[2004,5,5]],"date-time":"2004-05-05T07:49:24Z","timestamp":1083743364000},"page":"140-154","source":"Crossref","is-referenced-by-count":4,"title":["Unifying proof methodologies of duration calculus and timed linear temporal logic"],"prefix":"10.1145","volume":"16","author":[{"given":"Zhiming","family":"Liu","sequence":"first","affiliation":[{"name":"International Institute for Software Technology, The United Nations University, 3058, Macau SAR, China"}]},{"given":"Anders P.","family":"Ravn","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University, Aalborg, Denmark"}]},{"given":"Xiaoshan","family":"Li","sequence":"additional","affiliation":[{"name":"Faculty of Science and Technology, University of Macau, Macau, China"}]}],"member":"320","reference":[{"key":"p_1","first-page":"390","volume-title":"Proceedings of the 5th annual symposium on logic in computer science. IEEE Computer Society","author":"Alur A","year":"1990"},{"issue":"2","key":"p_2","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","article-title":"The existence of refinement mapping","volume":"83","author":"Abadi M","year":"1991","journal-title":"Theor Comput Sci"},{"key":"p_3","first-page":"1","volume-title":"Huizing C, deRover WP, Rozenberg G (eds) Real-time: theory in practice. Lecture notes in computer science, vol 600","author":"Abadi M","year":"1992"},{"issue":"2","key":"p_4","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1006\/inco.1994.1060","article-title":"Temporal proof methodologies for timed transition systems","volume":"112","author":"Henzinger T","year":"1994","journal-title":"Inform Comput"},{"issue":"3","key":"p_5","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"},{"issue":"7","key":"p_6","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/360248.360251","article-title":"Formal verification of parallel programs","volume":"19","author":"Kel R","year":"1976","journal-title":"Commun ACM"},{"issue":"2","key":"p_8","first-page":"125","article-title":"Proving the correctness of multiprocess programs","volume":"3","author":"Lam L","year":"1977","journal-title":"IEEE Trans Softw Eng"},{"key":"p_9","first-page":"1","volume-title":"Grossman RL, Nerode A, Ravn AP, Rischel H (eds) Hybrid systems. Lecture notes in computer science, vol 736","author":"Lam L","year":"1993"},{"issue":"3","key":"p_10","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The temporal logic of actions","volume":"16","author":"Lam L","year":"1994","journal-title":"ACM Trans Program Lang Syst"},{"key":"p_11","first-page":"182","volume-title":"Joseph M (eds) Real-time systems: specification, verification and analysis","author":"Liu Z","year":"1996"},{"key":"p_13","first-page":"327","volume-title":"PROCOMET'98","author":"Liu Z","year":"1998"},{"key":"p_14","first-page":"215","volume-title":"Boyer RS, Moore JS (eds) The correctness problem in computer science","author":"Manna Z","year":"1981"},{"key":"p_15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems: specification","author":"Manna Z","year":"1992"},{"key":"p_16","first-page":"107","volume-title":"Heitmeyer C, Mandrioli D (eds) Formal methods in real-time systems, trends in software-engineering, chap 5","author":"Olderog E-R","year":"1996"},{"key":"p_17","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-50302-1_4","volume-title":"Joseph M (ed) Formal techniques in real-time and fault-tolerant systems. Lecture notes in computer science","author":"Pnueli A","year":"1988"},{"key":"p_18","first-page":"46","volume-title":"Proceeding of the 18th annual symposium on foundations of computer science","author":"Pnu A","year":"1977"},{"key":"p_19","volume-title":"Design of embedded real-time computing systems. Department of Computer Science","author":"Rav AP","year":"1995"},{"key":"p_20","first-page":"316","volume-title":"Rozenberg G, Vaandrager FW (eds) Embedded Systems. Lecture notes in computer science","author":"Ravn AP","year":"1998"},{"issue":"1","key":"p_21","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/32.210306","article-title":"Specifying and verifying requirements of real-time systems","volume":"19","author":"Ravn AP","year":"1993","journal-title":"IEEE Trans Softw Eng"},{"key":"p_22","first-page":"301","volume-title":"Maler O (ed) International workshop on hybrid and real-time systems. Lecture notes in computer science","author":"Xu QW","year":"1997"},{"key":"p_23","volume-title":"He JF, Cooke J, Wallis P (eds) Proceedings of the BCS FACS 7th Refinement Workshop: theory and practice of system design","author":"Zhou CC","year":"1996"},{"key":"p_24","first-page":"584","volume-title":"HansLangmaack Willem-Paulde Roever and Amir Pnueli (eds) Compositionality: the significant difference. Lecture notes in computer science","author":"Zhou CC","year":"1998"},{"issue":"5","key":"p_25","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 CC","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-0036-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-004-0036-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-004-0036-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:35:36Z","timestamp":1641483336000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-004-0036-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,5]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2004,5]]}},"alternative-id":["10.1007\/s00165-004-0036-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-004-0036-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,5]]}}}