{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:21:50Z","timestamp":1742948510900,"version":"3.40.3"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471686"},{"type":"electronic","value":"9783319471693"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-47169-3_11","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T21:56:23Z","timestamp":1475618183000},"page":"134-149","source":"Crossref","is-referenced-by-count":6,"title":["Formally Unifying Modeling and Design for Embedded Systems - A Personal View"],"prefix":"10.1007","author":[{"given":"G.","family":"Berry","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"11_CR1","unstructured":"Rodin Users Handbook. http:\/\/www3.hhu.de\/stups\/handbook\/rodin\/current\/html\/"},{"key":"11_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"11_CR3","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2013","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2013)"},{"key":"11_CR4","unstructured":"Andr\u00e9, C.: Representation, analysis of reactive behaviors: a synchronous approach. In: Proceedings of CESA 1996, IEEE-SMC, Lille, France (1996)"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Arditi, L., Berry, G., Kishinevsky, M.: Late design changes (ECOs) for sequentially optimized Esterel designs. In: Proceedings of Formal Methods in Computer Aided Design, FMCAD 2004, Austin, Texas (2004)","DOI":"10.1007\/978-3-540-30494-4_10"},{"key":"11_CR6","unstructured":"Arditi, L., Berry, G., Kishinevsky, M., Perreaut, M.: Clocking schemes in Esterel. In: Proceedings of Designing Correct Circuits, DCC 2006, Vienna, Austria (2006)"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Balarin, F., Chiodo, M., Jurecska, A., Hsieh, H., Lavagno, A.L., Passerone, C., Sangiovanni-Vincentelli, A., Sentovich, E., Suzuki, K., Tabbara, B.: Hardware-Software Co-Design of Embedded Systems: The Polis Approach. Kluwer Academic Press (1997)","DOI":"10.1007\/978-1-4615-6127-9"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybrid systems modelers. J. Comput. Syst. Sci. (JCSS) 78(3), 877\u2013910 (2012). Special issue in honor of Amir Pnueli","DOI":"10.1016\/j.jcss.2011.08.009"},{"issue":"1","key":"11_CR9","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1109\/JPROC.2002.805826","volume":"91","author":"A Benveniste","year":"2003","unstructured":"Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Le Guernic, P., de Simone, R.: The synchronous languages 12 years later. Proc. IEEE 91(1), 64\u201383 (2003)","journal-title":"Proc. IEEE"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Bergerand, J.L., Pilaud, E., Saga,: a software development environment for dependability in automatic control. In: Proceedings of Safecomp 1988. Pergamon Press (1988)","DOI":"10.1016\/S1474-6670(17)54524-3"},{"issue":"1","key":"11_CR11","first-page":"95","volume":"17","author":"G Berry","year":"1992","unstructured":"Berry, G.: A hardware implementation of pure Esterel. Sadhana Acad. Proc. Eng. Sci. Indian Acad. Sci. 17(1), 95\u2013130 (1992)","journal-title":"Sadhana Acad. Proc. Eng. Sci. Indian Acad. Sci."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Berry, G.: The foundations of Esterel. In: Proof, Language and Interaction Essays in Honour of Robin Milner. MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0021"},{"key":"11_CR13","unstructured":"Berry, G.: The Constructive Semantics of Pure Esterel. Draft book version 3 (without proofs) (2002). http:\/\/www-sop.inria.fr\/members\/Gerard.Berry\/Papers\/EsterelConstructiveBook.pdf"},{"key":"11_CR14","first-page":"1270","volume":"79","author":"G Berry","year":"1991","unstructured":"Berry, G., Benveniste, A.: The synchronous approach to reactive and real-time systems. Another Look Real Time Programm. Proc. IEEE 79, 1270\u20131282 (1991)","journal-title":"Another Look Real Time Programm. Proc. IEEE"},{"key":"11_CR15","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0167-6423(99)00015-5","volume":"36","author":"G Berry","year":"2000","unstructured":"Berry, G., Bouali, A., Fornari, X., Nassor, E., Ledinot, E., de Simone, R.: Esterel: a formal method applied to avionic development. Sci. Comput. Program. 36, 5\u201325 (2000)","journal-title":"Sci. Comput. Program."},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/3-540-15670-4_19","volume-title":"Seminar on Concurrency","author":"G Berry","year":"1985","unstructured":"Berry, G., Cosserat, L.: The ESTEREL synchronous programming language and its mathematical semantics. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 389\u2013448. Springer, Heidelberg (1985). doi: 10.1007\/3-540-15670-4_19"},{"issue":"2","key":"11_CR17","doi-asserted-by":"crossref","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. Sci. Comput. Program. 19(2), 87\u2013152 (1992)","journal-title":"Sci. Comput. Program."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Berry, G., Kishinevsky, M., Singh, S.: System level design and verification using a synchronous language. In: Proceedings of International Conference on Integrated Circuit Design, ICCAD 2003, San Jose, USA (2004)","DOI":"10.1109\/ICCAD.2003.159720"},{"key":"11_CR19","unstructured":"Berry, G., Moisan, S., Rigault, J.-P.: Towards a synchronous and semantically sound high level language for real-time applications. In: IEEE Real Time Systems Symposium, pp. 30\u201340 (1983). IEEE Catalog 83 CH 1941\u20134"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Berry, G., Serrano, M., Hop, H.: Multitier web orchestration. In: Proceedings of the ICDCIT 2014 Conference, pp. 1\u201313 (2014)","DOI":"10.1007\/978-3-319-04483-5_1"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Bertin, P., Roncin, D., Vuillemin, J.: Programmable active memories: a performance assessment. In: Borriello, G., Ebeling, C. (eds.) Research on Integrated Systems: Proceedings of the 1993 Symposium, pp. 88\u2013102 (1993)","DOI":"10.1007\/3-540-56731-3_12"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development- Coq\u2019Art: The Calculus of Inductive Constructions. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI 2003 ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, San Diego, California, USA, pp. 196\u2013207 (2003)","DOI":"10.1145\/781131.781153"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Bouali, A.: Xeve: an Esterel verification environment. In: Proceedings of Computer Aided Verification, CAV 1998, Vancouver, Canada (1998)","DOI":"10.1007\/BFb0028770"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-662-46663-6_4","volume-title":"Compiler Construction","author":"T Bourke","year":"2015","unstructured":"Bourke, T., Cola\u00e7o, J.-L., Pagano, B., Pasteur, C., Pouzet, M.: A synchronous-based code generator for explicit hybrid systems languages. In: Franke, B. (ed.) CC 2015. LNCS, vol. 9031, pp. 69\u201388. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46663-6_4"},{"issue":"4","key":"11_CR26","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1002\/spe.4380210406","volume":"21","author":"F Boussinot","year":"1991","unstructured":"Boussinot, F., Reactive, C.: An extension of C to program reactive systems. Softw. Pract. Exp. 21(4), 401\u2013428 (1991)","journal-title":"Softw. Pract. Exp."},{"key":"11_CR27","first-page":"1293","volume":"79","author":"F Boussinot","year":"1991","unstructured":"Boussinot, F., de Simone, R.: The Esterel language. Another Look Real Time Programm. Proc. IEEE 79, 1293\u20131304 (1991)","journal-title":"Another Look Real Time Programm. Proc. IEEE"},{"issue":"8","key":"11_CR28","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Cola\u00e7o, J.-L., Pagano, B., Pouzet, M.: A conservative extension of synchronous data-flow with state machines. In: Proceedings of Emsoft 2005, New Jersey, USA (2005)","DOI":"10.1145\/1086228.1086261"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Cola\u00e7o, J.-L., Girault, A., Hamon, G., Pouzet, M.: Towards a higher-order synchronous data-flow language. In :ACM Fourth International Conference on Embedded Software, EMSOFT 2004, Pisa, Italy, September 2004","DOI":"10.1145\/1017753.1017792"},{"key":"11_CR31","doi-asserted-by":"crossref","first-page":"974","DOI":"10.1109\/TPAMI.2009.106","volume":"32","author":"A Cont","year":"2010","unstructured":"Cont, A.: A coupled duration-focused architecture for real-time music-to-score alignment. IEEE Trans. Pattern Anal. Mach. Intell. 32, 974\u2013987 (2010)","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."},{"issue":"4","key":"11_CR32","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/s10626-013-0166-2","volume":"23","author":"J Echeveste","year":"2013","unstructured":"Echeveste, J., Cont, A., Giavitto, J.-L., Jacquemard, F.: Operational semantics of a domain specific language for real time musician-computer interaction. Discrete Event Dyn. Syst. 23(4), 343\u2013383 (2013)","journal-title":"Discrete Event Dyn. Syst."},{"issue":"2","key":"11_CR33","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1109\/43.980257","volume":"2","author":"S Edwards","year":"2002","unstructured":"Edwards, S.: An Esterel compiler for large control-dominated systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 2(2), 169\u2013183 (2002)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Espiau, B., Coste-Mani\u00e8re, E.: A synchronous approach for control sequencing in robotics applications, pp. 503\u2013508. In: Proceedings of IEEE International Workshop on Intelligent Motion, Istambul (1990)","DOI":"10.1109\/IMC.1990.687369"},{"issue":"9","key":"11_CR35","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L Moura De","year":"2011","unstructured":"De Moura, L., Bjrner, N.: Satisfiability modulo theories: introduction and applications. Comm. ACM 54(9), 69\u201377 (2011)","journal-title":"Comm. ACM"},{"key":"11_CR36","doi-asserted-by":"crossref","first-page":"1270","DOI":"10.1109\/5.97297","volume":"79","author":"P Guernic Le","year":"1991","unstructured":"Le Guernic, P., Le Borgne, M., Gauthier, T., Le Maire, C.: Programming real time applications with Signal. Another Look Real Time Programm. Proc. IEEE 79, 1270\u20131282 (1991). Special Issue","journal-title":"Proc. IEEE"},{"key":"11_CR37","doi-asserted-by":"crossref","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, Dordrecht (1993)"},{"key":"11_CR38","doi-asserted-by":"crossref","first-page":"1270","DOI":"10.1109\/5.97300","volume":"79","author":"N Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Pilaud, D.: The synchronous dataflow programming language Lustre. Another Look Real Time Programm. Proc. IEEE 79, 1270\u20131282 (1991). Special Issue","journal-title":"Proc. IEEE"},{"key":"11_CR39","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual approach to complex systems. Sci. Comput. Program. 8, 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"11_CR40","volume-title":"The e-Hardware Verification Language","author":"S Iman","year":"2004","unstructured":"Iman, S., Joshi, S.: The e-Hardware Verification Language. Springer, Heidelberg (2004)"},{"issue":"2","key":"11_CR41","first-page":"132","volume":"8","author":"L Jagadeesan","year":"1996","unstructured":"Jagadeesan, L., Von Olnhausen, J., Puchol, C.: A formal approach to reactive system software: a telecommunications application in Esterel. J. Formal Methods Syst. Des. 8(2), 132\u2013145 (1996)","journal-title":"J. Formal Methods Syst. Des."},{"key":"11_CR42","unstructured":"Knuth, D.: The Art of Computer Programming, Vol. 4: Combinatorial Algorithms, Section 7.1.4: Binary Decision Diagrams. Addison Wesley, Reading (2014)"},{"key":"11_CR43","unstructured":"Knuth, D.: The Art of Computer Programming, vol. 4B, 7.2.2.2: Satisfiability. Addison Wesley, Reading (2016)"},{"key":"11_CR44","unstructured":"Kroening, D., Strichman, O.: Decision Procedures An Algorithmic Point of View. Springer (2008)"},{"issue":"7","key":"11_CR45","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"7","key":"11_CR46","doi-asserted-by":"crossref","first-page":"950","DOI":"10.1109\/43.293952","volume":"13","author":"S Malik","year":"1994","unstructured":"Malik, S.: Analysis of cyclic combinational circuits. IEEE Trans. Comput. Aided Des. 13(7), 950\u2013956 (1994)","journal-title":"IEEE Trans. Comput. Aided Des."},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"Mandel, L., Pouzet, M.: ReactiveML, a reactive extension to ML. In: Proceedings of Principles and Practice of Declarative Programming, PPDP 2005, Lisbon (2005)","DOI":"10.1145\/1069774.1069782"},{"issue":"3","key":"11_CR48","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/S0167-6423(02)00093-X","volume":"46","author":"F Maraninchi","year":"2003","unstructured":"Maraninchi, F., R\u00e9mond, Y.: Mode automata: a new domain-specific construct for the development of safe critical systems. Sci. Comput. Programm. 46(3), 219\u2013254 (2003)","journal-title":"Sci. Comput. Programm."},{"issue":"3","key":"11_CR49","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s10703-012-0144-6","volume":"40","author":"M Mendler","year":"2012","unstructured":"Mendler, M., Shiple, T., Berry, G.: Constructive Boolean circuits and the exactness of timed ternary simulation. Formal Methods Syst. Des. 40(3), 283\u2013329 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"11_CR50","unstructured":"Murakami, G., Sethi, R.: Terminal call processing in Esterel. In: Proceedings of IFIP 92 World Computer Congress, Madrid, Spain (1992)"},{"key":"11_CR51","volume-title":"Compiling Esterel","author":"D Potop-Butucaru","year":"2007","unstructured":"Potop-Butucaru, D., Edwards, S.A., Berry, G.: Compiling Esterel. Springer, Heidelberg (2007)"},{"key":"11_CR52","doi-asserted-by":"crossref","unstructured":"Pouzet, M.: Building a hybrid systems modeler on synchronous languages principles. In: Proceedings of ACM International Conference on Embedded Software (EMSOFT), Amsterdam (2015)","DOI":"10.1109\/EMSOFT.2015.7318267"},{"key":"11_CR53","doi-asserted-by":"crossref","unstructured":"Roy, V., de Simone, R.: Auto and autograph. In: Kurshan, R. (ed.) Proceedings of Workshop on Computer Aided Verification, New-Brunswick, June 1990","DOI":"10.1090\/dimacs\/003\/29"},{"key":"11_CR54","doi-asserted-by":"crossref","unstructured":"Schneider, K.: Embedding imperative synchronous languages in interactive theorem provers. In: Proceedings of Conference on Application of Concurrency to System Design (ACSD) (2001)","DOI":"10.1109\/CSD.2001.981772"},{"key":"11_CR55","doi-asserted-by":"crossref","unstructured":"Sentovich, E., Toma, H., Berry, G.: Latch optimization in circuits generated from high-level descriptions. In: Proceedings of International Conference on Computer-Aided Design (ICCAD) (1996)","DOI":"10.1109\/ICCAD.1996.569833"},{"key":"11_CR56","doi-asserted-by":"crossref","unstructured":"Sentovich, E., Toma, H., Berry, G.: Efficient latch optimization using exclusive sets. In: Proceedings of Digital Automation Conference (DAC) (1997)","DOI":"10.1109\/DAC.1997.597108"},{"issue":"8","key":"11_CR57","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1145\/2240236.2240253","volume":"55","author":"M Serrano","year":"2012","unstructured":"Serrano, M., Berry, G.: Multitier programming in Hop - a first step toward programming 21st-century applications. Commun. ACM 55(8), 53\u201359 (2012)","journal-title":"Commun. ACM"},{"key":"11_CR58","doi-asserted-by":"crossref","unstructured":"Serrano, M., Prunet, V.: A glimpse of Hopjs. In: 21th Sigplan International Conference on Functional Programming (ICFP), Nara, Japan (2016)","DOI":"10.1145\/2951913.2951916"},{"key":"11_CR59","doi-asserted-by":"crossref","unstructured":"Shiple, T., Berry, G., Touati, H.: Constructive analysis of cyclic circuits. In: Proceedings of International Design and Testing Conf (ITDC), Paris (1996)","DOI":"10.1109\/EDTC.1996.494321"},{"key":"11_CR60","unstructured":"Touati, H., Berry, G.: Optimized controller synthesis using Esterel. In: Proceedings of International Workshop on Logic Synthesis IWLS 1993, Lake Tahoe (1993)"},{"key":"11_CR61","unstructured":"von Hanxleden, R., Duderstadt, B., Motika, C., Smyth, S., Mendler, M., Aguado, J., Mercer, S., OBrien, O.: SCCharts: Sequentially constructive statecharts for safety-critical applications. In: Proceedings ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI14), Edinburgh, UK, (2014)"},{"key":"11_CR62","doi-asserted-by":"crossref","unstructured":"von Hanxleden, R., Mendler, M., Aguado, J., Duderstadt, B., Fuhrmann, I., Motika, C., Mercer, S., O\u2019Brien, O.: Sequentially constructive concurrency - a conservative extension of the synchronous model of computation. In: Proceedings of Design, Automation and Test in Europe Conference, DATE 2013, Grenoble, France (2013)","DOI":"10.7873\/DATE.2013.128"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47169-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,19]],"date-time":"2024-06-19T19:25:49Z","timestamp":1718825149000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47169-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471686","9783319471693"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}