Tapir: Language Support to Reduce the State Space in Model-Checking

Veldema R, Philippsen M (2009)

Publication Language: English

Publication Type: Conference contribution, Original article

Publication year: 2009

Publisher: GI Gesellschaft für Informatik

Edited Volumes: INFORMATIK 2009 - Im Focus das Leben, Beitrage der 39. Jahrestagung der Gesellschaft fur Informatik e.V. (GI)

Series: Lecture Notes Informatics

City/Town: Bonn

Book Volume: 2860-74

Pages Range: 364

Conference Proceedings Title: Informatik 2009 - Im Focus das Leben

Event location: Lübeck DE

ISBN: 978-3-88579-248-2

URI: http://www2.informatik.uni-erlangen.de/publication/download/ATPS09-tapir.pdf

Abstract

Model-checking is a way of testing the correctness of concurrent programs. To do so, a model of the program is proven to match properties and constraints specified by the programmer. The model itself is created by disregarding irrelevant program details. The biggest problem in model-checking is the number of program states that need to be tested. Tapir, a simple but familiar object-oriented language and accompanying tool chain, addresses this problem in two ways. First, the programmer can provide application specific program transformations that reduce the state space. Second, for selected classes and methods, the programmer can provide an alternative implementation: a slim black box version for use in model-checking that abstracts away many details of the full fledged implementation. Tapir's aspect-oriented test case generation combined with black-boxing allows model-checking of low-level library code.

Authors with CRIS profile

Ronald Veldema Lehrstuhl für Informatik 2 (Programmiersysteme) Michael Philippsen Lehrstuhl für Informatik 2 (Programmiersysteme)

How to cite

APA:

Veldema, R., & Philippsen, M. (2009). Tapir: Language Support to Reduce the State Space in Model-Checking. In Fischer, Stefan ; Maehle, Erik ; Reischuck, Rüdiger (Eds.), Informatik 2009 - Im Focus das Leben (pp. 364). Lübeck, DE: Bonn: GI Gesellschaft für Informatik.

MLA:

Veldema, Ronald, and Michael Philippsen. "Tapir: Language Support to Reduce the State Space in Model-Checking." Proceedings of the ATPS 2009 - 4. Arbeitstagung Programmiersprachen, Lübeck Ed. Fischer, Stefan ; Maehle, Erik ; Reischuck, Rüdiger, Bonn: GI Gesellschaft für Informatik, 2009. 364.

BibTeX: Download