Skip to content

USAGE_EXAMPLES.md

Latest commit

 

History

History
605 lines (470 loc) · 14.3 KB

USAGE_EXAMPLES.md

File metadata and controls

605 lines (470 loc) · 14.3 KB

Usage Examples

This document provides practical examples of using the Hybrid Verification Framework with different protocols and workflows.

Table of Contents

  1. Quick Start: Raft Protocol
  2. Adding a New Protocol
  3. Hybrid Verification Workflow
  4. Property Synthesis Workflow
  5. Code Generation Workflow
  6. Protocol-Agnostic Usage

Quick Start: Raft Protocol

Step 1: Generate Verification Code

# Generate properties
python tools/generate_properties.py raft

# Generate KLEE test harness
python tools/generate_klee_test.py raft

# Generate TLA+ specification
python tools/generate_tla_spec.py raft

Step 2: Run KLEE Symbolic Execution

cd examples/raft/test_harness
make run-klee
# Or using Docker:
./run_docker.bat

Step 3: Extract Counterexamples

cd examples/raft/test_harness
python extract_klee_counterexamples.py klee-out-0 > counterexamples.json

Step 4: Run Hybrid Verification

# Windows
cd verification
.\refinement_loop.bat raft

# Linux/Mac
bash verification/refinement_loop.sh raft

Adding a New Protocol

Example: Adding a Simple Consensus Protocol

Step 1: Create Protocol Configuration

Create examples/my_protocol/config/my_protocol.yaml:

protocol:
  name: "MyProtocol"
  domain: "consensus"
  adapter: "examples/my_protocol/adapter/my_protocol_adapter.c"
  adapter_factory: "create_my_protocol_definition"
  
  description: "A simple consensus protocol"

configuration:
  num_nodes: 3
  max_rounds: 10
  timeout_range: [100, 200]

properties:
  - name: "LeaderUniqueness"
    type: "safety"
    template: "uniqueness.yaml"
    variables:
      ENTITY: "Leader"
      CONTEXT: "round"
      ENTITY_FIELD: "role"
      CONTEXT_FIELD: "current_round"
      MAX_CONTEXT: 10
    description: "At most one leader per round"
  
  - name: "Agreement"
    type: "safety"
    template: "agreement.yaml"
    variables:
      VALUE: "decision"
      FIELD: "decided_value"
      CONDITION: "nodes[i].decided == true"
    description: "All nodes agree on the decided value"

state_variables:
  - name: "id"
    type: "int"
    description: "Node identifier"
  
  - name: "role"
    type: "Role"
    description: "Current role (LEADER, FOLLOWER)"
  
  - name: "current_round"
    type: "int"
    description: "Current round number"
  
  - name: "decided_value"
    type: "int"
    description: "Decided value (if decided)"
  
  - name: "decided"
    type: "bool"
    description: "Whether node has decided"

message_types:
  - name: "PROPOSE"
    description: "Propose a value"
  
  - name: "ACCEPT"
    description: "Accept a proposal"

Step 2: Create Protocol Adapter

Create examples/my_protocol/adapter/my_protocol_adapter.c:

#include "core/system_interface.h"
#include "my_protocol_adapter.h"

// Node structure
typedef struct {
    int id;
    Role role;
    int current_round;
    int decided_value;
    bool decided;
} MyProtocolNode;

// Message structure
typedef struct {
    int sender_id;
    int round;
    int value;
    MessageType type;
} MyProtocolMessage;

// Initialize node
static void my_protocol_init_node(SystemNode* node, int id, SystemConfig* config) {
    MyProtocolNode* n = (MyProtocolNode*)node;
    n->id = id;
    n->role = FOLLOWER;
    n->current_round = 0;
    n->decided = false;
}

// Process message
static void my_protocol_process_message(SystemNode* node, SystemMessage* msg,
                                        void* network_state, void* metrics) {
    MyProtocolNode* n = SYSTEM_NODE(node, MyProtocolNode);
    MyProtocolMessage* m = SYSTEM_MSG(msg, MyProtocolMessage);
    
    // Process message based on type
    if (m->type == PROPOSE && n->role == FOLLOWER) {
        n->decided_value = m->value;
        n->decided = true;
    }
    // ... more message processing
}

// Generate message
static SystemMessage* my_protocol_generate_message(SystemNode* node, int target_id) {
    MyProtocolNode* n = SYSTEM_NODE(node, MyProtocolNode);
    
    if (n->role == LEADER) {
        MyProtocolMessage* msg = malloc(sizeof(MyProtocolMessage));
        msg->sender_id = n->id;
        msg->round = n->current_round;
        msg->type = PROPOSE;
        msg->value = n->decided_value;
        return (SystemMessage*)msg;
    }
    return NULL;
}

// Verify safety
static int my_protocol_verify_safety(SystemNode* nodes[], int num_nodes, void* metrics) {
    // Check leader uniqueness
    int leaders = 0;
    for (int i = 0; i < num_nodes; i++) {
        MyProtocolNode* n = SYSTEM_NODE(nodes[i], MyProtocolNode);
        if (n->role == LEADER) {
            leaders++;
        }
    }
    if (leaders > 1) {
        return 0;  // Safety violation
    }
    
    // Check agreement
    int decided_value = -1;
    for (int i = 0; i < num_nodes; i++) {
        MyProtocolNode* n = SYSTEM_NODE(nodes[i], MyProtocolNode);
        if (n->decided) {
            if (decided_value == -1) {
                decided_value = n->decided_value;
            } else if (decided_value != n->decided_value) {
                return 0;  // Agreement violation
            }
        }
    }
    
    return 1;  // Safety properties hold
}

// Verify liveness
static int my_protocol_verify_liveness(SystemNode* nodes[], int num_nodes,
                                       int round, void* metrics) {
    // Check if a leader is elected
    for (int i = 0; i < num_nodes; i++) {
        MyProtocolNode* n = SYSTEM_NODE(nodes[i], MyProtocolNode);
        if (n->role == LEADER) {
            return 1;  // Leader exists
        }
    }
    
    // If no leader after many rounds, liveness violation
    if (round > 10) {
        return 0;
    }
    
    return 1;
}

// Allocate nodes
static void my_protocol_alloc_nodes(SystemNode** nodes, int num_nodes) {
    *nodes = malloc(sizeof(MyProtocolNode) * num_nodes);
}

// Free nodes
static void my_protocol_free_nodes(SystemNode* nodes, int num_nodes) {
    free(nodes);
}

// Free message
static void my_protocol_free_message(SystemMessage* msg) {
    free(msg);
}

// Operations structure
static SystemOperations my_protocol_ops = {
    .initialize_node = my_protocol_init_node,
    .process_message = my_protocol_process_message,
    .generate_message = my_protocol_generate_message,
    .should_send_message = NULL,  // Optional
    .verify_safety = my_protocol_verify_safety,
    .verify_liveness = my_protocol_verify_liveness,
    .verify_invariant = NULL,  // Optional
    .alloc_nodes = my_protocol_alloc_nodes,
    .free_nodes = my_protocol_free_nodes,
    .free_message = my_protocol_free_message
};

// Default configuration
static SystemConfig my_protocol_default_config = {
    .num_nodes = 3,
    .max_rounds = 10,
    .timeout_range = {100, 200},
    .domain_specific = NULL
};

// Factory function
SystemDefinition* create_my_protocol_definition(void) {
    SystemDefinition* def = malloc(sizeof(SystemDefinition));
    def->name = "MyProtocol";
    def->domain = "consensus";
    def->ops = &my_protocol_ops;
    def->default_config = &my_protocol_default_config;
    def->property_definitions = NULL;
    return def;
}

Step 3: Generate Code

# Generate properties
python tools/generate_properties.py my_protocol

# Generate KLEE harness
python tools/generate_klee_test.py my_protocol

# Generate TLA+ spec
python tools/generate_tla_spec.py my_protocol

Step 4: Use the Protocol

# Run hybrid verification
bash verification/refinement_loop.sh my_protocol

Hybrid Verification Workflow

Complete Workflow Example

# 1. Generate verification code
python tools/generate_properties.py raft
python tools/generate_klee_test.py raft
python tools/generate_tla_spec.py raft

# 2. Run KLEE
cd examples/raft/test_harness
make run-klee

# 3. Extract KLEE counterexamples
python extract_klee_counterexamples.py klee-out-0 > klee_counterexamples.json

# 4. Convert KLEE to TLA+
cd ../..
python verification/counterexample_converter.py \
    --klee-to-tla examples/raft/test_harness/klee_counterexamples.json \
    --output-dir verification/iterations/iteration_1 \
    --protocol raft

# 5. Run TLA+ model checking (in TLA+ Toolbox)
# Open examples/raft/spec/Raft.tla and run model checking

# 6. Extract TLA+ counterexamples
python examples/raft/spec/extract_tla_counterexamples.py examples/raft/spec > examples/raft/spec/tla_counterexamples.json

# 7. Convert TLA+ to KLEE
python verification/counterexample_converter.py \
    --tla-to-klee examples/raft/spec/tla_counterexamples.json \
    --output-dir verification/iterations/iteration_1 \
    --protocol raft

# 8. Create guided initialization
python verification/create_tla_guided_json.py \
    examples/raft/spec/tla_counterexamples.json \
    --protocol raft

# 9. Run refinement loop (automates steps 2-8)
bash verification/refinement_loop.sh raft

Property Synthesis Workflow

Analyzing Counterexamples

# Analyze counterexamples (generic mode)
python synthesis/analyze_counterexample.py \
    examples/raft/test_harness/klee-out-0/counterexamples.json

# Analyze with protocol-specific patterns
python synthesis/analyze_counterexample.py \
    examples/raft/test_harness/klee-out-0/counterexamples.json \
    --protocol raft

Synthesizing Properties

# Synthesize properties from analysis
python synthesis/synthesize_property.py \
    counterexample_analysis.json

# Refine properties
python synthesis/property_refinement.py \
    counterexample_analysis.json

Example: Property Synthesis Script

#!/usr/bin/env python3
from synthesis.analyze_counterexample import analyze_counterexample
from synthesis.synthesize_property import synthesize_property

# Analyze counterexamples
analysis = analyze_counterexample('counterexamples.json', 'raft')

# Synthesize new properties
synthesized = synthesize_property(analysis)

# Save synthesized properties
import json
with open('synthesized_properties.json', 'w') as f:
    json.dump(synthesized, f, indent=2)

Code Generation Workflow

Generating All Code for a Protocol

#!/usr/bin/env python3
from tools.generate_properties import PropertyGenerator
from tools.generate_klee_test import KLEETestGenerator
from tools.generate_tla_spec import TLASpecGenerator

protocol = 'raft'

# Generate properties
prop_gen = PropertyGenerator()
prop_result = prop_gen.generate_properties(protocol)
print(f"Properties generated: {prop_result['json']}")

# Generate KLEE harness
klee_gen = KLEETestGenerator()
klee_file = klee_gen.generate_harness(protocol)
print(f"KLEE harness generated: {klee_file}")

# Generate TLA+ spec
tla_gen = TLASpecGenerator()
tla_file = tla_gen.generate_spec(protocol)
print(f"TLA+ spec generated: {tla_file}")

Customizing Property Templates

from tools.template_loader import TemplateLoader

loader = TemplateLoader()

# Load property template
template = loader.load_property_template('uniqueness')

# Customize variables
variables = {
    'ENTITY': 'Coordinator',
    'CONTEXT': 'epoch',
    'ENTITY_FIELD': 'role',
    'CONTEXT_FIELD': 'current_epoch',
    'MAX_CONTEXT': '20'
}

# Expand template
result = loader.expand_property_template('uniqueness', variables)

print("KLEE Code:")
print(result['klee_code'])
print("\nTLA+ Code:")
print(result['tla_code'])

Protocol-Agnostic Usage

Generic Counterexample Conversion

from verification.counterexample_converter import (
    convert_klee_to_tla,
    convert_tla_to_klee
)

# Generic KLEE counterexample
klee_cex = {
    'counterexample_id': 'generic_001',
    'property': 'SafetyProperty',
    'assertion': 'klee_assert(condition)',
    'symbolic_values': {
        'var1': 10,
        'var2': [1, 2, 3, 4, 5]
    }
}

# Convert to TLA+ (no protocol specified)
tla_result = convert_klee_to_tla(klee_cex)
print(tla_result['tla_code'])

# Generic TLA+ counterexample
tla_cex = {
    'counterexample_id': 'generic_002',
    'property': 'Invariant',
    'violated_invariant': 'TypeOK',
    'state': {
        'var1': 10,
        'var2': [1, 2, 3, 4, 5]
    }
}

# Convert to KLEE (no protocol specified)
klee_result = convert_tla_to_klee(tla_cex)
print(klee_result['klee_code'])

Generic Property Analysis

from synthesis.analyze_counterexample import identify_property_violation

# Generic counterexample
cex = {
    'assertion': 'klee_assert(entities <= 1)',
    'message': 'Uniqueness property violated: multiple entities per context',
    'property': 'UniquenessViolation'
}

# Identify violation (no protocol specified)
violation = identify_property_violation(cex)
print(f"Violation Type: {violation['violation_type']}")
print(f"Pattern: {violation['pattern']}")
print(f"Description: {violation['description']}")

Advanced Examples

Custom Domain Template

Create templates/domains/my_domain_system.yaml:

domain: "my_domain"
description: "Custom domain template"

components:
  - name: "Node"
    type: "entity"
  - name: "Message"
    type: "communication"

operations:
  - name: "initialize"
    description: "Initialize component"
  - name: "process"
    description: "Process event"

Custom Property Template

Create templates/properties/custom_property.yaml:

name: "custom_property"
type: "safety"
description: "Custom property template"

klee_template: |
  // Check {PROPERTY_NAME}
  int {VARIABLE_NAME} = 0;
  for (int i = 0; i < NUM_NODES; i++) {
      if ({CONDITION}) {
          {VARIABLE_NAME}++;
      }
  }
  klee_assert({VARIABLE_NAME} {OPERATOR} {THRESHOLD});

tla_template: |
  {PROPERTY_NAME} ==
      \\A i, j \\in 1..NumNodes :
          {CONDITION} => {VALUE_EXPRESSION}

Troubleshooting

Common Issues

  1. Protocol not found:

    • Ensure examples/{protocol}/config/{protocol}.yaml exists
    • Check protocol name spelling

  2. Template not found:

    • Ensure template file exists in templates/domains/ or templates/properties/
    • Check template name spelling

  3. Adapter not found:

    • Ensure adapter file exists at examples/{protocol}/adapter/{protocol}_adapter.c
    • Check factory function name matches config

  4. Code generation fails:

    • Verify protocol configuration is valid YAML
    • Check that all required fields are present

See Also