Automatic Refinement of ASM Abstract Test Cases

Model refinement is a specification approach widely used in formal modeling to deal with the complexity of large and complicated requirements. Specific artefacts are usually developed to complement specification with validation and verification activities. To avoid boresome and time-consuming activities when reusing models, in a model refinement specification process, techniques supporting reusability of formal development artefacts are highly desirable. In this paper, we tackle the problem of defining a technique for automatic refinement of abstract test cases for formal models given in terms of the Abstract State Machines (ASMs). We present an approach, based on a classical test generation technique exploiting model checking, able to reuse information of test cases obtained at a given level of abstraction in order to define, in an automatic way, the same kind of artefacts at a subsequent refinement level. We evaluate our approach on real case studies specified in ASMs by a sequence of refinement models.