A Metamodel-Based Approach for Adding Modularization to KeYmaera’s Input Syntax

Abstract

The theorem prover KeYmaera allows (1) to describe Cyber-Physical Systems (CPSs) in terms of a Hybrid Program (HP), (2) to specify properties for the defined system, and (3) to formally verify these properties using a tailored logic called Differential Dynamic Logic (DDL). The syntax of Hybrid Programs is rather poor and covers only the most basic program statements, such as assignment, test, sequential execution, and iteration. The decision to keep the syntax of HPs very simple has different consequences: An advantage is that also the verification calculus can be kept relatively simple. On the downside we have that even small programs are hard to understand and that the programmer is forced to program using a copy-and-paste style, which obviously hampers maintenance. The most significant drawback, however, is the absence of modularization and a library concept; making the development and verification of bigger systems a huge burden. In this paper, we identify several problems of KeYmaera’s input syntax and illustrate them with examples. To overcome these problems, we first describe the original syntax in form of a metamodel. Then, we propose to extend this metamodel with established programming concepts such as subprogram and abrupt termination. We illustrate our extensions by using a new graphical concrete syntax. Examples from a recent KeYmaera tutorial serve for our paper as illustration examples.