{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:35:27Z","timestamp":1761510927994},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026515"},{"type":"electronic","value":"9783642026522"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02652-2_20","type":"book-chapter","created":{"date-parts":[[2009,6,25]],"date-time":"2009-06-25T11:43:06Z","timestamp":1245930186000},"page":"241-260","source":"Crossref","is-referenced-by-count":24,"title":["Verification of GALS Systems by Combining Synchronous Languages and Process Calculi"],"prefix":"10.1007","author":[{"given":"Hubert","family":"Garavel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damien","family":"Thivolle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"20_CR1","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","volume":"16","author":"A. Benveniste","year":"1991","unstructured":"Benveniste, A., Le Guernic, P., Jacquemot, C.: Synchronous Programming with Events and Relations: The SIGNAL Language and Its Semantics. Sci. Comput. Program.\u00a016(2), 103\u2013149 (1991)","journal-title":"Sci. Comput. Program."},{"key":"20_CR2","first-page":"85","volume-title":"POPL\u201993","author":"G. Berry","year":"1993","unstructured":"Berry, G., Ramesh, S., Shyamasundar, R.K.: Communicating Reactive Processes. In: POPL\u201993, pp. 85\u201398. ACM, New York (1993)"},{"issue":"2","key":"20_CR3","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The Esterel Synchronous Programming Language: Design, Semantics, Implementation. Science of Computer Programming\u00a019(2), 87\u2013152 (1992)","journal-title":"Science of Computer Programming"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-44798-9_10","volume-title":"Correct Hardware Design and Verification Methods","author":"G. Berry","year":"2001","unstructured":"Berry, G., Sentovich, E.: Multiclock Esterel. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 110\u2013125. Springer, Heidelberg (2001)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Braden, R.: Requirements for Internet Hosts - Application and Support. RFC 1123, Internet Engineering Task Force (October 1989)","DOI":"10.17487\/rfc1123"},{"issue":"3","key":"20_CR6","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S.D. Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A Theory of Communicating Sequential Processes. Journal of the ACM\u00a031(3), 560\u2013599 (1984)","journal-title":"Journal of the ACM"},{"key":"20_CR7","unstructured":"Champelovier, D., Clerc, X., Garavel, H.: Reference Manual of the LOTOS NT to LOTOS Translator, Version 4G. Internal Report, INRIA\/VASY (January 2009)"},{"key":"20_CR8","unstructured":"Clerc, X., Garavel, H., Thivolle, D.: Pr\u00e9sentation du language SAM d\u2019Airbus. Internal Report, INRIA\/VASY (2008), TOPCASED forge: http:\/\/gforge.enseeiht.fr\/docman\/view.php\/33\/2745\/SAM.pdf"},{"issue":"2","key":"20_CR9","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.entcs.2005.05.038","volume":"146","author":"F. Doucet","year":"2006","unstructured":"Doucet, F., Menarini, M., Kr\u00fcger, I.H., Gupta, R.K., Talpin, J.-P.: A Verification Approach for GALS Integration of Synchronous Components. Electr. Notes Theor. Comput. Sci.\u00a0146(2), 105\u2013131 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"20_CR10","unstructured":"Garavel, H.: Compilation et v\u00e9rification de programmes LOTOS. Th\u00e8se de Doctorat, Universit\u00e9 Joseph\u00a0Fourier (Grenoble) (November 1989)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/3-540-45614-7_23","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"H. Garavel","year":"2002","unstructured":"Garavel, H., Hermanns, H.: On Combining Functional Verification and Performance Evaluation using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 410\u2013429. Springer, Heidelberg (2002)"},{"key":"20_CR12","first-page":"377","volume-title":"Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE\u20192001","author":"H. Garavel","year":"2001","unstructured":"Garavel, H., Lang, F.: SVL: a Scripting Language for Compositional Verification. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE\u20192001, Cheju Island, Korea, pp. 377\u2013392. IFIP, Kluwer Academic Publishers, Dordrecht (2001); Full version available as INRIA Research Report\u00a0RR-4223"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-540-73368-3_18","volume-title":"Computer Aided Verification","author":"H. Garavel","year":"2007","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 158\u2013163. Springer, Heidelberg (2007)"},{"key":"20_CR14","unstructured":"Garavel, H., Turlier, P.: C\u00c6SAR.ADT\u00a0: un compilateur pour les types abstraits alg\u00e9briques du langage LOTOS. In: Dssouli, R., Bochmann, G.v. (eds.) Actes du Colloque Francophone pour l\u2019Ing\u00e9nierie des Protocoles CFIP 1993, Montr\u00e9al, Canada (1993)"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/3-540-45828-X_20","volume-title":"Embedded Software","author":"A. Girault","year":"2002","unstructured":"Girault, A., M\u00e9nier, C.: Automatic Production of Globally Asynchronous Locally Synchronous Systems. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol.\u00a02491, pp. 266\u2013281. Springer, Heidelberg (2002)"},{"issue":"9","key":"20_CR16","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The Synchronous Dataflow Programming Language LUSTRE. Proceedings of the IEEE\u00a079(9), 1305\u20131320 (1991)","journal-title":"Proceedings of the IEEE"},{"key":"20_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2231-4","volume-title":"Synchronous programming of reactive systems","author":"N. Halbwachs","year":"1993","unstructured":"Halbwachs, N.: Synchronous programming of reactive systems. Kluwer Academic, Dordrecht (1993)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-45828-X_18","volume-title":"Embedded Software","author":"N. Halbwachs","year":"2002","unstructured":"Halbwachs, N., Baghdadi, S.: Synchronous Modelling of Asynchronous Systems. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol.\u00a02491, pp. 240\u2013251. Springer, Heidelberg (2002)"},{"key":"20_CR19","first-page":"3","volume-title":"ACSD \u201906","author":"N. Halbwachs","year":"2006","unstructured":"Halbwachs, N., Mandel, L.: Simulation and Verification of Asynchronous Systems by Means of a Synchronous Model. In: ACSD \u201906, pp. 3\u201314. IEEE Computer Society, Washington (2006)"},{"key":"20_CR20","volume-title":"The Spin Model Checker - Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"20_CR21","unstructured":"ISO\/IEC. LOTOS \u2014 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization \u2014 Information Processing Systems \u2014 Open Systems Interconnection, Gen\u00e8ve (September 1989)"},{"key":"20_CR22","unstructured":"ISO\/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization \u2014 Information Technology, Gen\u00e8ve (September 2001)"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Le Guernic, P., Talpin, J.-P., Le Lann, J.-C.: Polychrony for System Design. Journal of Circuits, Systems and Computers. World Scientific\u00a012 (2003)","DOI":"10.1142\/S0218126603000763"},{"issue":"1\u20133","key":"20_CR24","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/S0096-0551(01)00016-9","volume":"27","author":"F. Maraninchi","year":"2001","unstructured":"Maraninchi, F., R\u00e9mond, Y.: Argos: an Automaton-Based Synchronous Language. Computer Languages\u00a027(1\u20133), 61\u201392 (2001)","journal-title":"Computer Languages"},{"issue":"3","key":"20_CR25","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","volume":"46","author":"R. Mateescu","year":"2003","unstructured":"Mateescu, R., Sighireanu, M.: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. Science of Computer Programming\u00a046(3), 255\u2013281 (2003)","journal-title":"Science of Computer Programming"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-68237-0_12","volume-title":"FM 2008: Formal Methods","author":"R. Mateescu","year":"2008","unstructured":"Mateescu, R., Thivolle, D.: A Model Checking Language for Concurrent Value-Passing Systems. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 148\u2013164. Springer, Heidelberg (2008)"},{"issue":"5","key":"20_CR27","doi-asserted-by":"publisher","first-page":"1045","DOI":"10.1002\/j.1538-7305.1955.tb03788.x","volume":"34","author":"G.H. Mealy","year":"1955","unstructured":"Mealy, G.H.: A Method for Synthesizing Sequential Circuits. Bell System Technical Journal\u00a034(5), 1045\u20131079 (1955)","journal-title":"Bell System Technical Journal"},{"key":"20_CR28","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R. Milner","year":"1983","unstructured":"Milner, R.: Calculi for Synchrony and Asynchrony. Theoretical Computer Science\u00a025, 267\u2013310 (1983)","journal-title":"Theoretical Computer Science"},{"key":"20_CR29","first-page":"10384","volume-title":"DATE \u201904","author":"M.R. Mousavi","year":"2004","unstructured":"Mousavi, M.R., Le Guernic, P., Talpin, J.-P., Shukla, S.K., Basten, T.: Modeling and Validating Globally Asynchronous Design in Synchronous Frameworks. In: DATE \u201904, p. 10384. IEEE Computer Society Press, Washington (2004)"},{"issue":"1","key":"20_CR30","first-page":"131","volume":"78","author":"D. Potop-Butucaru","year":"2007","unstructured":"Potop-Butucaru, D., Caillaud, B.: Correct-by-Construction Asynchronous Implementation of Modular Synchronous Specifications. Fundam. Inf.\u00a078(1), 131\u2013159 (2007)","journal-title":"Fundam. Inf."},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Ramesh, S.: Communicating Reactive State Machines: Design, Model and Implementation. In: IFAC Workshop on Distributed Computer Control Systems (1998)","DOI":"10.1016\/S1474-6670(17)36343-7"},{"key":"20_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/978-3-540-27813-9_47","volume-title":"Computer Aided Verification","author":"S. Ramesh","year":"2004","unstructured":"Ramesh, S., Sonalkar, S., D\u2019Silva, V., Chandra, N., Vijayalakshmi, B.: A Toolset for Modelling and Verification of GALS Systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 506\u2013509. Springer, Heidelberg (2004)"},{"key":"20_CR33","doi-asserted-by":"crossref","unstructured":"Sollins, K.: The TFTP Protocol (Revision 2). RFC 1350, Internet Engineering Task Force (July 1992)","DOI":"10.17487\/rfc1350"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02652-2_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T02:37:22Z","timestamp":1558406242000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02652-2_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026515","9783642026522"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02652-2_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}