|
|
# Default Configuration for Formal Specification Generation System
|
|
|
|
|
|
# System Information
|
|
|
system:
|
|
|
name: "Formal Spec Generator"
|
|
|
version: "0.1.0"
|
|
|
description: "基于大型语言模型的形式化程序规范自动生成验证系统"
|
|
|
author: "国防科大计算机学院22级软件工程小班刘卓小组"
|
|
|
|
|
|
# LLM Configuration (SiliconFlow DeepSeek V3.1)
|
|
|
llm:
|
|
|
provider: "siliconflow"
|
|
|
model: "deepseek-ai/DeepSeek-V3.1"
|
|
|
base_url: "https://api.siliconflow.cn/v1"
|
|
|
api_key: "${SILICONFLOW_API_KEY:-sk-xtzjxgjzqtxqjdpvzxxgkxgqkqjgkqjkqgqkqgkqgkqkqj}"
|
|
|
timeout: 120
|
|
|
max_retries: 3
|
|
|
retry_delay: 1.0
|
|
|
rate_limit_delay: 5.0
|
|
|
max_concurrent_requests: 3
|
|
|
|
|
|
# Generation Parameters
|
|
|
temperature: 0.7
|
|
|
max_tokens: 4096
|
|
|
top_p: 0.95
|
|
|
|
|
|
# Streaming Configuration
|
|
|
streaming:
|
|
|
enabled: true
|
|
|
chunk_timeout: 30
|
|
|
|
|
|
# Prompt Templates and Context
|
|
|
prompts:
|
|
|
system_role: "你是一个专业的形式化方法专家，擅长为C/C++程序生成CBMC兼容的形式化规范。"
|
|
|
|
|
|
# Template selection based on function characteristics
|
|
|
template_selection:
|
|
|
complexity_thresholds:
|
|
|
low: 20
|
|
|
medium: 50
|
|
|
high: 80
|
|
|
domain_keywords:
|
|
|
freertos: ["task", "queue", "semaphore", "timer", "freertos", "xTask", "xQueue"]
|
|
|
network: ["socket", "connect", "send", "recv", "bind", "listen"]
|
|
|
crypto: ["encrypt", "decrypt", "hash", "aes", "rsa", "sha", "hmac"]
|
|
|
filesystem: ["file", "open", "read", "write", "close", "fopen", "fwrite"]
|
|
|
|
|
|
# CBMC Syntax Reference
|
|
|
cbmc_syntax: |
|
|
|
CBMC Annotation Syntax:
|
|
|
- \\requires(condition) - Preconditions
|
|
|
- \\ensures(condition) - Postconditions
|
|
|
- \\assigns(location) - Memory modification specification
|
|
|
- \\valid(ptr) - Pointer validity
|
|
|
- \\valid_read(ptr) - Readable memory
|
|
|
- \\valid_write(ptr) - Writable memory
|
|
|
- \\forall(type var : range; condition) - Universal quantifier
|
|
|
- \\exists(type var : range; condition) - Existential quantifier
|
|
|
- \\behavior name: ... \\complete behaviors; \\disjoint behaviors;
|
|
|
|
|
|
# Quality Assessment
|
|
|
quality_metrics:
|
|
|
syntax_completeness: 0.9
|
|
|
logical_consistency: 0.8
|
|
|
domain_relevance: 0.85
|
|
|
verifiability: 0.9
|
|
|
|
|
|
# CBMC Configuration
|
|
|
cbmc:
|
|
|
path: "cbmc"
|
|
|
min_version: "5.0"
|
|
|
default_unwinding: 10
|
|
|
default_timeout: 300
|
|
|
|
|
|
# Verification Options
|
|
|
options:
|
|
|
pointer_check: true
|
|
|
overflow_check: true
|
|
|
bounds_check: true
|
|
|
assertion_check: true
|
|
|
div_by_zero_check: true
|
|
|
undefined_shift_check: true
|
|
|
signed_overflow_check: true
|
|
|
|
|
|
# Memory Model
|
|
|
memory_model: "precise"
|
|
|
object_bits: 8
|
|
|
|
|
|
# Output Control
|
|
|
show_properties: true
|
|
|
trace: true
|
|
|
error_trace: true
|
|
|
|
|
|
# Web Server Configuration
|
|
|
web:
|
|
|
host: "0.0.0.0"
|
|
|
port: 8080
|
|
|
debug: true
|
|
|
threaded: true
|
|
|
|
|
|
# File Upload
|
|
|
max_file_size: "10MB"
|
|
|
allowed_extensions: [".c", ".cpp", ".h", ".hpp"]
|
|
|
upload_dir: "uploads"
|
|
|
|
|
|
# Session
|
|
|
secret_key: "your-secret-key-here"
|
|
|
session_lifetime: 3600
|
|
|
|
|
|
# Logging Configuration
|
|
|
logging:
|
|
|
level: "INFO"
|
|
|
format: "%(asctime)s - %(name)s - %(levelname)s - %(message)s"
|
|
|
|
|
|
# Component-specific log files
|
|
|
log_files:
|
|
|
parser: "logs/parser.log"
|
|
|
llm_generation: "logs/llm_generation.log"
|
|
|
cbmc_verification: "logs/cbmc_verification.log"
|
|
|
error_analysis: "logs/error_analysis.log"
|
|
|
mutation: "logs/mutation.log"
|
|
|
system: "logs/system.log"
|
|
|
|
|
|
# Rotation
|
|
|
max_size: "10MB"
|
|
|
backup_count: 5
|
|
|
encoding: "utf-8"
|
|
|
|
|
|
# Verification Configuration
|
|
|
verification:
|
|
|
max_concurrent: 3
|
|
|
cache_enabled: true
|
|
|
cache_ttl: 3600
|
|
|
|
|
|
# Mutation Weights (heuristic selection)
|
|
|
mutation_weights:
|
|
|
predicate: 0.3 # 谓词变异: \forall ↔ \exists
|
|
|
boundary: 0.25 # 边界变异: < ↔ <=, > ↔ >=
|
|
|
logical: 0.2 # 逻辑变异: && ↔ ||, ==> ↔ <==
|
|
|
array_bounds: 0.15 # 数组边界: 0 .. n-1 ↔ 0 .. n
|
|
|
pointer_validity: 0.1 # 指针有效性: \valid(ptr) ↔ \valid_read(ptr)
|
|
|
|
|
|
# Quality Assessment
|
|
|
quality:
|
|
|
# Evaluation Metrics
|
|
|
metrics:
|
|
|
accuracy: 0.8 # 准确性目标
|
|
|
completeness: 0.75 # 完整性目标
|
|
|
verifiability: 0.9 # 可验证性目标
|
|
|
stability: 0.85 # 稳定性目标
|
|
|
|
|
|
# Performance Thresholds
|
|
|
max_generation_time: 30
|
|
|
max_verification_time: 300
|
|
|
max_memory_usage: "512MB"
|
|
|
|
|
|
# Specification Generation Configuration
|
|
|
specification:
|
|
|
# Storage Settings
|
|
|
storage:
|
|
|
base_path: "specifications"
|
|
|
format: "json"
|
|
|
enable_versioning: true
|
|
|
max_versions: 10
|
|
|
cleanup_interval: 86400 # 24 hours
|
|
|
|
|
|
# Validation Settings
|
|
|
validation:
|
|
|
enabled: true
|
|
|
quality_thresholds:
|
|
|
syntax: 0.9
|
|
|
logic: 0.8
|
|
|
completeness: 0.7
|
|
|
overall: 0.75
|
|
|
strict_mode: false
|
|
|
auto_refine: true
|
|
|
max_refinements: 3
|
|
|
|
|
|
# Generation Modes
|
|
|
generation:
|
|
|
default_mode: "single"
|
|
|
batch_size: 10
|
|
|
enable_streaming: true
|
|
|
timeout_per_function: 60
|
|
|
|
|
|
# Domain-Specific Settings
|
|
|
domains:
|
|
|
freertos:
|
|
|
handle_validation: true
|
|
|
task_context: true
|
|
|
interrupt_safety: true
|
|
|
network:
|
|
|
timeout_handling: true
|
|
|
error_recovery: true
|
|
|
crypto:
|
|
|
side_channel_protection: true
|
|
|
key_validation: true
|
|
|
filesystem:
|
|
|
resource_management: true
|
|
|
error_handling: true
|
|
|
|
|
|
# Development Settings
|
|
|
development:
|
|
|
mode: true
|
|
|
test_mode: false
|
|
|
show_debug_info: true
|
|
|
mock_llm: false
|
|
|
|
|
|
# Code Quality
|
|
|
code_style:
|
|
|
line_length: 88
|
|
|
docstring_coverage: 0.8
|
|
|
|
|
|
# Testing
|
|
|
test_coverage_target: 0.8
|
|
|
|
|
|
# API Configuration
|
|
|
api:
|
|
|
# API Server Settings
|
|
|
host: "0.0.0.0"
|
|
|
port: 8080
|
|
|
debug: true
|
|
|
|
|
|
# CORS Configuration
|
|
|
cors:
|
|
|
enabled: true
|
|
|
origins: ["*"]
|
|
|
methods: ["GET", "POST", "PUT", "DELETE", "OPTIONS"]
|
|
|
headers: ["Content-Type", "Authorization"]
|
|
|
|
|
|
# Rate Limiting
|
|
|
rate_limiting:
|
|
|
enabled: true
|
|
|
requests_per_minute: 100
|
|
|
burst_limit: 10
|
|
|
|
|
|
# Authentication (to be implemented)
|
|
|
authentication:
|
|
|
enabled: false
|
|
|
method: "session" # session, jwt, api_key
|
|
|
session_lifetime: 3600
|
|
|
|
|
|
# WebSocket Configuration
|
|
|
websocket:
|
|
|
enabled: true
|
|
|
max_connections: 1000
|
|
|
connection_timeout: 300 # 5 minutes
|
|
|
message_size_limit: "16MB"
|
|
|
ping_interval: 25
|
|
|
ping_timeout: 60
|
|
|
|
|
|
# Room Configuration
|
|
|
rooms:
|
|
|
user_prefix: "user:"
|
|
|
session_prefix: "session:"
|
|
|
job_prefix: "job:"
|
|
|
system_room: "system"
|
|
|
|
|
|
# Event Handling
|
|
|
events:
|
|
|
enable_logging: true
|
|
|
broadcast_system_events: true
|
|
|
|
|
|
# Job Manager Configuration
|
|
|
job_manager:
|
|
|
storage_dir: "job_storage"
|
|
|
max_concurrent: 5
|
|
|
cleanup_interval: 3600 # 1 hour
|
|
|
max_job_age_days: 7
|
|
|
enable_persistence: true
|
|
|
|
|
|
# Job Timeout Settings
|
|
|
timeouts:
|
|
|
upload: 300
|
|
|
parsing: 600
|
|
|
generation: 1800 # 30 minutes
|
|
|
mutation: 900
|
|
|
verification: 1800 # 30 minutes
|
|
|
workflow: 3600 # 1 hour
|
|
|
|
|
|
# API Response Settings
|
|
|
responses:
|
|
|
enable_debug_info: false
|
|
|
include_traceback: false
|
|
|
default_page_size: 20
|
|
|
max_page_size: 100
|
|
|
|
|
|
# File Upload Settings
|
|
|
upload:
|
|
|
max_file_size: "50MB"
|
|
|
allowed_extensions: [".c", ".cpp", ".h", ".hpp", ".cc", ".cxx"]
|
|
|
temp_directory: "temp_uploads"
|
|
|
enable_virus_scan: false
|
|
|
|
|
|
# Workflow Configuration
|
|
|
workflow:
|
|
|
default_mode: "single_function" # single_function, batch_processing, iterative_refinement, comprehensive_analysis
|
|
|
|
|
|
# Mode-specific Settings
|
|
|
modes:
|
|
|
single_function:
|
|
|
max_functions: 1
|
|
|
enable_mutation: true
|
|
|
enable_verification: true
|
|
|
|
|
|
batch_processing:
|
|
|
max_functions: 50
|
|
|
batch_size: 10
|
|
|
concurrent_batches: 3
|
|
|
|
|
|
iterative_refinement:
|
|
|
max_iterations: 3
|
|
|
quality_threshold: 0.8
|
|
|
enable_auto_refine: true
|
|
|
|
|
|
comprehensive_analysis:
|
|
|
enable_full_analysis: true
|
|
|
generate_report: true
|
|
|
export_formats: ["json", "html", "pdf"]
|
|
|
|
|
|
# Global Settings
|
|
|
settings:
|
|
|
enable_mutation: true
|
|
|
enable_verification: true
|
|
|
max_iterations: 3
|
|
|
total_timeout: 3600
|
|
|
step_timeout: 300
|
|
|
error_tolerance: 3
|
|
|
quality_threshold: 0.7
|
|
|
|
|
|
# Output Settings
|
|
|
output:
|
|
|
save_intermediate: true
|
|
|
generate_report: true
|
|
|
export_formats: ["json", "html"]
|
|
|
result_directory: "workflow_results"
|
|
|
|
|
|
# Concurrency Control
|
|
|
concurrency:
|
|
|
max_concurrent_jobs: 3
|
|
|
max_concurrent_operations: 10
|
|
|
semaphore_timeout: 30 |
