TL-CTD: Temporal Logic Combinatorial Test Generator

Overview

TL-CTD is an automated testing tool for reactive systems that combines formal verification with combinatorial testing. The tool automatically generates optimized test suites by integrating NuSMV model checking with pairwise coverage algorithms.

Problem Statement

Testing critical software systems faces three fundamental challenges:

1. State Space Explosion: The number of possible test sequences is infinite or extremely large
2. Insufficient Coverage: Manual testing often misses edge cases and rare behavioral combinations
3. Scenario Generation Complexity: Creating test sequences that reach specific system states is difficult and error-prone

Solution Approach

TL-CTD addresses these challenges through:

• Formal Models: Systematic state space exploration using NuSMV
• Combinatorial Algorithms: Pairwise coverage to reduce test suite size by 70-90%
• Automated Witness Extraction: Counter-example generation via model checking
• Guaranteed Coverage: 100% coverage of all feasible test targets

Architecture

The tool implements a five-stage pipeline:

1. Parser: Load and parse NuSMV model and temporal logic properties
2. Coverage Target Generation: Create pairwise combinations of property valuations
3. Witness Extraction: Extract execution traces from NuSMV for each target
4. Optimization: Apply greedy set cover to minimize test suite size
5. Reporting: Generate JSON output with coverage statistics

Installation

Prerequisites

• Python 3.9 or higher
• NuSMV 2.7.1 or higher (available from http://nusmv.fbk.eu)
• pip (Python package manager)

Setup Instructions

# Clone the repository
git clone https://github.com/edenbar23/Introduction-to-Formal-Verification-Methods.git
cd Introduction-to-Formal-Verification-Methods

# Install dependencies
pip install -r requirements.txt

# Install TL-CTD
pip install -e .

# Verify installation
tlctd --help

Quick Start

Generate a test suite using the provided e-commerce example:

tlctd --model examples/ecommerce/store.smv \
      --properties examples/ecommerce/properties.yaml \
      --output test_suite.json \
      --coverage-report

The tool will:

1. Parse the shopping cart model and 7 properties
2. Generate coverage targets (typically 80-100 targets)
3. Extract execution traces from NuSMV
4. Optimize the test suite (typically 20-30 tests)
5. Save results to test_suite.json

Usage

Command Line Interface

Basic syntax:

tlctd --model MODEL.smv --properties PROPS.yaml --output OUTPUT.json

Common options:

# Display detailed progress
tlctd -m model.smv -p props.yaml -o out.json --verbose

# Show coverage statistics
tlctd -m model.smv -p props.yaml -o out.json --coverage-report

# Set timeout for NuSMV calls (in seconds)
tlctd -m model.smv -p props.yaml -o out.json --timeout 120

# Skip optimization (keep all witnesses)
tlctd -m model.smv -p props.yaml -o out.json --no-optimize

# Limit number of targets (for testing)
tlctd -m model.smv -p props.yaml -o out.json --max-targets 50

Interactive Mode

Running tlctd without arguments launches an interactive wizard that guides you through the process with menu-based selections.

Input Specification

NuSMV Model Format

Models should include:

• State variables representing the system
• An action/step variable for test sequences
• A program counter (pc) for bounded model checking
• Transition logic using ASSIGN statements

Example:

MODULE main
VAR
  state: {IDLE, LOGGED_IN, CHECKOUT, ERROR};
  cart_items: 0..5;
  step: {None, Login, AddItem, RemoveItem, Pay, Logout};
  pc: 0..10;

ASSIGN
  init(state) := IDLE;
  init(cart_items) := 0;
  init(step) := None;
  init(pc) := 0;
  
  next(pc) := (pc < 10) ? pc + 1 : pc;
  
  next(state) := case
    state = IDLE & step = Login : LOGGED_IN;
    state = LOGGED_IN & step = Pay & cart_items > 0 : CHECKOUT;
    state = LOGGED_IN & step = Pay & cart_items = 0 : ERROR;
    TRUE : state;
  esac;

Properties File Format

Properties are specified in YAML with two sections:

properties:
  - name: "login_performed"
    type: "LTL"
    formula: "F (state = LOGGED_IN)"
    description: "The test sequence includes a successful login."
    
  - name: "checkout_reached"
    type: "LTL"
    formula: "F (state = CHECKOUT)"
    description: "The test reaches the checkout phase."
    
  - name: "security_violation"
    type: "CTL"
    formula: "EF (state = IDLE & step = Pay)"
    description: "Tests unauthorized payment attempt."

configuration:
  max_trace_length: 10
  strategy: "pairwise"
  timeout: 60

Output Format

The tool generates a JSON file containing:

Metadata Section

{
  "metadata": {
    "generated_at": "2026-02-05T22:20:33",
    "model_file": "store.smv",
    "properties_file": "properties.yaml",
    "tool": "TL-CTD",
    "version": "0.1.0"
  }
}

Coverage Statistics

{
  "coverage": {
    "total_targets": 93,
    "covered_targets": 23,
    "infeasible_targets": 70,
    "uncovered_targets": 0,
    "coverage_percentage": 100.0,
    "infeasible_target_ids": ["target_1", "target_2", ...]
  }
}

Test Suite

{
  "test_suite": {
    "total_tests": 23,
    "test_cases": [
      {
        "test_id": "TC-001",
        "target_id": "prop_login_performed",
        "description": "Test property: login functionality",
        "feasible": true,
        "steps": [
          {
            "step_number": 1,
            "state": {
              "state": "IDLE",
              "cart_items": 0,
              "step": "None",
              "pc": 0
            }
          },
          {
            "step_number": 2,
            "state": {
              "state": "LOGGED_IN",
              "step": "Login",
              "pc": 1
            }
          }
        ]
      }
    ]
  }
}

Examples

Two complete examples are provided:

E-commerce Shopping Cart

Location: examples/ecommerce/

Demonstrates:

• Web application state modeling
• Security properties (authentication, authorization)
• Business logic validation
• Error state handling

Elevator Control System

Location: examples/elevator/

Demonstrates:

• Embedded system modeling
• Safety-critical properties
• Multi-floor state management
• Real-time constraints

Both examples include:

• Complete NuSMV models (.smv files)
• Property specifications (.yaml files)
• Documentation explaining the system

Success Criteria

The tool satisfies the following criteria from the project proposal:

1. Successfully loads models and properties without errors
2. Produces test suites with 100% coverage of feasible property pairs
3. Identifies and reports infeasible targets
4. Completes execution in reasonable time (seconds to minutes for medium models)
5. Generates machine-readable JSON and human-readable reports

Methodology

TL-CTD implements the methodology described in the project proposal:

1. Parsing: Load NuSMV model and YAML properties
2. Target Generation: Create pairwise combinations of property valuations
3. Witness Extraction: For each target, construct a negated formula and use NuSMV to find counter-examples
4. Greedy Optimization: Use set cover algorithm to minimize test suite while maintaining coverage
5. Reporting: Export results in JSON format with coverage statistics

Technical Details

• Language: Python 3.9+
• Model Checker: NuSMV (subprocess-based execution)
• Algorithm: Greedy set cover for test suite optimization
• Coverage Strategy: Pairwise combinatorial testing
• Model Checking Mode: Bounded Model Checking (BMC) for shorter traces

Documentation

• README.md (this file): Project overview and quick start
• USER_GUIDE.md: Comprehensive usage guide with examples
• examples/: Complete working examples with documentation

License

MIT License - See LICENSE file for details

Author

Eden Bar Ben-Gurion University Introduction to Formal Verification Methods Course