{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:52:35Z","timestamp":1694623955997},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[1996,3,1]],"date-time":"1996-03-01T00:00:00Z","timestamp":825638400000},"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":[[1996,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            This paper presents an assumption\/commitment specification technique and a refinement calculus for networks of agents communicating asynchronously via unbounded FIFO channels in the tradition of Kahn.\n            <jats:list list-type=\"bullet\">\n              <jats:list-item>\n                <jats:p>We define two types of assumption\/commitment specifications, namely simple and general specifications.<\/jats:p>\n              <\/jats:list-item>\n              <jats:list-item>\n                <jats:p>It is shown that semantically, any deterministic agent can be uniquely characterized by a simple specification, and any nondeterministic agent can be uniquely characterized by a general specification.<\/jats:p>\n              <\/jats:list-item>\n              <jats:list-item>\n                <jats:p>We define two sets of refinement rules, one for simple specifications and one for general specifications. The rules are Hoare-logic inspired. In particular the feedback rules employ invariants in the style of a traditional while-rule.<\/jats:p>\n              <\/jats:list-item>\n              <jats:list-item>\n                <jats:p>Both sets of rules have been proved to be sound and also (semantic) relative complete.<\/jats:p>\n              <\/jats:list-item>\n              <jats:list-item>\n                <jats:p>Conversion rules allow the two logics to be combined. This means that general specifications and the rules for general specifications have to be introduced only at the point in a system development where they are really needed.<\/jats:p>\n              <\/jats:list-item>\n            <\/jats:list>\n          <\/jats:p>","DOI":"10.1007\/bf01214554","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T15:24:32Z","timestamp":1109345072000},"page":"127-161","source":"Crossref","is-referenced-by-count":4,"title":["Specification and refinement of networks of asynchronously communicating agents using the assumption\/commitment paradigm"],"prefix":"10.1145","volume":"8","author":[{"given":"Ketil","family":"St\u00f8len","sequence":"first","affiliation":[{"name":"Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Dederichs","sequence":"additional","affiliation":[{"name":"Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rainer","family":"Weber","sequence":"additional","affiliation":[{"name":"Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","volume-title":"Technical Report 29","author":"Abadi M.","year":"1988"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Abadi M. and Lamport L.: Composing specifications. In J. W. de Bakker W. P. de Roever and G. Rozenberg editors Proc. REX Workshop on Stepwise Refinement of Distributed Systems Lecture Notes in Computer Science 430 pages 1\u201341 1990.","DOI":"10.1007\/3-540-52559-9_59"},{"key":"e_1_2_1_2_3_2","volume-title":"Technical Report 118","author":"Abadi M.","year":"1993"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Brock J. D. and Ackermann W. B.: Scenarios: A model of non-determinate computation. In J. Diaz and I. Ramos editors Proc. Formalization of Programming Concepts Lecture Notes in Computer Science 107 pages 252\u2013259 1981.","DOI":"10.1007\/3-540-10699-5_102"},{"key":"e_1_2_1_2_6_2","unstructured":"Broy M. Dederichs F. Dendorfer C. Fuchs M. Gritzner T. F. and Weber R.: The design of distributed systems \u2014 an introduction to Focus (revised version). Technical Report SFB 342\/2\/92 A Technische Universit\u00e4t M\u00fcnchen 1993."},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Barringer H. Kuiper R. and Pnueli A.: Now you may compose temporal logic specifications. In Proc. Sixteenth ACM Symposium on Theory of Computing pages 51\u201363 1984.","DOI":"10.1145\/800057.808665"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Broy M.: Towards a design methodology for distributed systems. In M. Broy editor Proc. Constructive Methods in Computing Science Summerschool Marktoberdorf pages 311\u2013364. Springer 1989.","DOI":"10.1007\/978-3-642-74884-4_10"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Broy M.: Functional specification of time sensitive communicating systems. In M. Broy editor Proc. Programming and Mathematical Method Summerschool Marktoberdorf pages 325\u2013367. Springer 1992.","DOI":"10.1007\/978-3-642-77572-7_14"},{"key":"e_1_2_1_2_10_2","unstructured":"Broy M.: A functional rephrasing of the assumption\/commitment specification style. Technical Report SFB 342\/10\/94 A Technische Universit\u00e4t M\u00fcnchen 1994."},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Broy M. and St\u00f8len K.: Specification and refinement of finite dataflow networks \u2014a relational approach. In H. Langmaack W.-P. de Roever and J. Vytopil editors Proc. FTRTFT'94 Lecture Notes in Computer Science 863 pages 247\u2013267 1994.","DOI":"10.1007\/3-540-58468-4_169"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Chandy K. M. and Misra J.: Parallel Program Design A Foundation . Addison-Wesley 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_2_13_2","unstructured":"Dederichs F.: Transformation verteilter Systeme: Von applikativen zu prozeduralen Darstellungen. PhD thesis Technische Universit\u00e4t M\u00fcnchen 1992. Also available as SFB-report 342\/17\/92 A Technische Universit\u00e4t M\u00fcnchen."},{"key":"e_1_2_1_2_14_2","unstructured":"de Roever W. P.: The quest for compositionality formal models in programming. In F. J. Neuhold and G. Chroust editors Proc. IFIP 85 pages 181\u2013205 1985."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Fuchs M. and Philipps J.: Formal development of a production cell in Focus \u2014 a case study. In C. Lewerenz and T. Lindner editors Formal Development of Reactive Systems: Case Study Production Cell Lecture Notes in Computer Science 891 pages 187\u2013200. 1995.","DOI":"10.1007\/3-540-58867-1_55"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_17_2","unstructured":"Jones C. B.: Specification and design of (parallel) programs. In R.E.A. Mason editor Proc. Information Processing 83 pages 321\u2013331. North-Holland 1983."},{"key":"e_1_2_1_2_18_2","unstructured":"Jones C. B.: Systematic Software Development Using VDM Second Edition. Prentice-Hall 1990."},{"key":"e_1_2_1_2_19_2","unstructured":"Kahn G.: The semantics of a simple language for parallel programming. In J.L. Rosenfeld editor Proc. Information Processing 74 pages 471\u2013475. North-Holland 1974."},{"key":"e_1_2_1_2_20_2","unstructured":"Keller R. M.: Denotational models for parallel programs with indeterminate operators. In E. J. Neuhold editor Proc. Formal Description of Programming Concepts pages 337\u2013366. North-Holland 1978."},{"key":"e_1_2_1_2_21_2","unstructured":"Kleene S. C.: Introduction to Metamathematics . Van Nostrand 1952."},{"key":"e_1_2_1_2_22_2","unstructured":"Kahn G. and MacQueen D. B.: Corutines and networks of parallel processes. In B. Gilchrist editor Proc. Information Processing 77 pages 993\u2013998. North-Holland 1977."},{"key":"e_1_2_1_2_23_2","unstructured":"Manna Z.: Mathematical Theory of Computation . McGraw-Hill 1974."},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Pandya P. K.: Some comments on the assumption-commitment framework for compositional verification of distributed programs. In J. W. de Bakker W. P. de Roever and G. Rozenberg editors Proc. REX Workshop on Stepwise Refinement of Distributed Systems Lecture Notes in Computer Science 430 pages 622\u2013640 1990.","DOI":"10.1007\/3-540-52559-9_81"},{"key":"e_1_2_1_2_28_2","unstructured":"Park D.: The \u201cfairness\u201d problem and nondeterministic computing networks. In J. W. de Bakker and J van Leeuwen editors Proc. 4th Foundations of Computer Science Mathematical Centre Tracts 159 pages 133\u2013161. Mathematisch Centrum Amsterdam 1983."},{"key":"e_1_2_1_2_29_2","unstructured":"Philipps J.: Spezifikation einer Fertigungszelle \u2014 eine Fallstudie in Focus. Master's thesis Technische Universi\u00e4t M\u00fcnchen 1993."},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02311231"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Pnueli A.: In transition from global to modular temporal reasoning about programs. In K. R. Apt editor Proc. Logics and Models of Concurrent Systems pages 123\u2013144. Springer 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"e_1_2_1_2_32_2","unstructured":"St\u00f8len K. Dederichs F. and Weber R.: Assumption\/commitment rules for networks of asynchronously communicating agents. Technical Report SFB 342\/2\/93 A Technische Universit\u00e4t M\u00fcnchen 1993."},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Stark E. W.: A proof technique for rely\/guarantee properties. In S. N. Maheshwari editor Proc. 5th Conference on the Foundation of Software Technology and Theoretical Computer Science Lecture Notes in Computer Science 206 pages 369\u2013391 1985.","DOI":"10.1007\/3-540-16042-6_21"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"St\u00f8len K.: A method for the development of totally correct shared-state parallel programs. In J. C. M. Baeten and J. F. Groote editors Proc. CONCUR'91 Lecture Notes in Computer Science 527 pages 510\u2013525 1991.","DOI":"10.1007\/3-540-54430-5_110"},{"key":"e_1_2_1_2_35_2","unstructured":"Zwiers J.: Compositionality Concurrency and Partial Correctness: Proof Theories for Networks of Processes and Their Relationship Lecture Notes in Computer Science 321. 1989."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01214554.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01214554\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01214554","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:23:41Z","timestamp":1641482621000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01214554"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,3]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,3]]}},"alternative-id":["10.1007\/BF01214554"],"URL":"https:\/\/doi.org\/10.1007\/bf01214554","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,3]]}}}