{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,15]],"date-time":"2023-08-15T17:53:40Z","timestamp":1692122020299},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T00:00:00Z","timestamp":1472688000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Inria Rhone Alpes"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            A GALS (\n            <jats:italic>Globally Asynchronous, Locally Synchronous<\/jats:italic>\n            ) system consists of several synchronous components that evolve concurrently and interact with each other asynchronously. The design of GALS systems is tedious and error-prone due to the high degree of synchronous and asynchronous concurrency present in complex architectures. In this paper, we present GRL (\n            <jats:italic>GALS Representation Language<\/jats:italic>\n            ), a formal language designed to model GALS systems, for the purpose of formal verification of the asynchronous aspects. GRL combines the synchronous reactive model underlying dataflow languages and the asynchronous concurrent model underlying process algebras. We propose a translation from GRL to LNT, a value-passing concurrent language with classical process algebra flavour. This makes possible the analysis of GRL specifications using all the state-of-the-art simulation and verification functionalities provided by the CADP toolbox.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0373-3","type":"journal-article","created":{"date-parts":[[2016,5,3]],"date-time":"2016-05-03T07:42:13Z","timestamp":1462261333000},"page":"767-804","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal modelling and verification of GALS systems using GRL and CADP"],"prefix":"10.1145","volume":"28","author":[{"given":"Fatma","family":"Jebali","sequence":"first","affiliation":[{"name":"INRIA, Grenoble, France"},{"name":"Univ. Grenoble Alpes, LIG, 38000, Grenoble, France"},{"name":"CNRS, LIG, 38000, Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Lang","sequence":"additional","affiliation":[{"name":"INRIA, Grenoble, France"},{"name":"Univ. Grenoble Alpes, LIG, 38000, Grenoble, France"},{"name":"CNRS, LIG, 38000, Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Mateescu","sequence":"additional","affiliation":[{"name":"INRIA, Grenoble, France"},{"name":"Univ. Grenoble Alpes, LIG, 38000, Grenoble, France"},{"name":"CNRS, LIG, 38000, Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Benveniste A Bouillard A Caspi P (2010) A unifying view of loosely time-triggered architectures. In: Proceedings of the Tenth ACM International Conference on Embedded Software EMSOFT \u201910 ACM New York NY USA pp 189\u2013198","DOI":"10.1145\/1879021.1879047"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bai Y Brandt J Schneider K (2012) Preservation of LTL properties in desynchronized systems. In: MEMOCODE . IEEE July 2012 pp 53\u201364","DOI":"10.1109\/MEMCOD.2012.6292300"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Benveniste A Caillaud B Le Guernic P (1999) From synchrony to asynchrony. In: Jos C Baeten M Mauw S (eds) CONCUR\u201999 vol 1664 of LNCS . Springer Berlin pp 162\u2013177","DOI":"10.1007\/3-540-48320-9_13"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Backes J Cofer DD Miller SP Whalen M (2015) Requirements analysis of a quad-redundant flight control system. CoRR arXiv:1502.03343","DOI":"10.1007\/978-3-319-17524-9_7"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bae K \u00d6lveczky PC Meseguer J (2014) Definition semantics and analysis of multirate synchronous AADL. In: Jones C Pihlajasaari P Sun J (eds) FM 2014 vol 8442 of LNCS pp 94\u2013109","DOI":"10.1007\/978-3-319-06410-9_7"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bouali A (1998) Xeve an Esterel verification environment. In: Hu AJ Vardi MY (eds) CAV vol 1427 of LNCS. Springer Berlin pp 500\u2013504","DOI":"10.1007\/BFb0028770"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Berry G Ramesh S Shyamasundar RK (1993) Communicating reactive processes. In: Proc. of POPL ACM Press pp 85\u201398","DOI":"10.1145\/158511.158526"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Berry G Sentovich E (2001) Multiclock Esterel. In: Proc. of CHARME volume 2144 of LNCS Springer Berlin pp 110\u2013125","DOI":"10.1007\/3-540-44798-9_10"},{"key":"e_1_2_1_2_9_2","unstructured":"Champelovier D Clerc X Garavel H Guerte Y Powazny V Lang F Serwe W Smeding G (2014) Reference Manual of the LNT to LOTOS Translator (Version 6.1). INRIA\/VASY and INRIA\/CONVECS pp 131"},{"key":"e_1_2_1_2_10_2","unstructured":"Chapiro DM (1984) Globally-Asynchronous Locally-Synchronous Systems. Technical report DTIC Document"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Caspi P Mazuet C Paligot N (2001) About the design of distributed control systems: the quasi-synchronous approach. In: Udo Voges editor Computer Safety Reliability and Security volume 2187 of LNCS Springer Berlin Heidelberg pp 215\u2013226","DOI":"10.1007\/3-540-45416-0_21"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.05.038"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.009"},{"key":"e_1_2_1_2_14_2","unstructured":"Gamati\u00e9 A Gautier T (2003) The signal approach to the design of system architectures. In: 10th IEEE international conference on engineering of computer-based systems ECBS 2003 IEEE Huntsville AL USA pp 80\u201388"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Ganai MK Gupta A (2007) Efficient BMC for multi-clock systems with clocked specifications. In: Design automation conference pp 310\u2013315","DOI":"10.1109\/ASPDAC.2007.358004"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2009.125"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Glouche Y Le Guernic P Talpin J-P Gautier T (2010) A boolean algebra of contracts for assume-guarantee reasoning. In: Electron Notes Theor Comput Sci 263:111\u2013127 (Proceedings of the 6th International Workshop on Formal Aspects of Component Software (FACS 2009))","DOI":"10.1016\/j.entcs.2010.05.007"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Garavel H Lang F (2002) SVL: a scripting language for compositional verification. In: Formal techniques for networked and distributed systems IFIP conference proceedings Springer Berlin pp 377\u2013392","DOI":"10.1007\/0-306-47003-9_24"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Garavel H Lang F Mateescu R (2002) Compiler Construction using LOTOS NT. In: Horspool N (ed) Proceedings of the 11th international conference on compiler construction (CC\u201902) Grenoble France vol 2304 of LNCS pp 9\u201313","DOI":"10.1007\/3-540-45937-5_3"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0226-1"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0244-z"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Garavel H Thivolle D (2009) Verification of GALS systems by combining synchronous languages and process calculi. In: Pasareanu C (ed) Model checking software proceedings of the 16th international SPIN workshop on model checking of software SPIN\u20192009 (Grenoble France) vol 5578 of LNCS pp 241\u2013260","DOI":"10.1007\/978-3-642-02652-2_20"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100044"},{"key":"e_1_2_1_2_24_2","volume-title":"Synchronous programming of reactive systems, vol 215","author":"Halbwachs N","year":"2013"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Halbwachs N Baghdadi S (2012) Synchronous modeling of asynchronous systems. In: EMSOFT\u201902 vol 2491 of LNCS Springer Grenoble pp 240\u2013251","DOI":"10.1007\/3-540-45828-X_18"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Halbwachs N Lagnier F Raymond P (1993) Synchronous observers and the verification of reactive systems. In: AMAST\u201993 Twente Springer Berlin pp 83\u201396","DOI":"10.1007\/978-1-4471-3227-1_8"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Halbwachs N Lagnier F Raymond P (1993) Synchronous observers and the verification of reactive systems. In: Nivat M Rattray C Rus T Scollo G (eds) AMAST\u201993 Twente June 1993. Workshops in Computing Springer Berlin","DOI":"10.1007\/978-1-4471-3227-1_8"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Halbwachs N Mandel L (2006) Simulation and verification of asynchronous systems by means of a synchronous model. In: Proc. of ACSD pp 3\u201314","DOI":"10.1109\/ACSD.2006.24"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5)","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_2_30_2","unstructured":"ISO\/IEC (2001) Enhancements to LOTOS (E-LOTOS). International standard 15437:2001 International organization for standardization\u2014information technology Gen\u00e8ve"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Jebali F Lang F Mateescu R (2014) GRL: A specification language for globally asynchronous locally synchronous systems. Proc. of ICFEM vol 8829 pp 219\u2013234","DOI":"10.1007\/978-3-319-11737-9_15"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Jebali F Lang F Mateescu R (2014) GRL: A specification language for globally asynchronous locally synchronous systems (syntax and formal semantics). Research report RR-8527 INRIA","DOI":"10.1007\/978-3-319-11737-9_15"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126603000763"},{"key":"e_1_2_1_2_34_2","unstructured":"Milner R (1982) A calculus of communicating systems Springer New York"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"e_1_2_1_2_36_2","volume-title":"Communication and concurrency, vol 84","author":"Milner R","year":"1989"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2010.01.001"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Mateescu R Thivolle D (2008) A model checking language for concurrent value-passing systems. In: Proc. of FM LNCS Springer Berlin pp 148\u2013164","DOI":"10.1007\/978-3-540-68237-0_12"},{"key":"e_1_2_1_2_39_2","unstructured":"Miller SP Whalen MW O\u2019Brien D Heimdahl MP Joshi A (2005) A methodology for the design and verification of globally asynchronous\/locally synchronous architectures. National Aeronautics and Space Administration Langley Research Center"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-7844-8"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Potop-Butucaru D De Simone R Sorel Y Talpin J-P (2009) From concurrent multi-clock programs to deterministic asynchronous implementations. In: ACSD \u201909. IEEE pp 42\u201351","DOI":"10.1109\/ACSD.2009.23"},{"key":"e_1_2_1_2_42_2","unstructured":"Plotkin GD (1981) A structural approach to operational semantics. Technical Report DAIMI FN-19 University of Aarhus"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Heejong P Avinash M Zoran S (2015) Compiling and verifying 0SC-systemJ programs for safety-critical reactive systems. Comput Lang Syst Struct 44(PC):251\u2013282","DOI":"10.1016\/j.cl.2015.08.006"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Ramesh S (1998) Communicating reactive state machines: design model and implementation. In: IFAC Workshop on Distributed Computer Control Systems","DOI":"10.1016\/S1474-6670(17)36343-7"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Ramesh S Sonalkar S Dsilva V Naveen Chandra R Vijayalakshmi B (2004) A Toolset for Modelling and Verification of GALS Systems. In: Alur R Peled DA (eds) Proc. of CAV volume 3114 of LNCS Springer pp 506\u2013509","DOI":"10.1007\/978-3-540-27813-9_47"},{"key":"e_1_2_1_2_46_2","unstructured":"Smeding G (2013) Verification of Weakly-Hard Requirements on Quasi-Synchronous Systems. Theses Universit\u00e9 de Grenoble"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/352029.352035"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/233551.233556"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0373-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0373-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0373-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:16:23Z","timestamp":1641485783000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0373-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":48,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,9]]}},"alternative-id":["10.1007\/s00165-016-0373-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0373-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9]]}}}