@inproceedings{micskeiz-FMTU05,
  author={Zoltan Micskei},
  year={2005},
  title={Automatikus tesztgener{\'a}l{\'a}s modell ellen\H{o}rz\H{o}vel},
  abstract={Testing is an essential, but time and resource consuming activity in
    the software development process. Generating a short, but effective test suite
    usually needs a lot of manual work and expert knowledge. In a model-based process,
    among other subtasks, test construction and test execution can also be partially
    automated. Based on the method suggested in [1], this paper presents a test
    generator tool, which can be used for test set generation in the development
    process of event-driven embedded systems. For a selected test coverage criterion
    and from the UML statechart model of the system the program generates test
    cases using the SPIN model checker. The test generator tool supports currently
    the test sequence construction on the basis of the "all states" and "all transitions"
    coverage criteria. The necessary model transformation [2] and requirement generation
    steps are performed automatically. The configuration of the model checker in
    the case of test generation, namely the settings required for constructing
    a short and minimal test suite, differs from the usual needs of classic model
    checking problems. The paper analyzes the possible settings of the model checker
    SPIN by measuring the efficiency of test construction in the case of different
    real-life statechart models, and introduces an optimized setting for test generation.
    The test generator is extended for real-time applications, in this case the
    model is available in the form of timed automata, and the model checker to
    be used is Uppaal [3]. },
  booktitle={Proc. of X. Fiatal M{\^u}szakiak Tudom{\'a}nyos {\"U}l{\'e}sszaka
    (FMTU)},
  address={Kolozsvar, Romania},
  editor={Bitay E.},
  pages={47--50},
  organization={Erd{\'e}lyi M{\'u}zeum Egyes{\"u}let}
}