@article{cit:nonstd_sem_hyb_sys_mod, title = {Non-standard semantics of hybrid systems modelers}, journal = {Journal of Computer and System Sciences}, volume = {78}, number = {3}, pages = {877-910}, year = {2012}, note = {In Commemoration of Amir Pnueli}, issn = {0022-0000}, doi = {https://doi.org/10.1016/j.jcss.2011.08.009}, url = {https://www.sciencedirect.com/science/article/pii/S0022000011001061}, author = {Albert Benveniste and Timothy Bourke and Benoît Caillaud and Marc Pouzet}, keywords = {Hybrid systems, Hybrid systems modelers, Non-standard analysis, Non-standard semantics, Constructive semantics, Kahn process networks, Compilation of hybrid systems}, abstract = {Hybrid system modelers have become a corner stone of complex embedded system development. Embedded systems include not only control components and software, but also physical devices. In this area, Simulink is a de facto standard design framework, and Modelica a new player. However, such tools raise several issues related to the lack of reproducibility of simulations (sensitivity to simulation parameters and to the choice of a simulation engine). In this paper we propose using techniques from non-standard analysis to define a semantic domain for hybrid systems. Non-standard analysis is an extension of classical analysis in which infinitesimal (the ε and η in the celebrated generic sentence ∀ε∃η… of college maths) can be manipulated as first class citizens. This approach allows us to define both a denotational semantics, a constructive semantics, and a Kahn Process Network semantics for hybrid systems, thus establishing simulation engines on a sound but flexible mathematical foundation. These semantics offer a clear distinction between the concerns of the numerical analyst (solving differential equations) and those of the computer scientist (generating execution schemes). We also discuss a number of practical and fundamental issues in hybrid system modelers that give rise to non-reproducibility of results, non-determinism, and undesirable side effects. Of particular importance are cascaded mode changes (also called “zero-crossings” in the context of hybrid systems modelers).}, } @inbook{cit:op_sem_hyb_sys, series = {Lecture Notes in Computer Science}, title = {Operational Semantics of Hybrid Systems}, volume = {3414}, ISBN = {978-3-540-25108-8}, url = {http://link.springer.com/10.1007/978-3-540-31954-2_2}, DOI = {10.1007/978-3-540-31954-2_2}, abstractNote = {This paper discusses an interpretation of hybrid systems as executable models. A specification of a hybrid system for this purpose can be viewed as a program in a domain-specific programming language. We describe the semantics of HyVisual, which is such a domain-specific programming language. The semantic properties of such a language affect our ability to understand, execute, and analyze a model. We discuss several semantic issues that come in defining such a programming language, such as the interpretation of discontinuities in continuous-time signals, and the interpretation of discrete-event signals in hybrid systems, and the consequences of numerical ODE solver techniques. We describe the solution in HyVisual by giving its operational semantics. }, booktitle = {Hybrid Systems: Computation and Control}, publisher = {Springer Berlin Heidelberg}, author = {Lee, Edward A. and Zheng, Haiyang}, editor = {Morari, Manfred and Thiele, Lothar}, year = {2005}, pages = {25–53}, collection = {Lecture Notes in Computer Science}, language = {en}, } @inproceedings{cit:zelus_sync_lng_with_ode, address = {Philadelphia Pennsylvania USA}, title = {Zélus: a synchronous language with ODEs}, ISBN = {978-1-4503-1567-8}, url = {https://dl.acm.org/doi/10.1145/2461328.2461348}, DOI = {10.1145/2461328.2461348}, abstractNote = { Z´elus is a new programming language for modeling systems that mix discrete logical time and continuous time behaviors. From a user’s perspective, its main originality is to extend an existing Lustre-like synchronous language with Ordinary Differential Equations (ODEs). The extension is conservative: any synchronous program expressed as dataflow equations and hierarchical automata can be composed arbitrarily with ODEs in the same source code. }, booktitle = { Proceedings of the 16th international conference on Hybrid systems: computation and control }, publisher = {ACM}, author = {Bourke, Timothy and Pouzet, Marc}, year = {2013}, month = apr, pages = {113–118}, language = {en}, } @inbook{cit:sync_based_codegen_hyb_sys_lng, address = {Berlin, Heidelberg}, series = {Lecture Notes in Computer Science}, title = {A Synchronous-Based Code Generator for Explicit Hybrid Systems Languages}, volume = {9031}, rights = {http://www.springer.com/tdm}, ISBN = {978-3-662-46662-9}, url = {http://link.springer.com/10.1007/978-3-662-46663-6_4}, DOI = {10.1007/978-3-662-46663-6_4}, abstractNote = {Modeling languages for hybrid systems are cornerstones of embedded systems development in which software interacts with a physical environment. Sequential code generation from such languages is important for simulation efficiency and for producing code for embedded targets. Despite being routinely used in industrial compilers, code generation is rarely, if ever, described in full detail, much less formalized. Yet formalization is an essential step in building trustable compilers for critical embedded software development.}, booktitle = {Compiler Construction}, publisher = {Springer Berlin Heidelberg}, author = {Bourke, Timothy and Colaço, Jean-Louis and Pagano, Bruno and Pasteur, Cédric and Pouzet, Marc}, editor = {Franke, Björn}, year = {2015}, pages = {69–88}, collection = {Lecture Notes in Computer Science}, language = {en}, } @article{cit:alg_ana_hyb_sys, title = {The algorithmic analysis of hybrid systems}, author = {Alur, Rajeev and Courcoubetis, Costas and Halbwachs, Nicolas and Henzinger, Thomas A and Ho, P-H and Nicollin, Xavier and Olivero, Alfredo and Sifakis, Joseph and Yovine, Sergio}, journal = {Theoretical Computer Science}, volume = {138}, number = {1}, pages = {3--34}, year = {1995}, publisher = {Elsevier}, } @inproceedings{cit:lustre, title = {LUSTRE: A declarative language for programming synchronous systems}, author = {Pilaud, Daniel and Halbwachs, N and Plaice, J.A.}, booktitle = {Proceedings of the 14th Annual ACM Symposium on Principles of Programming Languages (14th POPL 1987). ACM, New York, NY}, volume = {178}, pages = {188}, year = {1987}, organization = {Citeseer}, } @article{cit:sundials, title = {SUNDIALS: Suite of nonlinear and differential/algebraic equation solvers}, author = {Hindmarsh, Alan C and Brown, Peter N and Grant, Keith E and Lee, Steven L and Serban, Radu and Shumaker, Dan E and Woodward, Carol S }, journal = {ACM Transactions on Mathematical Software (TOMS)}, volume = {31}, number = {3}, pages = {363--396}, year = {2005}, publisher = {ACM New York, NY, USA}, } @inproceedings{cit:sundialsml, title = {Sundials/ML: interfacing with numerical solvers}, author = {Bourke, Timothy and Inoue, Jun and Pouzet, Marc}, booktitle = {ACM Workshop on ML}, year = {2016}, } @book{cit:theory_timed_io_automata, address = {Cham}, series = {Synthesis Lectures on Distributed Computing Theory}, title = {The Theory of Timed I/O Automata}, rights = {https://www.springernature.com/gp/researchers/text-and-data-mining }, ISBN = {978-3-031-00875-7}, url = {https://link.springer.com/10.1007/978-3-031-02003-2}, DOI = {10.1007/978-3-031-02003-2}, abstractNote = {This monograph presents the Timed Input/Output Automaton (TIOA) modeling framework, a basic mathematical framework to support description and analysis of timed (computing) systems. Timed systems are systems in which desirable correctness or performance properties of the system depend on the timing of events, not just on the order of their occurrence. Timed systems are employed in a wide range of domains including communications, embedded systems, real-time operating systems, and automated control. Many applications involving timed systems have strong safety, reliability and predictability requirements, which makes it important to have methods for systematic design of systems and rigorous analysis of timing-dependent behavior. An important feature of the TIOA framework is its support for decomposing timed system descriptions. In particular, the framework includes a notion of external behavior for a timed I/O automaton, which captures its discrete interactions with its environment. The framework also defines what it means for one TIOA to implement another, based on an inclusion relationship between their external behavior sets, and defines notions of simulations, which provide sufficient conditions for demonstrating implementation relationships. The framework includes a composition operation for TIOAs, which respects external behavior, and a notion of receptiveness, which implies that a TIOA does not block the passage of time.}, publisher = {Springer International Publishing}, author = {Kaynar, Dilsun K. and Lynch, Nancy and Segala, Roberto and Vaandrager, Frits}, year = {2011}, collection = {Synthesis Lectures on Distributed Computing Theory}, language = {en}, } @article{cit:illinois, title = {Inverse interpolation, a real root of f (x)= 0}, author = {Snyder, J.N.}, journal = {University of Illinois Digital Computer Laboratory, ILLIAC I Library Routine H1-71}, volume = {4}, year = {1953}, }