Sciweavers

Share
GI
2009
Springer

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

11 years 4 months ago
Tapir: Language Support to Reduce the State Space in Model-Checking
: 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 implemena 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.
Ronald Veldema, Michael Philippsen
Added 24 Jul 2010
Updated 24 Jul 2010
Type Conference
Year 2009
Where GI
Authors Ronald Veldema, Michael Philippsen
Comments (0)
books