Automatic Test Data Generation and Model Checking with CHR

TL;DR

This paper demonstrates how Constraint Handling Rules (CHR) can be applied to automate test data generation and model checking, enhancing verification processes for mission-critical satellite control software.

Contribution

It introduces a novel application of CHR for automated testing and model checking in satellite software verification.

Findings

Effective test data generation using CHR

Improved model checking efficiency

Potential for verifying mission-critical systems

Abstract

We present an example for application of Constraint Handling Rules to automated test data generation and model checking in verification of mission critical software for satellite control.