{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:36:07Z","timestamp":1761510967114,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642336775"},{"type":"electronic","value":"9783642336782"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33678-2_25","type":"book-chapter","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T15:02:42Z","timestamp":1346943762000},"page":"291-304","source":"Crossref","is-referenced-by-count":5,"title":["On the Formal Verification of Systems of Synchronous Software Components"],"prefix":"10.1007","author":[{"given":"Henning","family":"G\u00fcnther","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Milius","sequence":"additional","affiliation":[]},{"given":"Oliver","family":"M\u00f6ller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"de Alfaro, L., Alur, R., Grosu, R., Henzinger, T., Kang, M., Majumdar, R., Mang, F., Meyer-Kirsch, C., Wang, B.: Mocha: Exploiting modularity in model checking (2000), http:\/\/www.cis.upenn.edu\/~mocha"},{"issue":"1","key":"25_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information and Computation\u00a0104(1), 2\u201334 (1993)","journal-title":"Information and Computation"},{"key":"25_CR3","first-page":"7","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive modules. FMSD\u00a015, 7\u201348 (1999)","journal-title":"FMSD"},{"key":"25_CR4","unstructured":"Andr\u00e9, C.: Semantics of S.S.M (safe state machine). Tech. Rep. UMR 6070, I3S Laboratory, University of Nice-Sophia Antipolis (2003)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48983-5_1","volume-title":"Hybrid Systems: Computation and Control","author":"P. Baufreton","year":"1999","unstructured":"Baufreton, P.: SACRES: A Step Ahead in the Development of Critical Avionics Applications. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol.\u00a01569, p. 1. Springer, Heidelberg (1999)"},{"key":"25_CR6","unstructured":"Baufreton, P.: Visual notations based on synchronous languages for dynamic validation of GALS systems. In: CCCT 2004 Computing, Communications and Control Technologies, Austin, Texas (August 2004)"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-02053-7_11","volume-title":"Coordination Models and Languages","author":"T. Bouhadiba","year":"2009","unstructured":"Bouhadiba, T., Maraninchi, F.: Contract-Based Coordination of Hardware Components for the Development of Embedded Software. In: Field, J., Vasconcelos, V.T. (eds.) COORDINATION 2009. LNCS, vol.\u00a05521, pp. 204\u2013224. Springer, Heidelberg (2009)"},{"key":"25_CR8","unstructured":"Chapiro, D.M.: Globally-asynchronous locally-synchronous systems. Ph.D. thesis. Stanford University (1984)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-30206-3_3","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"S. Dajani-Brown","year":"2004","unstructured":"Dajani-Brown, S., Cofer, D., Bouali, A.: Formal Verification of an Avionics Sensor Voter Using SCADE. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol.\u00a03253, pp. 5\u201320. Springer, Heidelberg (2004)"},{"key":"25_CR11","first-page":"105","volume":"146","author":"F. Doucet","year":"2006","unstructured":"Doucet, F., Menarini, M., Kr\u00fcger, I.H., Gupta, R., Talpin, J.P.: A verification approach for GALS integration of synchronous components. ENTCS\u00a0146, 105\u2013131 (2006)","journal-title":"ENTCS"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-642-02652-2_20","volume-title":"Model Checking Software","author":"H. Garavel","year":"2009","unstructured":"Garavel, H., Thivolle, D.: Verification of GALS Systems by Combining Synchronous Languages and Process Calculi. In: P\u0103s\u0103reanu, C.S. (ed.) SPIN 2009. LNCS, vol.\u00a05578, pp. 241\u2013260. Springer, Heidelberg (2009)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"25_CR14","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1145\/949952.940078","volume":"28","author":"H. Giese","year":"2003","unstructured":"Giese, H., Tichy, M., Burmester, S., Sch\u00e4fer, W., Flake, S.: Towards the compositional verification of real-time uml designs. SIGSOFT Softw. Eng. Notes\u00a028, 38\u201347 (2003)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"issue":"2","key":"25_CR15","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/s10270-005-0103-4","volume":"5","author":"H. Giese","year":"2006","unstructured":"Giese, H., Vilbig, A.: Separation of non-orthogonal concerns in software architecture and design. Software and System Modeling\u00a05(2), 136\u2013169 (2006)","journal-title":"Software and System Modeling"},{"key":"25_CR16","unstructured":"G\u00fcnther, H.: Bahn\u00fcbergangsfallstudie: Verifikationsbericht. Tech. rep. Institut f\u00fcr Theoretische Informatik, Technische Universit\u00e4t Braunschweig (February 2012), http:\/\/www.versyko.de"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"G\u00fcnther, H., Hedayati, R., L\u00f6ding, H., Milius, S., M\u00f6ller, O., Peleska, J., Sulzmann, M., Zechner, A.: A framework for formal verification of systems of synchronous components. In: Proc.\u00a0MBEES 2012 (2012), http:\/\/www.versyko.de","DOI":"10.1007\/978-3-642-33678-2_25"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"G\u00fcnther, H., Milius, S., M\u00f6ller, O.: On the formal verification of systems of synchronous software components (extended version) (May 2012), http:\/\/www.versyko.de","DOI":"10.1007\/978-3-642-33678-2_25"},{"key":"25_CR19","series-title":"Workshops in Computing","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/978-1-4471-3227-1_8","volume-title":"Proc. of AMAST 1993","author":"N. Halbwachs","year":"1994","unstructured":"Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: Proc. of AMAST 1993. Workshops in Computing, pp. 83\u201396. Springer, London (1994)"},{"key":"25_CR20","first-page":"3","volume-title":"Proc. of IFIP","author":"N. Halbwachs","year":"2006","unstructured":"Halbwachs, N., Mandel, L.: Simulation and verification of asynchronous systems by means of a synchronous model. In: Proc. of IFIP, pp. 3\u201314. IEEE Computer Society, Washington, DC (2006)"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46674-6_1","volume-title":"Advances in Computing Science - ASIAN\u201999","author":"N. Halbwachs","year":"1999","unstructured":"Halbwachs, N., Raymond, P.: Validation of Synchronous Reactive Systems: From Formal Verification to Automatic Testing. In: Thiagarajan, P.S., Yap, R.H.C. (eds.) ASIAN 1999. LNCS, vol.\u00a01742, pp. 1\u201312. Springer, Heidelberg (1999)"},{"key":"25_CR22","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/1289927.1289951","volume-title":"Proc. of EMSOFT 2007","author":"E. Jahier","year":"2007","unstructured":"Jahier, E., Halbwachs, N., Raymond, P., Nicollin, X., Lesens, D.: Virtual execution of AADL models via a translation into synchronous programs. In: Proc. of EMSOFT 2007, pp. 134\u2013143. ACM, New York (2007)"},{"key":"25_CR23","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: Proc.\u00a0IFIP Congress, pp. 321\u2013332 (1983)"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Tinelli, C.: PKind: A parallel k-induction based model checker. In: Barnat, J., Heljanko, K. (eds.) PDMC. EPTCS, vol.\u00a072, pp. 55\u201362 (2011)","DOI":"10.4204\/EPTCS.72.6"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Le Guernic, P., Talpin, J.P., Le Lann, J.L.: Polychrony for system design. Journal of Circuits, Systems and Computers (2002); special issue on Application-Specific Hardware Design. World Scientific","DOI":"10.1142\/S0218126603000763"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Milner, R.: Calculi for synchrony and asynchrony. Theoret.\u00a0Comput.\u00a0Sci. 25(3) (July 1983)","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"25_CR27","unstructured":"M\u00f6ller, M.O.: Benchmark Analysis of GTL-Backends using Client-Server Mutex, vol. 1(2). Verified Systems International GmbH (2012) Doc.Id.: Verified-WHITEPAPER-001-2012, http:\/\/www.verified.de\/en\/publications\/"},{"key":"25_CR28","first-page":"10384","volume-title":"Proc. of DATE 2004","author":"M.R. Mousavi","year":"2004","unstructured":"Mousavi, M.R., Le Guernic, P., Talpin, J., Shukla, S.K., Basten, T.: Modeling and validating globally asynchronous design in synchronous frameworks. In: Proc. of DATE 2004, p. 10384. IEEE Computer Society, Washington, DC (2004)"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Rajan, B., Shyamasundar, R.: Multiclock Esterel: a reactive framework for asynchronous design. In: Proc. of IPDPS, pp. 201\u2013209 (2000)","DOI":"10.1109\/IPDPS.2000.845982"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Ramesh, S.: Communicating reactive state machines: Design, model and implementation. In: Proc.\u00a0IFAC Workshop on Distributed Computer Control Systems. Pergamon Press (September 1998)","DOI":"10.1016\/S1474-6670(17)36343-7"},{"key":"25_CR31","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":"25_CR32","unstructured":"Sulzmann, M., Zechner, A., Hedayati, R.: Anforderungsdokument f\u00fcr die Fallstudie Bahn\u00fcbergangssicherungsanlage. Tech. rep., ICS AG (2011)"},{"key":"25_CR33","unstructured":"Contract specification and domain specific modelling language for GALS systems, an approach to system validation. Tech. rep., ICS AG, Verified Systems International GmbH, TU Braunschweig (2011), http:\/\/www.versyko.de"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33678-2_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:27:14Z","timestamp":1744068434000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33678-2_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642336775","9783642336782"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33678-2_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}