*banner
 

Modeling Kernel Language (MKL) - A formal and extensible approach to
David Broman

Citation
David Broman. "Modeling Kernel Language (MKL) - A formal and extensible approach to". Talk or presentation, 17, February, 2011.

Abstract
Performing computational experiments on mathematical models instead of building and testing physical prototypes can drastically reduce the development cost for complex systems such as automobiles, aircraft, and powerplants. In the past three decades, a category of equation-based modeling languages has appeared that is based on acausal and object-oriented modeling principles, enabling good reuse of models. Examples of these languages are Modelica, VHDL-AMS, and gPROMS. However, the modeling languages within this category have grown to be large and complex, where the specifications of the language's semantics are informally defined, typically described in natural languages. The lack of a formal semantics makes these languages hard to interpret unambiguously and to reason about. In this talk a new research language called the Modeling Kernel Language (MKL) is presented. By introducing the concept of higher-order acausal models (HOAMs), we show that it is possible to create expressive modeling libraries in a manner analogous to Modelica, but using a small and simple language concept. In contrast to the current state-of-the-art modeling languages, the semantics of how to use the models, including meta operations on models, are also specified in MKL libraries. This enables extensible formal executable specifications where important language features are expressed through libraries rather than by adding completely new language constructs. MKL is a statically typed language based on a typed lambda calculus. We define the core of the language formally using operational semantics and prove type safety. An MKL interpreter is implemented and verified in comparison with a Modelica environment.

Electronic downloads

Citation formats  
  • HTML
    David Broman. <a
    href="http://chess.eecs.berkeley.edu/pubs/838.html"
    ><i>Modeling Kernel Language (MKL) - A formal and
    extensible approach to</i></a>, Talk or
    presentation,  17, February, 2011.
  • Plain text
    David Broman. "Modeling Kernel Language (MKL) - A
    formal and extensible approach to". Talk or
    presentation,  17, February, 2011.
  • BibTeX
    @presentation{Broman11_ModelingKernelLanguageMKLFormalExtensibleApproach,
        author = {David Broman},
        title = {Modeling Kernel Language (MKL) - A formal and
                  extensible approach to},
        day = {17},
        month = {February},
        year = {2011},
        abstract = {Performing computational experiments on
                  mathematical models instead of building and
                  testing physical prototypes can drastically reduce
                  the development cost for complex systems such as
                  automobiles, aircraft, and powerplants. In the
                  past three decades, a category of equation-based
                  modeling languages has appeared that is based on
                  acausal and object-oriented modeling principles,
                  enabling good reuse of models. Examples of these
                  languages are Modelica, VHDL-AMS, and gPROMS.
                  However, the modeling languages within this
                  category have grown to be large and complex, where
                  the specifications of the language's semantics are
                  informally defined, typically described in natural
                  languages. The lack of a formal semantics makes
                  these languages hard to interpret unambiguously
                  and to reason about. In this talk a new research
                  language called the Modeling Kernel Language (MKL)
                  is presented. By introducing the concept of
                  higher-order acausal models (HOAMs), we show that
                  it is possible to create expressive modeling
                  libraries in a manner analogous to Modelica, but
                  using a small and simple language concept. In
                  contrast to the current state-of-the-art modeling
                  languages, the semantics of how to use the models,
                  including meta operations on models, are also
                  specified in MKL libraries. This enables
                  extensible formal executable specifications where
                  important language features are expressed through
                  libraries rather than by adding completely new
                  language constructs. MKL is a statically typed
                  language based on a typed lambda calculus. We
                  define the core of the language formally using
                  operational semantics and prove type safety. An
                  MKL interpreter is implemented and verified in
                  comparison with a Modelica environment. },
        URL = {http://chess.eecs.berkeley.edu/pubs/838.html}
    }
    

Posted by Jan Reineke on 26 Apr 2011.
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