{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T22:35:47Z","timestamp":1777761347728,"version":"3.51.4"},"reference-count":175,"publisher":"Emerald","issue":"1-2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006,2,15]]},"abstract":"<jats:p>The explosive growth of embedded electronics is bringing information and control systems of increasing complexity to every aspects of our lives. The most challenging designs are safety-critical systems, such as transportation systems (e.g., airplanes, cars, and trains), industrial plants and health care monitoring. The difficulties reside in accommodating constraints both on functionality and implementation. The correct behavior must be guaranteed under diverse states of the environment and potential failures; implementation has to meet cost, size,and power consumption requirements. The design is therefore subject to extensive mathematical analysis and simulation. However, traditional models of information systems do not interface well to the continuous evolving nature of the environment in which these devices operate.Thus, in practice, different mathematical representations have to be mixed to analyze the overall behavior of the system. Hybrid systems are a particular class of mixed models that focus on the combination of discrete and continuous subsystems. There is a wealth of tools and languages that have been proposed over the years to handle hybrid systems. However, each tool makes different assumptions on the environment, resulting in somewhat different notions of hybrid system. This makes it difficult to share information among tools. Thus, the community cannot maximally leverage the substantial amount of work that has been directed to this important topic. In this paper, we review and compare hybrid system tools by highlighting their differences in terms of their underlying semantics, expressive power and mathematical mechanisms. We conclude our review with a comparative summary, which suggests the need for a unifying approach to hybrid systems design. As a step in this direction, we make the case for a semantic-aware inter-change format, which would enable the use of joint techniques, make a formal comparison between different approaches possible, and facilitate exporting and importing design representations.<\/jats:p>","DOI":"10.1561\/1000000001","type":"journal-article","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T09:18:43Z","timestamp":1153819123000},"page":"1-193","source":"Crossref","is-referenced-by-count":92,"title":["Languages and Tools for Hybrid Systems Design"],"prefix":"10.1108","volume":"1","author":[{"given":"Luca P.","family":"Carloni","sequence":"first","affiliation":[{"name":"Department of Computer Science, Columbia University , 1214 Amsterdam Avenue, Mail Code 0401, New York, NY 10027,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Passerone","sequence":"additional","affiliation":[{"name":"Cadence Berkeley Laboratories , 1995 University Ave Suite 460, Berkeley, CA 94704,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Pinto","sequence":"additional","affiliation":[{"name":"Department of EECS, University of California at Berkeley , Berkeley, CA 94720,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[{"name":"Department of EECS, University of California at Berkeley , Berkeley, CA 94720,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"140","published-online":{"date-parts":[[2006,2,15]]},"reference":[{"key":"2026041711534341900_ref001","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","article-title":"Model checking in dense real time","volume":"104","author":"Alur","year":"1993","journal-title":"Information and Computation"},{"key":"2026041711534341900_ref002","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","article-title":"The algorithmic analysis of hybrid systems","volume":"138","author":"Alur","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"2026041711534341900_ref003","first-page":"14","article-title":"Hierarchical hybrid modeling of embedded systems","volume-title":"EMSOFT 2001: Embedded Software, First International Workshop","author":"Alur","year":"2001"},{"key":"2026041711534341900_ref004","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/JPROC.2002.805817","article-title":"Hierarchical modeling and analysis of embedded systems","volume":"91","author":"Alur","year":"2003","journal-title":"Proceedings of the IEEE"},{"key":"2026041711534341900_ref005","first-page":"289","article-title":"A framework and architecture for multirobot coordination","volume-title":"Proc. ISER00, 7th Intl. Symp. on Experimental Robotics","author":"Alur","year":"2000"},{"key":"2026041711534341900_ref006","first-page":"390","article-title":"Modular refinement of hierarchic reactive machines","volume-title":"Principles of Programming Languages","author":"Alur","year":"2000"},{"key":"2026041711534341900_ref007","first-page":"390","article-title":"Modular refinement of hierarchic reactive machines","volume-title":"Proc. of the 27th Annual ACM Symp. on Principles of Programming Languages","author":"Alur","year":"2000"},{"key":"2026041711534341900_ref008","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1007\/3-540-46430-1_5","article-title":"Modular specification of hybrid systems in Charon","volume-title":"Proc. of the Third Intl. Workshop on Hybrid Systems: Computation and Control","author":"Alur","year":"2000"},{"key":"2026041711534341900_ref009","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/3-540-63141-0_6","article-title":"Modularity for timed and hybrid systems","volume-title":"CONCUR \u201997: International Conference on Concurrency Theory","author":"Alur","year":"1997"},{"key":"2026041711534341900_ref010","first-page":"2","article-title":"Automatic symbolic verification of embedded systems","volume-title":"Proc. of the 14th Annual Real-time Systems Symp.","author":"Alur","year":"1993"},{"key":"2026041711534341900_ref011","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","article-title":"Automatic symbolic verification of embedded systems","volume":"22","author":"Alur","year":"1996","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2026041711534341900_ref012","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0020931","volume-title":"Hybrid Systems III: Verification and Control, Proceedings of the DIMACS\/SYCON Workshop, October 22-25, 1995, Rutgers University, New Brunswick, NJ, USA","author":"Alur","year":"1996"},{"key":"2026041711534341900_ref013","first-page":"5","article-title":"Polyhedral flows in hybrid automata","volume-title":"HSCC \u201999: Proceedings of the Second International Workshop on Hybrid Systems","author":"Alur","year":"1999"},{"key":"2026041711534341900_ref014","volume-title":"Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27","author":"Alur","year":"2004"},{"key":"2026041711534341900_ref015","volume-title":"MATLAB, Simulink, Stateflow: grundlagen, toolboxen, beispiele (MATLAB, Simulink, Stateflow: fundamentals, toolboxes, examples)","author":"Angermann","year":"2003"},{"key":"2026041711534341900_ref016","article-title":"SHIFT and Smart AHS: A language for hybrid system engineering modeling and simulation","volume-title":"Proceedings of the Conference on Domain-Specific Languages","author":"Antoniotti","year":"1997"},{"key":"2026041711534341900_ref017","doi-asserted-by":"crossref","DOI":"10.1109\/JPROC.2000.871299","article-title":"Special issue on hybrid systems: Theory and applications","volume":"88","author":"Antsaklis","year":"2000","journal-title":"Proceedings of the IEEE"},{"key":"2026041711534341900_ref018","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60472-3","volume-title":"Hybrid Systems II","author":"Antsaklis","year":"1995"},{"key":"2026041711534341900_ref019","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0031551","volume-title":"Hybrid Systems IV","author":"Antsaklis","year":"1997"},{"key":"2026041711534341900_ref020","doi-asserted-by":"crossref","DOI":"10.1109\/TAC.1998.664148","article-title":"Hybrid control systems, special issue","volume":"43","author":"Antsaklis","year":"1998","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026041711534341900_ref021","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/3-540-46430-1_6","article-title":"Approximate reachability analysis of piecewise linear dynamical systems","volume-title":"HSCC 00: Hybrid Systems\u2014Computation and Control","author":"Asarin","year":"2000"},{"key":"2026041711534341900_ref022","doi-asserted-by":"crossref","first-page":"1011","DOI":"10.1109\/5.871306","article-title":"Effective synthesis of switching controllers for linear systems","volume":"88","author":"Asarin","year":"2000","journal-title":"Proceedings of the IEEE"},{"key":"2026041711534341900_ref023","first-page":"2893","article-title":"d\/dt: A verification tool for hybrid systems","volume-title":"Proc. of the 40th IEEE Conf. on Decision and Control","author":"Asarin","year":"2001"},{"key":"2026041711534341900_ref024","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","article-title":"The d\/dt tool for verification of hybrid systems","volume-title":"Proc. of the 14th Intl. Conf. on Computer-Aided Verification","author":"Asarin","year":"2002"},{"key":"2026041711534341900_ref025","doi-asserted-by":"crossref","unstructured":"R.\n              Bagnara\n            , E.Ricci, E.Zaffanella, and P. M.Hill, \u201cPossibly not closed convex polyhedra and the Parma Polyhedra Library,\u201d 2002.","DOI":"10.1007\/3-540-45789-5_17"},{"key":"2026041711534341900_ref026","first-page":"45","article-title":"Metropolis: An integrated design environment for electronic system design","volume":"36","author":"Balarin","year":"2003","journal-title":"IEEE Micro"},{"key":"2026041711534341900_ref027","doi-asserted-by":"crossref","unstructured":"F.\n              Balarin\n            , L.Lavagno, C.Passerone, A.Sangiovanni-Vincentelli, M.Sgroi, and Y.Watanabe, \u201cModeling and designing heterogeneous systems,\u201d Tech. Rep. 2002\/01, Cadence Berkeley Laboratories, January2002.","DOI":"10.1007\/3-540-36190-1_7"},{"key":"2026041711534341900_ref028","article-title":"Ariadne: A framework for reachability analysis of hybrid automata","volume-title":"17th International Symposium on Mathematical Theory of Networks and Systems (MTNS)","author":"Balluchi","year":"2006"},{"key":"2026041711534341900_ref029","first-page":"1190","article-title":"Piecewise linear optimal controllers for hybrid systems","volume-title":"American Control Conference","author":"Bemporad","year":"2000"},{"key":"2026041711534341900_ref030","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/3-540-45873-5_11","article-title":"On the optimal control law for linear discrete time hybrid systems","volume-title":"International Workshop on Hybrid Systems: Computation and Control","author":"Bemporad","year":"2002"},{"key":"2026041711534341900_ref031","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1016\/S0005-1098(98)00178-2","article-title":"Control of systems integrating logic, dynamics, and constraints","volume":"35","author":"Bemporad","year":"1999","journal-title":"Automatica"},{"key":"2026041711534341900_ref032","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/BFb0020949","article-title":"UPPAAL\u2014a tool suite for automatic verification of real-time systems","volume-title":"Hybrid Systems III","author":"Bengtsson","year":"1996"},{"key":"2026041711534341900_ref033","doi-asserted-by":"crossref","first-page":"579","DOI":"10.1109\/9.664162","article-title":"Compositional and uniform modelling of hybrid systems","volume":"43","author":"Benveniste","year":"1998","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026041711534341900_ref034","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1109\/9.53519","article-title":"Hybrid dynamical systems theory and the signal language","volume":"35","author":"Benveniste","year":"1990","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026041711534341900_ref035","article-title":"Taxis = Esterel + Kronos: A tool for verifying real-time properties of embedded systems","volume-title":"Proc. of the 40th IEEE Conf. on Decision and Control","author":"Bertin","year":"2001"},{"key":"2026041711534341900_ref036","volume-title":"The Art of the Metaobject Protocol","author":"Bobrow","year":"1991"},{"key":"2026041711534341900_ref037","article-title":"Common Lisp object specification","volume":"1","author":"Bobrow","year":"1989","journal-title":"Lisp and Symbolic Computation"},{"key":"2026041711534341900_ref038","volume-title":"Unified Modeling Language User Guide","author":"Booch","year":"1997"},{"key":"2026041711534341900_ref039","first-page":"73","article-title":"Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations","volume-title":"HSCC","author":"Botchkarev","year":"2000"},{"key":"2026041711534341900_ref040","first-page":"46","article-title":"Orthogonal polyhedra: representation and computation","volume-title":"HSCC \u201999: Proceedings of the Second International Workshop on Hybrid Systems","author":"Bournez","year":"1999"},{"key":"2026041711534341900_ref041","doi-asserted-by":"crossref","first-page":"546","DOI":"10.1007\/BFb0028779","article-title":"Kronos: A model-checking tool for real-time systems","volume-title":"Proc. of the 10th Intl. Conf. on Computer-Aided Verification","author":"Bozga","year":"1998"},{"issue":"2","key":"2026041711534341900_ref042","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 10^20 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Information and Computation"},{"key":"2026041711534341900_ref043","unstructured":"L. P.\n              Carloni\n            , M.Di Benedetto, R.Passerone, A.Pinto, and A.Sangiovanni-Vincentelli, \u201cModeling techniques, programming languages and design toolsets for hybrid systems,\u201d Tech. Rep., IST - Columbus Project, 2004."},{"key":"2026041711534341900_ref044","first-page":"2322","article-title":"Improving reachability analysis of hybrid automata for engine control","volume-title":"Proc. of CDC 2004, 44th IEEE Conference on Decision and Control","author":"Casagrande","year":"2004"},{"key":"2026041711534341900_ref045","first-page":"84","article-title":"Translating discrete-time Simulink to Lustre","volume-title":"Proc. of the Third Intl. Conf. on Embedded Software (EMSOFT)","author":"Caspi","year":"2003"},{"key":"2026041711534341900_ref046","unstructured":"A.\n              Chutinan\n            \n          , Hybrid system verification using discrete model approximations, PhD thesis, Carnegie Mellon University, 1999."},{"key":"2026041711534341900_ref047","doi-asserted-by":"crossref","DOI":"10.1109\/CDC.1998.758642","article-title":"Computing polyhedral approximations to flow pipes for dynamic systems","volume-title":"37th IEEE Conf. on Decision and Control","author":"Chutinan","year":"1998"},{"key":"2026041711534341900_ref048","article-title":"Design and synthesis of synchronization skeletons using branching-time temporal logic","volume-title":"Workshop on Logic of Programs","author":"Clarke","year":"1981"},{"key":"2026041711534341900_ref049","volume-title":"Model Checking","author":"Clarke","year":"2000"},{"key":"2026041711534341900_ref050","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44585-4_39","article-title":"Taxys: A tool for the development and verification real-time embedded systems","volume-title":"Proc. of the 13th Intl. Conf. on Computer-Aided Verification","author":"Closse","year":"2001"},{"key":"2026041711534341900_ref051","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1016\/j.tcs.2005.05.001","article-title":"Continuity and computability of reachable sets","volume":"341","author":"Collins","year":"2005","journal-title":"Theoretical Computer Science"},{"key":"2026041711534341900_ref052","volume-title":"Mastering Simulink","author":"Dabney","year":"2003"},{"key":"2026041711534341900_ref053","unstructured":"T.\n              Dang\n            \n          , Verification and synthesis of hybrid systems, PhD thesis, INPG, 2000."},{"key":"2026041711534341900_ref054","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/3-540-64358-3_34","article-title":"Reachability analysis via face lifting","volume-title":"HSCC 98: Hybrid Systems\u2014Computation and Control","author":"Dang","year":"1998"},{"key":"2026041711534341900_ref055","first-page":"208","article-title":"A Tool architecture for the next generation of UPPAAL","volume-title":"Proceedings of UNU\/IIST 10th Anniversary Colloquium: Formal Methods at the Crossroads","author":"David","year":"2002"},{"key":"2026041711534341900_ref056","unstructured":"J.\n              Davis\n            , M.Goel, C.Hylands, B.Kienhuis, E. A.Lee, J.Liu, X.Liu, L.Muliadi, S.Neuendorffer, J.Reekie, N.Smyth, J.Tsay, and Y.Xiong, \u201cOverview of the Ptolemy project,\u201d Tech. Rep. UCB\/ERL M99\/37, Univ. of California at Berkeley, 1999."},{"key":"2026041711534341900_ref057","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/BFb0020947","article-title":"The tool Kronos","volume-title":"Hybrid Systems III","author":"Daws","year":"1996"},{"key":"2026041711534341900_ref058","unstructured":"A.\n              Deshpande\n            , D.Godbole, A.Gollu, L.Semenzato, R.Sengupta, D.Swaroop, and P.Varaiya, \u201cAutomated highway system tool interface format,\u201d California PATH Technical Report, January1996."},{"key":"2026041711534341900_ref059","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0020941","article-title":"Design and evaluation tools for automated highway systems","volume-title":"Hybrid Systems III","author":"Deshpande","year":"1996"},{"key":"2026041711534341900_ref060","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/BFb0031558","article-title":"Shift: A formalism and a programming language for dynamic networks of hybrid automata","volume-title":"Hybrid Systems IV","author":"Deshpande","year":"1997"},{"key":"2026041711534341900_ref061","doi-asserted-by":"crossref","first-page":"584","DOI":"10.1109\/9.664163","article-title":"The SHIFT programming language for dynamic networks of hybrid automata","volume":"43","author":"Deshpande","year":"1998","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026041711534341900_ref062","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60472-3_7","article-title":"Viable control of hybrid systems","volume-title":"Hybrid Systems II","author":"Deshpande","year":"1995"},{"key":"2026041711534341900_ref063","volume-title":"Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001","author":"Di Benedetto","year":"2001"},{"key":"2026041711534341900_ref064","first-page":"74","article-title":"From hybrid simulation to real-time implementation","volume-title":"ESS\u201999 11th European Simulation Symposium and Exhibition","author":"Djenidi","year":"1999"},{"key":"2026041711534341900_ref065","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1109\/5.558710","article-title":"Design of embedded systems: Formal models, validation and synthesis","volume":"85","author":"Edwards","year":"1997","journal-title":"Proceedings of the IEEE"},{"key":"2026041711534341900_ref066","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1109\/JPROC.2002.805829","article-title":"Taming heterogeneity\u2014The Ptolemy approach","volume":"91","author":"Eker","year":"2003","journal-title":"Proceedings of the IEEE"},{"key":"2026041711534341900_ref067","unstructured":"H.\n              Elmqvist\n            \n          , \u201cDymola - user\u2019s manual,\u201d DynaSim AB, Research Park Ideon, Lund, Sweden, 1993."},{"issue":"1","key":"2026041711534341900_ref068","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0968-090X(94)00013-U","article-title":"Design and evaluation tools for automated highway systems","volume":"3","author":"Eskafi","year":"1995","journal-title":"Transportation Research - C"},{"key":"2026041711534341900_ref069","first-page":"258","article-title":"PHAVer: Algorithmic verification of hybrid systems past HyTech","volume-title":"HSCC","author":"Frehse","year":"2005"},{"key":"2026041711534341900_ref070","volume-title":"Principles of Object-oriented Modeling and Simulation with Modelica 2.1","author":"Fritzson","year":"2004"},{"key":"2026041711534341900_ref071","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/BFb0054087","article-title":"Modelica - a unified object-oriented language for system modeling and simulation","volume-title":"ECCOP \u201998: Proc. of the 12th Eur. Conf. on Object-Oriented Programming","author":"Fritzson","year":"1998"},{"key":"2026041711534341900_ref072","doi-asserted-by":"crossref","DOI":"10.1109\/CDC.2005.1582904","article-title":"Approximate bisimulations for constrained linear systems","volume-title":"Proc. of the 44th IEEE Conf. on Decision and Control","author":"Girard","year":"2005"},{"key":"2026041711534341900_ref073","doi-asserted-by":"crossref","DOI":"10.1109\/CDC.2005.1582235","article-title":"Approximate bisimulations for nonlinear dynamical systems","volume-title":"Proc. of the 44th IEEE Conf. on Decision and Control","author":"Girard","year":"2005"},{"key":"2026041711534341900_ref074","doi-asserted-by":"crossref","DOI":"10.1109\/CDC.1995.478835","article-title":"Design and verification of communication protocols for degraded modes of operation of AHS","volume-title":"Conference on Decision and Control","author":"Godbole","year":"1995"},{"key":"2026041711534341900_ref075","unstructured":"A.\n              Gollu\n            \n          , Object management systems, PhD thesis, UC Berkeley, 1995."},{"key":"2026041711534341900_ref076","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/S0895-7177(98)00054-5","article-title":"Smart AHS: A simulation framework for automated vehicles and highway systems","volume":"27","author":"Gollu","year":"1998","journal-title":"Mathematical and Computer Modeling"},{"key":"2026041711534341900_ref077","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1584-4","volume-title":"Engineering and Scientific Computing with Scilab","author":"Gomez","year":"1999"},{"key":"2026041711534341900_ref078","first-page":"74","article-title":"Optimized rapid prototyping for real-time embedded heterogeneous multiprocessors","volume-title":"Proc. of CODES \u201999","author":"Grandpierre","year":"1999"},{"key":"2026041711534341900_ref079","doi-asserted-by":"crossref","DOI":"10.1109\/MEMCOD.2003.1210097","article-title":"From algorithm and architecture specifications to automatic generation of distributed real-time executives: A seamless flow of graphs transformations","volume-title":"MEMOCODE2003, Formal Methods and Models for Codesign Conference","author":"Grandpierre","year":"2003"},{"key":"2026041711534341900_ref080","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-57318-6","volume-title":"Hybrid systems","author":"Grossman","year":"1993"},{"key":"2026041711534341900_ref081","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BFb0020943","article-title":"Verification of hybrid systems: monotonicity in the AHS control system","volume-title":"Proceedings of the DIMACS\/SYCON workshop on Hybrid systems III : verification and control","author":"Haddon","year":"1996"},{"key":"2026041711534341900_ref082","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2231-4","volume-title":"Synchronous Programming of Reactive Systems","author":"Halbwachs","year":"1993"},{"key":"2026041711534341900_ref083","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/3-540-58485-4_43","article-title":"Verification of linear hybrid systems by means of convex approximation","volume-title":"SAS 94: Static Analysis Symposium","author":"Halbwachs","year":"1994"},{"key":"2026041711534341900_ref084","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","article-title":"Statecharts: A visual formalism for complex systems","volume":"8","author":"Harel","year":"1987","journal-title":"Science of Computer Programming"},{"key":"2026041711534341900_ref085","doi-asserted-by":"crossref","first-page":"1085","DOI":"10.1016\/S0005-1098(01)00059-0","article-title":"Equivalence of hybrid dynamical models","volume":"37","author":"Heemels","year":"2001","journal-title":"Automatica"},{"key":"2026041711534341900_ref086","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-60472-3_13","volume-title":"Hybrid Systems II","author":"Henzinger","year":"1995"},{"key":"2026041711534341900_ref087","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"Henzinger","year":"1995"},{"key":"2026041711534341900_ref088","first-page":"41","volume-title":"TACAS 95","author":"Henzinger","year":"1995"},{"key":"2026041711534341900_ref089","doi-asserted-by":"crossref","first-page":"540","DOI":"10.1109\/9.664156","article-title":"Algorithmic analysis of nonlinear hybrid systems","volume":"43","author":"Henzinger","year":"1998","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"2","key":"2026041711534341900_ref090","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","article-title":"Symbolic model checking for real-time systems","volume":"111","author":"Henzinger","year":"1994","journal-title":"Information and Computation"},{"key":"2026041711534341900_ref091","first-page":"2886","article-title":"Some lessons from the HyTech experience","volume-title":"Proc. of the 40th IEEE Conf. on Decision and Control","author":"Henzinger","year":"2001"},{"key":"2026041711534341900_ref092","first-page":"278","article-title":"The theory of hybrid automata","volume-title":"Logic in Computer Science","author":"Henzinger","year":"1996"},{"key":"2026041711534341900_ref093","first-page":"549","article-title":"Masaccio: A formal model for embedded components","volume-title":"Theoretical Computer Science","author":"Henzinger","year":"2000"},{"key":"2026041711534341900_ref094","article-title":"Model checking strategies for linear hybrid systems","volume-title":"Workshop on Hybrid Systems and Autonomous Control","author":"Henzinger","year":"1994"},{"issue":"1-2","key":"2026041711534341900_ref095","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","article-title":"HyTech: A model checker for hybrid systems","volume":"1","author":"Henzinger","year":"1997","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2026041711534341900_ref096","first-page":"373","article-title":"What\u2019s decidable about hybrid automata?","volume-title":"Proc. 27th Annual ACM Symp. on Theory of Computing (STOC)","author":"Henzinger","year":"1995"},{"key":"2026041711534341900_ref097","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/3-540-45351-2_24","article-title":"Assume-guarantee reasoning for hierarchical hybrid systems","volume-title":"HSCC 01: Hybrid Systems\u2014Computation and Control","author":"Henzinger","year":"2001"},{"key":"2026041711534341900_ref098","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-64358-3","volume-title":"Hybrid Systems: Computation and Control, First International Workshop, HSCC\u201998","author":"Henzinger","year":"1998"},{"key":"2026041711534341900_ref099","volume-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"issue":"5","key":"2026041711534341900_ref100","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The Model Checker SPIN","volume":"23","author":"Holzmann","year":"1997","journal-title":"Software Engineering"},{"key":"2026041711534341900_ref101","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1109\/AIHAS.1994.390475","article-title":"The DEVS formalism: A framework for logical analysis and performance","volume-title":"Fifth Annual Conference on AI, Simulation and Planning in High Autonomy Systems","author":"Hong","year":"1994"},{"key":"2026041711534341900_ref102","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF01797158","article-title":"Protocol design for an automated highway system","author":"Hsu","year":"1993","journal-title":"Discrete Event Dynamic Systems"},{"key":"2026041711534341900_ref103","unstructured":"C.\n              Hylands\n            , E. A.Lee, J.Liu, X.Liu, S.Neuendorffer, and H.Zheng, \u201cHyVisual: A hybrid system visual modeler\u201d,Tech. Rep.UCB\/ERL M03\/1, UC Berkeley, 2003.available at ptolemy.eecs.berkeley.edu\/hyvisual\/"},{"key":"2026041711534341900_ref104","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1109\/9.1271","article-title":"Finitely recursive process models for discrete-event systems","volume":"33","author":"Inan","year":"1988","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026041711534341900_ref105","unstructured":"Specification and description language SDL, 1988."},{"key":"2026041711534341900_ref106","unstructured":"Estelle - A formal description technique based on extended state transition model."},{"key":"2026041711534341900_ref107","unstructured":"J.\n              Jang\n            , R.Teo, and C.Tomlin, \u201cEmbedded software design for the Stanford DragonFly UAV\u201d,Tech. Rep.,2002."},{"key":"2026041711534341900_ref108","article-title":"Design and implementation of a low cost hierarchical avionics architecture","volume-title":"AIAA Guidance, Navigation, and Control Conference","author":"Jang","year":"2002"},{"key":"2026041711534341900_ref109","doi-asserted-by":"crossref","first-page":"1523","DOI":"10.1109\/43.898830","article-title":"System level design","volume":"19","author":"Keutzer","year":"2000","journal-title":"IEEE Transactions on CAD"},{"key":"2026041711534341900_ref110","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0277-6","volume-title":"Ellipsoidal Calculus for Estimation and Control","author":"Kurzhanski","year":"1997"},{"key":"2026041711534341900_ref111","first-page":"202","article-title":"Ellipsoidal techniques for reachability analysis","volume-title":"HSCC 00","author":"Kurzhanski","year":"2000"},{"key":"2026041711534341900_ref112","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/S0167-6911(00)00059-1","article-title":"Ellipsoidal techniques for reachability analysis: Internal approximation","volume":"41","author":"Kurzhanski","year":"2000","journal-title":"Systems and Control Letters"},{"key":"2026041711534341900_ref113","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1080\/1055678021000012426","article-title":"On ellipsoidal techniques for reachability analysis","volume":"17","author":"Kurzhanski","year":"2000","journal-title":"Optimization Methods and Software"},{"issue":"2","key":"2026041711534341900_ref114","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1080\/1055678021000012426","article-title":"On ellipsoidal techniques for reachability analysis - Part I: external approximations","volume":"17","author":"Kurzhanski","year":"2002","journal-title":"Optimization Methods and Software"},{"issue":"2","key":"2026041711534341900_ref115","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1080\/1055678021000012435","article-title":"On ellipsoidal techniques for reachability analysis - Part II: internal approximations based-valued constraints","volume":"17","author":"Kurzhanski","year":"2002","journal-title":"Optimization Methods and Software"},{"issue":"3","key":"2026041711534341900_ref116","first-page":"347","article-title":"Reachability analysis for uncertain systems - the ellipsoidal technique","volume":"9","author":"Kurzhanski","year":"2002","journal-title":"Dynamics of Continuous, Discrete and Impulsive Systems"},{"key":"2026041711534341900_ref117","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/10984413_12","article-title":"Ellipsoidal techniques for hybrid dynamics: the reachability problem","volume-title":"New Directions and Applications in Control Theory","author":"Kurzhanski","year":"2005"},{"key":"2026041711534341900_ref118","doi-asserted-by":"crossref","first-page":"4682","DOI":"10.1109\/CDC.2005.1582901","article-title":"On verification of controlled hybrid dynamics through ellipsoidal techniques","volume-title":"44th IEEE Conference on Decision and Control","author":"Kurzhanski","year":"2005"},{"key":"2026041711534341900_ref119","article-title":"Ellipsoidal techniques for reachability analysis of discrete-time linear systems","author":"Kurzhanskiy","year":"2005","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026041711534341900_ref120","doi-asserted-by":"crossref","unstructured":"A. A.\n              Kurzhanskiy\n             and P.Varaiya, Ellipsoidal toolbox - technical report, University of California, Berkeley, www.eecs.berkeley.edu\/~akurzhan\/ellipsoids, 2006.","DOI":"10.1109\/CDC.2006.377036"},{"key":"2026041711534341900_ref121","first-page":"448","article-title":"Multi-parametric toolbox (MPT)","volume-title":"HSCC","author":"Kvasnica","year":"2004"},{"key":"2026041711534341900_ref122","first-page":"137","article-title":"A new class of decidable hybrid systems","volume-title":"HSCC \u201999","author":"Lafferriere","year":"1999"},{"key":"2026041711534341900_ref123","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the correctness of multiprocess programs","volume":"2","author":"Lamport","year":"1977","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2026041711534341900_ref124","unstructured":"L.\n              Lavagno\n            , J.Moondanos, T.Meyerowitz, and Y.Watanabe, \u201cModeling of architectural resources in Metropolis\u201d,2002."},{"key":"2026041711534341900_ref125","first-page":"239","article-title":"Concurrent models of computation for embedded software","volume":"153","author":"Lee","year":"2005","journal-title":"IEE Proceedings"},{"key":"2026041711534341900_ref126","doi-asserted-by":"crossref","first-page":"1217","DOI":"10.1109\/43.736561","article-title":"A framework for comparing models of computation","volume":"17","author":"Lee","year":"1998","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"2026041711534341900_ref127","first-page":"237","article-title":"System-level types for component-based design","volume-title":"EMSOFT 2001","author":"Lee","year":"2001"},{"key":"2026041711534341900_ref128","first-page":"25","article-title":"Operational semantics of hybrid systems","volume-title":"HSCC","author":"Lee","year":"2005"},{"key":"2026041711534341900_ref129","doi-asserted-by":"crossref","DOI":"10.1016\/S0005-1098(98)00193-9","article-title":"Controllers for reachability specifications for hybrid systems","volume-title":"Automatica, Special Issue on Hybrid Systems","author":"Lygeros","year":"1999"},{"key":"2026041711534341900_ref130","doi-asserted-by":"crossref","first-page":"496","DOI":"10.1007\/BFb0020971","article-title":"Hybrid I\/O automata","volume-title":"Hybrid Systems III: Verification and Control","author":"Lynch","year":"1996"},{"key":"2026041711534341900_ref131","volume-title":"Hybrid Systems: Computation and Control, Third International Workshop, HSCC 2000","author":"Lynch","year":"2000"},{"key":"2026041711534341900_ref132","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0014706","volume-title":"Hybrid and Real-Time Systems, HART\u201997 Proceedings","author":"Maler","year":"1997"},{"key":"2026041711534341900_ref133","first-page":"447","article-title":"From timed to hybrid systems","volume-title":"Real-Time: Theory in Practice, REX Workshop","author":"Maler","year":"1991"},{"key":"2026041711534341900_ref134","volume-title":"Hybrid Systems: Computation and Control, HSCC 2003","author":"Maler","year":"2003"},{"key":"2026041711534341900_ref135","unstructured":"Matisse,\u201cAvailable at wiki.grasp.upenn.edu\/~graspdoc\/hst\/."},{"key":"2026041711534341900_ref136","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"McMillan","year":"1993"},{"key":"2026041711534341900_ref137","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"Milner","year":"1980"},{"key":"2026041711534341900_ref138","unstructured":"MoBIES Group,\u201cHSIF syntax (version 3)\u201d,2002."},{"key":"2026041711534341900_ref139","unstructured":"Modelica Association,\u201cModelica - A unified object-oriented language for physical systems modeling\u201d,2000."},{"key":"2026041711534341900_ref140","volume-title":"Hybrid Systems: Computation and Control, HSCC 2005","author":"Morari","year":"2005"},{"key":"2026041711534341900_ref141","article-title":"On the normal component of centralized frictionless collision sequences","author":"Mosterman","year":"2005","journal-title":"ASME Journal of Applied Mechanics"},{"key":"2026041711534341900_ref142","unstructured":"S.\n              Neema\n            \n          , \u201cAnalysis of Matlab Simulink and Stateflow data model\u201d,2001."},{"key":"2026041711534341900_ref143","unstructured":"R.\n              Nikoukhah\n             and S.Steer, \u201cSCICOS - a dynamic system builder and simulator user\u2019s guide\u201d,1997."},{"key":"2026041711534341900_ref144","first-page":"491","article-title":"Interchange formats for hybrid systems: Abstract semantics","volume-title":"HSCC 2006","author":"Pinto","year":"2006"},{"key":"2026041711534341900_ref145","first-page":"526","article-title":"Interchange formats for hybrid systems: Review and proposal","volume-title":"HSCC 2005","author":"Pinto","year":"2005"},{"key":"2026041711534341900_ref146","first-page":"3597","article-title":"Driving safely in smart cars","volume-title":"American Control Conference","author":"Puri","year":"1995"},{"key":"2026041711534341900_ref147","first-page":"573","article-title":"Safety verification of hybrid systems by constraint propagation based abstraction refinement","volume-title":"HSCC","author":"Ratschan","year":"2005"},{"key":"2026041711534341900_ref148","volume-title":"MATLAB Simulink Stateflow avec des Exercices","author":"Rivoire","year":"2001"},{"key":"2026041711534341900_ref149","unstructured":"A. L.\n              Sangiovanni-Vincentelli\n            \n          , \u201cDefining platform-based design,\u201d; in EEDesign. Available at www.eedesign.com\/story\/OEG20020204S0062February2002."},{"key":"2026041711534341900_ref150","unstructured":"L.\n              Semenzato\n            , A.Deshpande, and A.Gollu, \u201cShift reference manual\u201d,1996."},{"key":"2026041711534341900_ref151","first-page":"323","article-title":"Modeling and verifying hybrid dynamic systems using CheckMate","volume-title":"4th International Conference on Automation of Mixed Processes","author":"Silva","year":"2000"},{"key":"2026041711534341900_ref152","first-page":"2867","article-title":"An assessment of the current status of algorithmic approaches to the verification of hybrid systems","volume-title":"40th IEEE Conference on Decision and Control","author":"Silva","year":"2001"},{"key":"2026041711534341900_ref153","unstructured":"T.\n              Simsek\n            \n          , \u201cSHIFT tutorial: A first course for SHIFT programmers\u201d,1999."},{"key":"2026041711534341900_ref154","unstructured":"T.\n              Simsek\n            \n          , \u201cThe A-SHIFT specification language for dynamic networks of hybrid automata\u201d,2000."},{"key":"2026041711534341900_ref155","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1109\/TAC.1981.1102596","article-title":"Nonlinear regulation: the piecewise linear approach","volume":"26","author":"Sontag","year":"1981","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026041711534341900_ref156","first-page":"44","article-title":"Massively parallel computing systems with real time constraints - the Algorithm Architecture Adequation methodology","volume-title":"Massively Parallel Computing Systems Conference","author":"Sorel","year":"1994"},{"key":"2026041711534341900_ref157","volume-title":"Common Lisp: The Language","author":"Steele","year":"1990"},{"key":"2026041711534341900_ref158","doi-asserted-by":"crossref","DOI":"10.1109\/CDC.2002.1184274","article-title":"Decentralized overlapping control of a formation of unmanned aerial vehicles","volume-title":"41st IEEE Conference on Decision and Control","author":"Stipanovic","year":"2002"},{"issue":"9-10","key":"2026041711534341900_ref159","first-page":"1097","article-title":"Block-diagram based modelling and analysis of hybrid processes under discrete control","volume":"32","author":"Stursberg","year":"1998","journal-title":"Journal Europeen des Systemes Automatises"},{"key":"2026041711534341900_ref160","unstructured":"The Metropolis Project Team,\u201cThe Metropolis meta model version 0.4\u201d,2004."},{"key":"2026041711534341900_ref161","unstructured":"The University of Pennsylvania MoBIES Group,\u201cHSIF semantics (version 3, synchronous edition)\u201d,2002."},{"key":"2026041711534341900_ref162","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-1561-6","volume-title":"Introduction to physical modeling with Modelica","author":"Tiller","year":"2001"},{"key":"2026041711534341900_ref163","volume-title":"Hybrid Systems: Computation and Control, HSCC 2002","author":"Tomlin","year":"2002"},{"key":"2026041711534341900_ref164","first-page":"2899","article-title":"Discrete-time hybrid modeling and verification","volume-title":"40th IEEE Conference on Decision and Control","author":"Torrisi","year":"2001"},{"key":"2026041711534341900_ref165","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1109\/TCST.2004.824309","article-title":"HYSDEL - a tool for generating computational hybrid models","volume":"12","author":"Torrisi","year":"2004","journal-title":"IEEE Transactions on Control Systems Technology"},{"key":"2026041711534341900_ref166","unstructured":"F. D.\n              Torrisi\n            , A.Bemporad, G.Bertini, P.Hertach, D.Jost, and D.Mignone, \u201cHysdel 2.0.5 - user manual\u201d,2002."},{"key":"2026041711534341900_ref167","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/BFb0014994","article-title":"A compositional semantics for Statecharts","volume-title":"Concurrency Theory","author":"Uselton","year":"1994"},{"key":"2026041711534341900_ref168","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-48983-5","volume-title":"Hybrid Systems: Computation and Control, HSCC\u201999","author":"Vaandrager","year":"1999"},{"key":"2026041711534341900_ref169","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1109\/9.250509","article-title":"Smart cars on smart roads: problems of control","volume":"38","author":"Varaiya","year":"1993","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2026041711534341900_ref170","article-title":"Reach set computation using optimal control","volume-title":"KIT Workshop on Verification of Hybrid Systems","author":"Varaiya","year":"1998"},{"key":"2026041711534341900_ref171","unstructured":"S. M.\n              Veres\n            \n          , User\u2019s manual - geometric bounding toolbox, 2004."},{"key":"2026041711534341900_ref172","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-56999-9","volume-title":"Computable Analysis - An Introduction","author":"Weihrauch","year":"2000"},{"key":"2026041711534341900_ref173","volume-title":"The Mathematica Book","author":"Wolfram","year":"2003"},{"key":"2026041711534341900_ref174","unstructured":"XML,\u201csee http:\/\/www.w3.org\/XML\/\u201d.www.w3.org\/XML\/"},{"key":"2026041711534341900_ref175","volume-title":"Multifaceted Modeling and Discrete Event Simulation","author":"Zeigler","year":"1984"}],"container-title":["Foundations and Trends\u00ae in Electronic Design Automation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/fteda\/article-pdf\/1\/1-2\/1\/11526623\/1000000001en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/fteda\/article-pdf\/1\/1-2\/1\/11526623\/1000000001en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T14:13:37Z","timestamp":1777472017000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/fteda\/article\/1\/1-2\/1\/1360498\/Languages-and-Tools-for-Hybrid-Systems-Design"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,2,15]]},"references-count":175,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2006,2,15]]}},"URL":"https:\/\/doi.org\/10.1561\/1000000001","relation":{},"ISSN":["1551-3939","1551-3947"],"issn-type":[{"value":"1551-3939","type":"print"},{"value":"1551-3947","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,2,15]]}}}