*banner
 

Operational Semantics of Hybrid Systems
Haiyang Zheng

Citation
Haiyang Zheng. "Operational Semantics of Hybrid Systems". PhD thesis, University of California, Berkeley, May, 2007.

Abstract
Hybrid systems are heterogeneous systems that include continuous-time (CT) subsystems interacting with discrete-event (DE) subsystems. They are effective models for physical systems interacting with software or experiencing discrete mode changes.

This dissertation discusses an interpretation of hybrid systems as executable programs written in a programming language with a hybrid system semantics. The semantic properties of such a programming language affect our ability to understand, execute, and analyze a hybrid system model. This dissertation focuses on a few semantic issues that come in defining such a programming language, such as the interpretation of discontinuities in CT signals and simultaneous discrete events in DE signals, liveness property, and the consequences of numerical ODE solver techniques.

The interactions between CT and DE subsystems and between DE subsystems themselves are captured by discontinuities in continuous-time signals and simultaneous discrete events in discrete-event signals. In order to precisely represent them in compute execution results, a two-dimension domain, called ``super-dense time," is used as the domain for defining signals. This domain allows a signal to have multiple values at the same time point while keeping the values ordered.

CT and DE subsystems are modeled as actors, which are functions that map a set of signals to another set of signals. In this way, a hybrid system model is just a network of actors interacting via signals. We can always transform a network of actors into a composite actor with feedback, where the function of the composition actor is the composition of functions of the component actors. The least fixed point solution to the function of the composite actor, which is a set of signals, gives the denotational semantics of the hybrid system model.

The operational semantics takes the denotational semantics as a mathematical foundation and defines a set of rules for evaluating actors such that the least fixed point solution can be constructed. Rather than constructing the whole signals, the operational semantics only computes a discrete subset of the signals called a discrete representation of the signals. The constructive procedure is formalized with the Abstract State Machine semantics, where a hybrid system is treated as a state transition system and the rules specify how state transformations are performed.

This operational semantics supports heterogeneous and hierarchical composition of different models of computation, such as CT, DE, finite state machines, and synchronous languages, and modular execution of the composition as a whole. This ability makes it easy to jointly model and design software controlled systems.

The operational semantics proposed in this dissertation has been implemented in HyVisual, which is a software tool for modeling and simulating hybrid systems. HyVisual is part of the Ptolemy II software framework, which is available in open-source form at http://ptolemy.org.

Electronic downloads

Citation formats  
  • HTML
    Haiyang Zheng. <a
    href="http://chess.eecs.berkeley.edu/pubs/303.html"
    ><i>Operational Semantics of Hybrid
    Systems</i></a>, PhD thesis,  University of
    California, Berkeley, May, 2007.
  • Plain text
    Haiyang Zheng. "Operational Semantics of Hybrid
    Systems". PhD thesis,  University of California,
    Berkeley, May, 2007.
  • BibTeX
    @phdthesis{Zheng07_OperationalSemanticsOfHybridSystems,
        author = {Haiyang Zheng},
        title = {Operational Semantics of Hybrid Systems},
        school = {University of California, Berkeley},
        month = {May},
        year = {2007},
        abstract = {Hybrid systems are heterogeneous systems that
                  include continuous-time (CT) subsystems
                  interacting with discrete-event (DE) subsystems.
                  They are effective models for physical systems
                  interacting with software or experiencing discrete
                  mode changes. <p>This dissertation discusses an
                  interpretation of hybrid systems as executable
                  programs written in a programming language with a
                  hybrid system semantics. The semantic properties
                  of such a programming language affect our ability
                  to understand, execute, and analyze a hybrid
                  system model. This dissertation focuses on a few
                  semantic issues that come in defining such a
                  programming language, such as the interpretation
                  of discontinuities in CT signals and simultaneous
                  discrete events in DE signals, liveness property,
                  and the consequences of numerical ODE solver
                  techniques. <p>The interactions between CT and DE
                  subsystems and between DE subsystems themselves
                  are captured by discontinuities in continuous-time
                  signals and simultaneous discrete events in
                  discrete-event signals. In order to precisely
                  represent them in compute execution results, a
                  two-dimension domain, called ``super-dense time,"
                  is used as the domain for defining signals. This
                  domain allows a signal to have multiple values at
                  the same time point while keeping the values
                  ordered. <p>CT and DE subsystems are modeled as
                  actors, which are functions that map a set of
                  signals to another set of signals. In this way, a
                  hybrid system model is just a network of actors
                  interacting via signals. We can always transform a
                  network of actors into a composite actor with
                  feedback, where the function of the composition
                  actor is the composition of functions of the
                  component actors. The least fixed point solution
                  to the function of the composite actor, which is a
                  set of signals, gives the denotational semantics
                  of the hybrid system model. <p>The operational
                  semantics takes the denotational semantics as a
                  mathematical foundation and defines a set of rules
                  for evaluating actors such that the least fixed
                  point solution can be constructed. Rather than
                  constructing the whole signals, the operational
                  semantics only computes a discrete subset of the
                  signals called a discrete representation of the
                  signals. The constructive procedure is formalized
                  with the Abstract State Machine semantics, where a
                  hybrid system is treated as a state transition
                  system and the rules specify how state
                  transformations are performed. <p>This operational
                  semantics supports heterogeneous and hierarchical
                  composition of different models of computation,
                  such as CT, DE, finite state machines, and
                  synchronous languages, and modular execution of
                  the composition as a whole. This ability makes it
                  easy to jointly model and design software
                  controlled systems. <p>The operational semantics
                  proposed in this dissertation has been implemented
                  in HyVisual, which is a software tool for modeling
                  and simulating hybrid systems. HyVisual is part of
                  the Ptolemy II software framework, which is
                  available in open-source form at
                  http://ptolemy.org.},
        URL = {http://chess.eecs.berkeley.edu/pubs/303.html}
    }
    

Posted by Christopher Brooks on 7 Jun 2007.
Groups: ptolemy
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess