Document Open Access Logo

Principles for Value Annotation Languages

Author Björn Lisper

PDF
Thumbnail PDF

File

OASIcs.WCET.2014.1.pdf
  • Filesize: 384 kB
  • 10 pages

Document Identifiers

Author Details

Björn Lisper

Cite AsGet BibTex

Björn Lisper. Principles for Value Annotation Languages. In 14th International Workshop on Worst-Case Execution Time Analysis. Open Access Series in Informatics (OASIcs), Volume 39, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/OASIcs.WCET.2014.1

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.
Keywords
  • Real-Time System
  • WCET analysis
  • Flow Fact
  • Assertion

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Clément Ballabriga, Hugues Cassé, Christine Rochange, and Pascal Sainrat. OTAWA: An open toolbox for adaptive WCET analysis. In Proc. IFIP Workshop on Software Technologies for Future Embedded and Ubiquitous Systems (SEUS), pages 35-46. Springer, October 2010. Google Scholar
  2. Dines Bjørner and Cliff B. Jones, editors. The Vienna Development Method: the Meta-Language, number 61 in Lecture Notes in Comput. Sci. Springer-Verlag, 1978. Google Scholar
  3. Armelle Bonenfant, Hugues Cassé, Marianne de Michiel, Jens Knoop, Laura Kovács, and Jakob Zwirchmayr. FFX: A portable WCET annotation language. In Proc. 20th International Conference on Real-Time and Network Systems (RTNS'12), pages 91-100, New York, NY, USA, 2012. ACM. Google Scholar
  4. Marianne de Michiel, Armelle Bonenfant, Hugues Cassé, and Pascal Sainrat. Static loop bound analysis of C programs based on flow analysis and abstract interpretation. In Proc. IEEE Int. Conf. on Embedded and Real-Time Computing Systems and Applications (RTCSA'08), pages 161-168, Kaohsiung, Taiwan, August 2008. IEEE Computer Society. Google Scholar
  5. Christian Ferdinand, Reinhold Heckmann, and Bärbel Franzen. Static memory and timing analysis of embedded systems code. In 3rd European Symposium on Verification and Validation of Software Systems (VVSS'07), Eindhoven, The Netherlands, number 07-04 in TUE Computer Science Reports, pages 153-163, March 2007. Google Scholar
  6. Christian Ferdinand, Reinhold Heckmann, and Henrik Theiling. Convenient user annotations for a WCET tool. In Jan Gustafsson, editor, Proc. 3^rd International Workshop on Worst-Case Execution Time Analysis (WCET'03), Porto, July 2003. Google Scholar
  7. R. W. Floyd. Assigning meaning to programs. In J. T. Schwartz, editor, Proc. Symp. Applied Mathematics, vol. 19: Mathematical Aspects of Computer Science, pages 19-32, Providence, R.I., 1967. American Mathematical Society. Google Scholar
  8. C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(10):576-580, 583, October 1969. Google Scholar
  9. Niklas Holsti and Sami Saarinen. Status of the Bound-T WCET tool. In Proc. 2^nd International Workshop on Worst-Case Execution Time Analysis (WCET'02), 2002. Google Scholar
  10. Raimund Kirner. The WCET analysis tool CalcWcet167. In Tiziana Margaria and Bernhard Steffen, editors, Proc. 5^th International Symposium on Leveraging Applications of Formal Methods (ISOLA'12), Lecture Notes in Comput. Sci., Heraclion, Crete, October 2012. Springer-Verlag. Google Scholar
  11. Raimund Kirner, Jens Knoop, Adrian Prantl, Markus Schordan, and Albrecht Kadlec. Beyond loop bounds: comparing annotation languages for worst-case execution time analysis. Software &Systems Modeling, 10(3):411-437, 2011. Google Scholar
  12. Jens Knoop, Laura Kováćs, and Jakob Zwirchmayr. r-TuBound: Loop bounds for WCET analysis. In Nikolaj Bjørner and Andrei Voronkov, editors, Proc. Logic for Programming, Artificial Intelligence, and Reasoning, volume 7180 of Lecture Notes in Comput. Sci., pages 435-444. Springer, 2012. Google Scholar
  13. Bertrand Meyer. Applying "design by contract". Computer, 25(10):40-51, October 1992. Google Scholar
  14. Flemming Nielson, Hanne Ries Nielson, and Chris Hankin. Principles of Program Analysis, 2^nd edition. Springer, 2005. ISBN 3-540-65410-0. Google Scholar
  15. Chang Yun Park. Predicting Program Execution Times by Analyzing Static and Dynamic Program Paths. Real-Time Systems, 5(1):31-62, March 1993. Google Scholar
  16. Mark Richters and Martin Gogolla. On formalizing the UML object constraint language OCL. In Tok-Wang Ling, Sudha Ram, and Mong Lee, editors, Proc. 17th Int. Conf. Conceptual Modeling (ER’98), volume 1507 of Lecture Notes in Comput. Sci., pages 449-464. Springer-Verlag, 1998. Google Scholar
  17. J. Michael Spivey. Understanding Z: a specification language and its formal semantics. Cambridge University Press, 1988. Google Scholar
  18. SWEET home page, 2011. URL: http://www.mrtc.mdh.se/projects/wcet/sweet/.
  19. Glynn Winskel. The Formal Semantics of Programming Languages - An Introduction. MIT Press, 1993. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact