{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T15:28:29Z","timestamp":1694618909950},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2000,10,1]],"date-time":"2000-10-01T00:00:00Z","timestamp":970358400000},"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":[[2000,10]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>A dense temporal logic development method for the specification, refinement, composition and verification of reactive systems is introduced. A reactive system is specified by a pair consisting of a machine and a condition that indicate the valid computations of this machine. Compositionality is achieved by indicating whether each step is an environment step, a system step, or a communication step. Refinement can be expressed straightforwardly in the logic because the stutter problem is elegantly solved by using the dense structure of the logic. Compositionality enables us to break refinement between complex systems into refinement between small and simple systems. The latter can then be verified by existing proof rules for refinement which are reformulated in our formalism.<\/jats:p>","DOI":"10.1007\/s001650070036","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T06:34:23Z","timestamp":1030257263000},"page":"52-70","source":"Crossref","is-referenced-by-count":1,"title":["Composing and Refining Dense Temporal Logic Specifications"],"prefix":"10.1145","volume":"12","author":[{"given":"Antonio","family":"Cau","sequence":"first","affiliation":[{"name":"Software Technology Research Laboratory, Science and Engineering Research Centre, De Montfort University, Leicester, UK, , , , , , GB"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"On an inference rule for parallel composition","author":"Acz","year":"1983"},{"issue":"2","key":"p_2","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":"Al","year":"1994","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"p_3","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","article-title":"The existence of refinement mappings","volume":"82","author":"Ab","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"p_4","first-page":"1","volume-title":"J.W. de Bakker, C. Huizing, W.-P","author":"Ab","year":"1991"},{"issue":"1","key":"p_5","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1145\/151646.151649","article-title":"Composing specifications","volume":"15","author":"Ab","year":"1993","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"p_6","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","article-title":"Defining liveness","volume":"21","author":"Al","year":"1985","journal-title":"Information Processing Letters"},{"key":"p_7","first-page":"131","volume-title":"Proceedings of the Second Symposium on Logic in Computer Science","author":"Al","year":"1987"},{"issue":"4","key":"p_8","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/BF01872848","article-title":"Appraising fairness in languages for distributed programming","volume":"2","author":"Apt K. R.","year":"1988","journal-title":"Distributed Computing"},{"key":"p_9","first-page":"51","volume-title":"Proceedings of 16th ACM Symposium on Theory of Computing","author":"Barringer H.","year":"1984"},{"key":"p_10","first-page":"173","volume-title":"Proc. 13th ACM Symposium on the Principles of Programming Languages","author":"Barringer H.","year":"1986"},{"issue":"4","key":"p_11","first-page":"367","article-title":"Axioms for tense logic, I. \u2018Since\u2019 and \u2018Until\u2019","volume":"23","author":"Bur","year":"1982","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"p_12","first-page":"89","volume-title":"Handbook of Philosophical Logic","author":"Bur","year":"1984"},{"issue":"2","key":"p_14","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/s002360050039","article-title":"Parallel composition of assumption-commitment specifications: a unifying approach for shared variable and distributed message passing concurrency","volume":"33","author":"Ca","year":"1996","journal-title":"Acta Informatica"},{"key":"p_15","volume-title":"Trace theory for automatic hierarchical verification of speed-independent circuits. ACM Distinguished Dissertations","author":"Dil","year":"1988"},{"key":"p_16","first-page":"208","volume-title":"LNCS 430: Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness","author":"Di","year":"1990"},{"issue":"3","key":"p_17","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/BF01212304","article-title":"Temporal theories as modularisation units for concurrent system specification","volume":"4","author":"Fi","year":"1992","journal-title":"Formal Aspects of Computing"},{"key":"p_18","first-page":"48","volume-title":"Proceedings of 1st International Conference on Temporal Logic","author":"Fi","year":"1994"},{"key":"p_19","volume-title":"Proceedings of ICALP 21","author":"Gawlick R.","year":"1994"},{"key":"p_20","volume-title":": Communicating sequential processes","author":"Hoa","year":"1984"},{"issue":"4","key":"p_21","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","article-title":"Tentative steps towards a development method for interfering programs","volume":"5","author":"Jon","year":"1983","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"p_22","first-page":"273","volume-title":"J.W. de Bakker, W.-P","author":"Kesten Y.","year":"1993"},{"key":"p_23","first-page":"657","volume-title":"Information Processing 83: Proceedings of the IFIP 9th World Congress","author":"Lam","year":"1983"},{"issue":"3","key":"p_24","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The temporal logic of actions","volume":"16","author":"Lam","year":"1994","journal-title":"ACM TOPLAS"},{"issue":"2","key":"p_25","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1006\/inco.1995.1134","article-title":"Forward and backward simulations - Part II: Timing-based systems","volume":"121","author":"Ly","year":"1995","journal-title":"Information and Computation"},{"issue":"4","key":"p_26","first-page":"417","article-title":"Proofs of networks of processes","volume":"7","author":"Mi","year":"1981","journal-title":"IEEE Transactions on Software Engineering"},{"key":"p_28","first-page":"342","volume-title":"5th Refinement Workshop, Workshops in Computing","author":"Cd","year":"1992"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650070036.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650070036\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650070036","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:30:56Z","timestamp":1641483056000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650070036"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,10]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,10]]}},"alternative-id":["10.1007\/s001650070036"],"URL":"https:\/\/doi.org\/10.1007\/s001650070036","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,10]]}}}