{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T17:04:06Z","timestamp":1694624646026},"reference-count":15,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1989,3,1]],"date-time":"1989-03-01T00:00:00Z","timestamp":604713600000},"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":[[1989,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            This paper is about specification and verification of processes, modelled as CCS-agents. We show, by means of examples that Hennessy-Milner Logic (HML) with recursion is a suitable language for expressing implicit or partial specifications. By extending this specification language with\n            <jats:italic>refinement operators<\/jats:italic>\n            , i.e. operators that describe the internal structure of a system, we obtain a calculus for stepwise refinement of agents from a specification in HML to a realisation in CCS. The method is demonstrated by proving the alternating-bit protocol under weak assumptions about the unreliable media.\n          <\/jats:p>","DOI":"10.1007\/bf01887208","type":"journal-article","created":{"date-parts":[[2005,7,5]],"date-time":"2005-07-05T06:18:31Z","timestamp":1120544311000},"page":"242-272","source":"Crossref","is-referenced-by-count":9,"title":["A refinement calculus for specifications in Hennessy-Milner logic with recursion"],"prefix":"10.1145","volume":"1","author":[{"given":"S\u00f6ren","family":"Holmstr\u00f6m","sequence":"first","affiliation":[{"name":"Programming Methodology Group, Department of Computer Science, Chalmers University of Technology, S-412 96, G\u00f6teborg, Sweden"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Brookes S. and Rounds W.: Behavioural equivalences induced by programming logics ICALP'83 LNCS 154 Springer-Verlag 1983."},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Graf S. and Sifakis J.: A modal characterization of observational congruence on finite terms of CCS ICALP'84 LNCS 172 Springer-Verlag 1984.","DOI":"10.1007\/3-540-13345-3_20"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Hennessy M. and Milner R.: Algebraic laws for Nondeterminism and Concurrency. J. ACM 32(1) (1985).","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Kozen D.: Results on the Propositional \u03bc -calculus ICALP'82 LNCS 140 Springer-Verlag 1982.","DOI":"10.7146\/dpb.v11i146.7420"},{"key":"e_1_2_1_2_5_2","unstructured":"Larsen K.G.: Context-Dependent Bisimulation between Processes Ph.D. thesis CST-37-86 University of Edinburgh 1986."},{"key":"e_1_2_1_2_6_2","unstructured":"Larsen K.G.: Proof Systems for Hennessy-Milner Logic with Recursion CAAP'88 LNCS 299 Springer-Verlag 1988."},{"key":"e_1_2_1_2_7_2","unstructured":"Larsen K. G. and Milner R.: A Complete Protocol Verification using Relativized Bisimulation R86-12 Institute of Electronic Systems Aalborg University Center 1986."},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Milner R.: A Calculus of Communicating Systems LNCS 92 Springer-Verlag 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Milner R.: The calculus CCS and its evaluation rules Seminar on Concurrency CMU LNCS 197 Springer-Verlag 1984.","DOI":"10.1007\/3-540-15670-4_10"},{"key":"e_1_2_1_2_11_2","unstructured":"Pnueli A.: Linear and Branching Structures in the Semantics and Logics of Reactive Systems ICALP'85 LNCS 194 Springer-Verlag 1985."},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Stirling C.: A Proof Theoretic Characterisation of Observational Equivalence Theoretical Computer Science 39 (1985).","DOI":"10.1016\/0304-3975(85)90129-X"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Stirling C.: A Complete Compositional Modal Proof System for a Subset of CCS ICALP'85 LNCS 194 Springer-Verlag 1985.","DOI":"10.1007\/3-540-15198-2_16"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Tarski A.: A Lattice-Theoretical Fixpoint Theorem and its Applications Pacific J. Math. 5 (1955).","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Winskel G.: A Complete Proof System for SCCS with Modal Assertions Cambridge Computer Lab. Tech. Rep. 78 September 1985.","DOI":"10.1007\/3-540-16042-6_22"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01887208.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01887208\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01887208","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:24:21Z","timestamp":1641482661000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01887208"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,3]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1989,3]]}},"alternative-id":["10.1007\/BF01887208"],"URL":"https:\/\/doi.org\/10.1007\/bf01887208","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1989,3]]}}}