License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WCET.2014.1
URN: urn:nbn:de:0030-drops-45996
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4599/
Go to the corresponding OASIcs Volume Portal

Lisper, Björn

Principles for Value Annotation Languages

pdf-format:
2.pdf (0.4 MB)

Abstract

Tools for code-level program analysis need formats to express various properties, like relevant properties of the environment where the analysed code will execute, and the analysis results. Different WCET analysis tools typically use tool-specific annotation languages for this purpose. These languages are often geared towards expressing properties that the particular tool can handle rather than being general, and mostly their semantics is only specified informally. This makes it harder for tools to communicate, as well as for users to provide relevant information to them. Here, we propose a small but general assertion language for value constraints including IPET flow facts, which is an important class of annotations for WCET analysis tools. We show how to express interesting properties in this language, we propose some syntactic conveniences, and we give the language a formal semantics. The language could be used directly as a tool-independent annotation language, or as a meta-language to give exact semantics to existing value annotation and flow fact formats.

BibTeX - Entry

@InProceedings{lisper:OASIcs:2014:4599,
  author =	{Bj{\"o}rn Lisper},
  title =	{{Principles for Value Annotation Languages}},
  booktitle =	{14th International Workshop on Worst-Case Execution Time Analysis},
  pages =	{1--10},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-69-9},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{39},
  editor =	{Heiko Falk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4599},
  URN =		{urn:nbn:de:0030-drops-45996},
  doi =		{10.4230/OASIcs.WCET.2014.1},
  annote =	{Keywords: Real-Time System, WCET analysis, Flow Fact, Assertion}
}

Keywords: Real-Time System, WCET analysis, Flow Fact, Assertion
Collection: 14th International Workshop on Worst-Case Execution Time Analysis
Issue Date: 2014
Date of publication: 08.07.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI