WG211/M10Hermann

Multi-Level DSLs with a co-design of code generation and analysis/verification by Christoph Herrmann

The aim of this approach is to obtain precise information
about properties of program-controlled systems in terms
of input parameters. The language constructs are assigned
to different levels of abstraction.
Code generation transforms a program at one level to a
program at the next lower level. The lowest level has a
direct correspondence to a machine operation in a general
sense, e.g. an instruction of a concrete or virtual
processor, a command to an actuator or a request from a
sensor.
Program analysis uses the information at one level to
obtain the information at the next higher level; and
this involves the semantics of the transformation between
the levels. The information will necessarily be expressed
in terms of parameters, to account for data-dependent
case distinctions or iteration counts. The crucial point
in the design methodology is that the properties for which
the system is to be analysed/verified are stated before
the design and that only language constructs are introduced
that permit the analysis/verification of all these
properties. Depending on how these properties depend on
run-time information the complexity of language constructs
will be limited.
In the first example I will report about the formal
verification in Agda that a robot can move from one location
to another in a certain time given as an expression in terms
of start and final location. Although it will be simple
to obtain such a formula by an analysis, the verification
in Agda ties the result to the semantics of the translation.
In the second example I will sketch the design of a system
of collaborating autonomous vehicles, in which the language
levels deal with
(1) global strategic planning,
(2) execution of a plan by an arbitrary vehicle, and
(3) operational implemention of an execution step.
With the proposed design methodology it will be possible to
develop quite complex systems that allow for an analysis
of important properties such as execution time or energy
consumption and include these results into the planning
process.