Home | english  | Impressum | Sitemap | KIT

Model Checking and Model-Based Testing - Improving Their Feasibility by Lazy Techniques, Parallelization, and Other Optimizations

Model Checking and Model-Based Testing - Improving Their Feasibility by Lazy Techniques, Parallelization, and Other Optimizations
Autor(en):

David Faragó

Links:
Quelle:

Doctoral dissertation

Datum: 29.01.2016

Abstract


The major problem in MC is state space explosion, causing infeasible time and space
requirements, especially for liveness properties. For the important liveness property of livelock freedom, DFSfifo reduces both time and space requirements by simultaneously
exploring and checking the specification in one pass and without a Büchi product, and
by improving partial order reduction for DFSfifo. The time requirement is further
reduced by parallelization with almost linear speedup. Usability is improved by simpler
and more accurate modeling of progress and shortest counterexamples. Unfortunately,
DFSfifo cannot be generalized to cover all LTL properties.

 

The major problem in MBT is state space explosion and test case explosion for offline MBT and low meaningfulness for on-the-fly MBT, both causing infeasible time, for
offline MBT also infeasible space requirements, especially for SUTs with uncontrollable
nondeterminism. LazyOTF
reduces both time and space requirements by integrating
both on-the-fly and offline MBT: It swaps between state space traversal and test execution phases, enabling strong guidance by traversing sub-graphs of the specification,
employing heuristics that make use of dynamic information from previous test execution
phases, for instance the SUT’s resolution of uncontrollable nondeterminism. The time
requirement is further reduced by parallelization with (super-)linear speedup of mean-
ingful test execution and almost linear speedup overall. Usability is improved by higher
meaningfulness and reproducibility. Furthermore, flexible heuristics via weights, composable TOs, and a provisos framework offer usable configuration and guarantees for
exhaustiveness, coverage, and discharging. Unfortunately, LazyOTF tightly integrates
MC algorithms with heuristics to make strong use of the available dynamic information;
hence useful off-the-shelf tools (e.g., for MC or SMT solving) cannot be efficiently employed by
LazyOTF without adaption; but our provisos framework helps the adaption.
Furthermore, many aspects of MBT and possibilities for further heuristics are future
work, with MBT of timed automata being a big challenge.


In summary, this thesis focuses on the lightweight formal method of MBT for checking
safety properties, and derives a new and more feasible approach. For liveness properties,
dynamic testing is impossible, so feasibility is increased by specializing on an impor-
tant class of properties, livelock freedom, and deriving a more feasible model checking
algorithm for it. All mentioned improvements are substantiated by experiments