Some approximations in Model Checking and Testing
This work addresses verification problems for systems where exact methods are too costly, but it appears incremental as it reviews and organizes existing approximation notions rather than proposing new ones.
The paper tackles the challenge of computationally hard verification in model checking and testing by introducing several approximation techniques, such as Bounded Model Checking and Approximate Probabilistic Model Checking, which guarantee quality and efficiency in verification.
Model checking and testing are two areas with a similar goal: to verify that a system satisfies a property. They start with different hypothesis on the systems and develop many techniques with different notions of approximation, when an exact verification may be computationally too hard. We present some notions of approximation with their logic and statistics backgrounds, which yield several techniques for model checking and testing: Bounded Model Checking, Approximate Model Checking, Approximate Black-Box Checking, Approximate Model-based Testing and Approximate Probabilistic Model Checking. All these methods guarantee some quality and efficiency of the verification.