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

• broman-2011-mkl.pdf · application/pdf · 1219 kbytes

• 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.