http://mw.hh.se/wg211/index.php?action=history&feed=atom&title=WG211%2FM10HermannWG211/M10Hermann - Revision history2026-04-05T23:09:52ZRevision history for this page on the wikiMediaWiki 1.43.5http://mw.hh.se/wg211/index.php?title=WG211/M10Hermann&diff=35&oldid=prevAdmin: 1 revision2011-12-12T10:06:23Z<p>1 revision</p>
<p><b>New page</b></p><div>[[Category:WG211]]<br />
<br />
<br />
<br />
<strong>Multi-Level DSLs with a co-design of code generation and analysis/verification</strong> by Christoph Herrmann<br />
<br />
The aim of this approach is to obtain precise information <br />about properties of program-controlled systems in terms <br />of input parameters. The language constructs are assigned <br />to different levels of abstraction. <br />Code generation transforms a program at one level to a<br />program at the next lower level. The lowest level has a <br />direct correspondence to a machine operation in a general <br />sense, e.g. an instruction of a concrete or virtual <br />processor, a command to an actuator or a request from a <br />sensor. <br />Program analysis uses the information at one level to <br />obtain the information at the next higher level; and <br />this involves the semantics of the transformation between <br />the levels. The information will necessarily be expressed <br />in terms of parameters, to account for data-dependent <br />case distinctions or iteration counts. The crucial point<br />in the design methodology is that the properties for which<br />the system is to be analysed/verified are stated before <br />the design and that only language constructs are introduced <br />that permit the analysis/verification of all these <br />properties. Depending on how these properties depend on <br />run-time information the complexity of language constructs <br />will be limited. <br />In the first example I will report about the formal <br />verification in Agda that a robot can move from one location <br />to another in a certain time given as an expression in terms <br />of start and final location. Although it will be simple<br />to obtain such a formula by an analysis, the verification<br />in Agda ties the result to the semantics of the translation.<br />In the second example I will sketch the design of a system <br />of collaborating autonomous vehicles, in which the language <br />levels deal with <br />(1) global strategic planning, <br />(2) execution of a plan by an arbitrary vehicle, and<br />(3) operational implemention of an execution step.<br />With the proposed design methodology it will be possible to <br />develop quite complex systems that allow for an analysis <br />of important properties such as execution time or energy<br />consumption and include these results into the planning <br />process.</div>Admin