{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,9,24]],"date-time":"2022-09-24T16:49:43Z","timestamp":1664038183605},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[1994,12,1]],"date-time":"1994-12-01T00:00:00Z","timestamp":786240000000},"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":[[1994,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>There can be different views of a concurrent distributed system, depending on who observes it. The final user may just want to know how the system behaves in terms of its possible sequences of actions, while the designer may want to know what are the sequential components of a system or how are they distributed in space. In other words, there is not a widely accepted single semantic model for concurrent systems. This paper describes a parametric verification tool for process description languages. It performs a symbolic execution of processes at different levels of abstraction and verifies deadlock and reachability properties. The tool also provides facilities to check behavioural equivalences. In addition to the classical interleaving semantics, truly concurrent approaches based on the notion of causality and locality are considered. This allows us to compare the expressive power of different models within the same environment. In this respect, we have verified many of the examples given in the literature using our tool.<\/jats:p>","DOI":"10.1007\/bf03259392","type":"journal-article","created":{"date-parts":[[2012,11,10]],"date-time":"2012-11-10T01:08:19Z","timestamp":1352509699000},"page":"676-695","source":"Crossref","is-referenced-by-count":6,"title":["Automatizing Parametric Reasoning on Distributed Concurrent Systems"],"prefix":"10.1145","volume":"6","author":[{"given":"Paola","family":"Inverardi","sequence":"first","affiliation":[{"name":"I.E.I. - C.N.R., Via S. Maria, 46, I-S6100, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corrado","family":"Priami","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universita di Pisa, Pisa, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Yankelevich","sequence":"additional","affiliation":[{"name":"Department of Computer Science, NC State University, Raleigh, NC, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Formal Aspects of Computing199462(A short version appeared as Rapport de Recherche 1483 INRIA July 1991.)"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90067-7"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/30.6.498"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(87)90085-7"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90088-X"},{"key":"e_1_2_1_2_6_2","first-page":"108","volume-title":"Proc. CONCUR\u201992","author":"Boudol G","year":"1992"},{"issue":"4","key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","first-page":"433","DOI":"10.3233\/FI-1988-11406","article-title":"A Non-interleaving Semantics for CCS Based on Proved Transitions","author":"Boudol G","year":"1988","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0013019","volume-title":"REX School\/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","author":"de Bakker J","year":"1989"},{"key":"e_1_2_1_2_9_2","volume-title":"Proc. of ERCIM Workshop on Theory and Practice in Verification, Pisa, 9\u201311 December","author":"Cleaveland R","year":"1992"},{"issue":"1","key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","article-title":"The Concurrency Workbench","volume":"15","author":"Cleaveland R","year":"1993","journal-title":"ACM TOPLAS"},{"key":"e_1_2_1_2_11_2","first-page":"234","volume-title":"Proc. ICALP \u201989","author":"Darondeau Ph","year":"1989"},{"key":"e_1_2_1_2_12_2","first-page":"105","volume-title":"Formal Description of Programming Concepts III","author":"Degano P","year":"1987"},{"key":"e_1_2_1_2_13_2","first-page":"3","volume-title":"Proc. IFIP\u201988","author":"Degano P","year":"1990"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90153-K"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90032-8"},{"key":"e_1_2_1_2_16_2","first-page":"629","volume-title":"Proc. ICALP\u201992","author":"Degano P","year":"1992"},{"key":"e_1_2_1_2_17_2","volume-title":"A Compact Representation of Finite-State Processes","author":"Degano P","year":"1993"},{"key":"e_1_2_1_2_18_2","volume-title":"IEEE Proc. 14th International Conference on Software Engineering","author":"Felder M","year":"1992"},{"key":"e_1_2_1_2_19_2","volume-title":"Ald\u00e9baran: a Tool for Verification of Communicating Processes","author":"Fernandez J C","year":"1989"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Ferrari G. L. Gorrieri R. and Montanari U.: An Extended Expansion Theorem. In Proc. TAPSOFT\u201991 LNCS 494 Springer-Verlag pp. 29\u201348.","DOI":"10.1007\/3540539816_56"},{"key":"e_1_2_1_2_21_2","volume-title":"IEEE Proc. 14th International Conference on Software Engineering","author":"Fernandez J C","year":"1992"},{"key":"e_1_2_1_2_22_2","first-page":"237","volume-title":"Proc. 14th MFCS LNCS 379","author":"van Glabbeek R","year":"1989"},{"key":"e_1_2_1_2_23_2","volume-title":"TAV Users Manual","author":"Godskesen J C","year":"1989"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/0164-1212(90)90074-V"},{"key":"e_1_2_1_2_25_2","first-page":"125","article-title":"The Non-Sequential Behaviour of Petri Nets","volume":"57","author":"Goltz U","year":"1983","journal-title":"Information and Computation"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_27_2","first-page":"158","article-title":"Evaluation of Tools for the Analysis of Communicating Systems","volume":"45","author":"Inverardi P","year":"1991","journal-title":"EATCS Bulletin"},{"key":"e_1_2_1_2_28_2","volume-title":"Proc. of ICALP\u201993","author":"Inverardi P","year":"1993"},{"key":"e_1_2_1_2_29_2","volume-title":"Local and Global Causes","author":"Kiehn A","year":"1991"},{"key":"e_1_2_1_2_30_2","volume-title":"The Current States of Bisimulation Tools. Tech. Rep. P9101, CWI","author":"Korver H","year":"1991"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Modal Specifications","author":"Larsen K","year":"1990"},{"key":"e_1_2_1_2_32_2","volume-title":"PAM: A Process Algebra Manipulator","author":"Lin H","year":"1991"},{"key":"e_1_2_1_2_33_2","first-page":"110","article-title":"Verification Tools from the CONCUR project","volume":"47","author":"Madelaine E","year":"1992","journal-title":"EATCS Bulletin"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"e_1_2_1_2_35_2","volume-title":"Communication and Concurrency","author":"Milner R","year":"1989"},{"issue":"2","key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1145\/3318.3322","article-title":"CIRCAL and the Representation of Communication, Concurrency and Time","volume":"7","author":"Milne G J","year":"1985","journal-title":"ACM TOPLAS"},{"key":"e_1_2_1_2_37_2","first-page":"617","volume-title":"Proc. ICALP\u201992","author":"Montanari U","year":"1992"},{"issue":"9","key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","first-page":"794","DOI":"10.1109\/32.159837","article-title":"Compiling Real Time Specifications into Extended Automata","volume":"18","author":"Niccolin X","year":"1992","journal-title":"Transaction of Software Engineering"},{"key":"e_1_2_1_2_39_2","unstructured":"SIAM J. Comput.1987166"},{"key":"e_1_2_1_2_40_2","volume-title":"A Structural Approach to Operational Semantics","author":"Plotkin G","year":"1981"},{"key":"e_1_2_1_2_41_2","first-page":"15","volume-title":"Proc. of ICALP\u201985","author":"Pnueli A","year":"1985"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01379149"},{"key":"e_1_2_1_2_43_2","volume-title":"Proc. of 1st International Workshop on Automated and Algorithmic Debugging","author":"Priami C","year":"1993"},{"key":"e_1_2_1_2_44_2","volume-title":"Petri Nets \u2014 an Introduction. EATCS Monographs on Theoretical Computer Science, Vol. 4","author":"Reisig W","year":"1985"},{"issue":"4","key":"e_1_2_1_2_45_2","first-page":"357","article-title":"Nets of Processes","author":"Rabinovich A","year":"1988","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90093-3"},{"key":"e_1_2_1_2_47_2","volume-title":"Aboard AUTO. Tech. Rep. Ill, INRIA, Sophia-Antipolis","author":"de Simone R","year":"1989"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322272"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322273"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90032-0"},{"key":"e_1_2_1_2_51_2","volume-title":"PhD Thesis","author":"Yankelevich D","year":"1993"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF03259392.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF03259392\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF03259392","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:31:27Z","timestamp":1641483087000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF03259392"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,12]]},"references-count":51,"journal-issue":{"issue":"6","published-print":{"date-parts":[[1994,12]]}},"alternative-id":["10.1007\/BF03259392"],"URL":"https:\/\/doi.org\/10.1007\/bf03259392","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,12]]}}}