Hyrose: A symbolic simulator of the hybrid constraint language HydLa

Shota Matsumoto, Kazunori Ueda

    Research output: Contribution to journalArticle

    1 Citation (Scopus)

    Abstract

    Hybrid systems are dynamical systems with continuous changes of states and discrete changes of states and governing equations. Hybrid systems are appliable to diverse fields including physics. HydLa is a declarative language for describing hybrid systems using constraints, and we have developed a symbolic simulator of HydLa named Hyrose. Hyrose is our first publicly available implementation of HydLa. Features of Hyrose include the simulation of systems with parameters, search based on automatic case analysis and bounded model checking. In this paper, we first describe the architecture and features of Hyrose, as well as semantical issues that had to be clarified to implement Hyrose. Then, in order to demonstrate the power of symbolic execution, we show several examples of the analysis of systems whose behavior exhibits quantitative and qualitative changes depending on parameters.

    Original languageEnglish
    Pages (from-to)18-35
    Number of pages18
    JournalComputer Software
    Volume30
    Issue number4
    Publication statusPublished - 2013 Nov

    Fingerprint

    Hybrid systems
    Simulators
    Phase transitions
    Model checking
    Dynamical systems
    Physics

    ASJC Scopus subject areas

    • Software

    Cite this

    Hyrose : A symbolic simulator of the hybrid constraint language HydLa. / Matsumoto, Shota; Ueda, Kazunori.

    In: Computer Software, Vol. 30, No. 4, 11.2013, p. 18-35.

    Research output: Contribution to journalArticle

    @article{db378adc56d7400ea39e19ff3e473839,
    title = "Hyrose: A symbolic simulator of the hybrid constraint language HydLa",
    abstract = "Hybrid systems are dynamical systems with continuous changes of states and discrete changes of states and governing equations. Hybrid systems are appliable to diverse fields including physics. HydLa is a declarative language for describing hybrid systems using constraints, and we have developed a symbolic simulator of HydLa named Hyrose. Hyrose is our first publicly available implementation of HydLa. Features of Hyrose include the simulation of systems with parameters, search based on automatic case analysis and bounded model checking. In this paper, we first describe the architecture and features of Hyrose, as well as semantical issues that had to be clarified to implement Hyrose. Then, in order to demonstrate the power of symbolic execution, we show several examples of the analysis of systems whose behavior exhibits quantitative and qualitative changes depending on parameters.",
    author = "Shota Matsumoto and Kazunori Ueda",
    year = "2013",
    month = "11",
    language = "English",
    volume = "30",
    pages = "18--35",
    journal = "Computer Software",
    issn = "0289-6540",
    publisher = "Japan Society for Software Science and Technology",
    number = "4",

    }

    TY - JOUR

    T1 - Hyrose

    T2 - A symbolic simulator of the hybrid constraint language HydLa

    AU - Matsumoto, Shota

    AU - Ueda, Kazunori

    PY - 2013/11

    Y1 - 2013/11

    N2 - Hybrid systems are dynamical systems with continuous changes of states and discrete changes of states and governing equations. Hybrid systems are appliable to diverse fields including physics. HydLa is a declarative language for describing hybrid systems using constraints, and we have developed a symbolic simulator of HydLa named Hyrose. Hyrose is our first publicly available implementation of HydLa. Features of Hyrose include the simulation of systems with parameters, search based on automatic case analysis and bounded model checking. In this paper, we first describe the architecture and features of Hyrose, as well as semantical issues that had to be clarified to implement Hyrose. Then, in order to demonstrate the power of symbolic execution, we show several examples of the analysis of systems whose behavior exhibits quantitative and qualitative changes depending on parameters.

    AB - Hybrid systems are dynamical systems with continuous changes of states and discrete changes of states and governing equations. Hybrid systems are appliable to diverse fields including physics. HydLa is a declarative language for describing hybrid systems using constraints, and we have developed a symbolic simulator of HydLa named Hyrose. Hyrose is our first publicly available implementation of HydLa. Features of Hyrose include the simulation of systems with parameters, search based on automatic case analysis and bounded model checking. In this paper, we first describe the architecture and features of Hyrose, as well as semantical issues that had to be clarified to implement Hyrose. Then, in order to demonstrate the power of symbolic execution, we show several examples of the analysis of systems whose behavior exhibits quantitative and qualitative changes depending on parameters.

    UR - http://www.scopus.com/inward/record.url?scp=84891817097&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=84891817097&partnerID=8YFLogxK

    M3 - Article

    AN - SCOPUS:84891817097

    VL - 30

    SP - 18

    EP - 35

    JO - Computer Software

    JF - Computer Software

    SN - 0289-6540

    IS - 4

    ER -