Graphical modeling tools have gained popularity within engineering communities, but such languages are known to suffer from lack of semantics and mathematical rigor. By supporting a graphical language with a textual language, and mapping graphical models to the textual language, one ensures proper unique semantics of the graphical language. In addition, some engineers prefer to express themselves in textual languages not unlike programming languages. This is in part due to the fact that it can be unnecessarily time-consuming to model graphically, and graphical models take up a considerable amount of visual space. As an example, the definition of a function in K may occupy one line of text, whereas in a graphical modeling language, it is not uncommon that such a specification may occupy one page. Finally, it is easier to provide analytical support for a textual language.
K is more specifically a textual formalism for representing SysML models. It is based on a merge of traditional formal specification languages such as Z and VDM, relational graphical formalisms such as SysML (UML), and modern high-level programming languages such as Scala. The idea is to combine modeling and programming in one language. The K language provides a capability for engineers to express their requirements and designs in one textual modeling language. The language is based on basic mathematical concepts such as predicate logic and set theory, concepts that should be familiar to engineers. The language is furthermore object-oriented, allowing for the definition of classes that can be arranged in a class hierarchy (inheritance). A class can contain named typed fields, functions, and constraints on the fields and the functions. The constraints are expressed using predicate logic. Fields and functions are defined over a type system, including basic types such as integers and Booleans, as well as structured types such as classes and collections (sets, lists, and maps). Functions can contain statements with side effects, making K a wide-spectrum development language, allowing for high-level specification as well as low-level programming all within one language.
The language is tied to visualization tools, which enable visualization of K models in a SysML style. One purpose of K is to support analysis of models. K is currently connected to a theorem prover, which allows formal reasoning about K models. This includes checking consistency of constraints, correctness of functions (against pre/post conditions), and program synthesis.
This work was done by Klaus Havelund, Rahul Kumar, Bradley J. Clement, and Christopher L. Delp of Caltech for NASA’s Jet Propulsion Laboratory. This software is available for license through the Jet Propulsion Laboratory, and you may request a license at: https://download.jpl.nasa.gov/ops/request/request_introduction.cfm . NPO-49865