angela0310/MSc-dissertation

# 硕士论文 这是硕士论文“自动驾驶系统中临时修复与永久驾驶规则之间的冲突检测与解决”的私有代码库。 # 基于 Z3 的自动驾驶规则冲突检测 本项目解析以小型领域特定语言（DSL）编写的自动驾驶策略规则，将其转换为 Z3 约束，并检查当两条规则在同一场景中同时激活时，是否会产生不兼容的操作。 ## 功能特性 - 将规则解析为 `trigger`、`condition` 和 `then` 部分。 - 收集变量并推断 `Int`、`Real`、`Bool` 和 `String` 类型。 - 将变量转换为 Z3 约束。 - 检查单条规则的内部一致性。 - 比较每一对规则。 - 报告 `Conflict`（冲突）或 `No conflict`（无冲突）。 - 生成 JSON 文件和人类可读的冲突报告。 - 使用 Z3 unsatisfiable cores 来识别真实冲突中涉及的确切约束。 ## 环境要求 - Python 3.10 或更高版本 - `z3-solver` 安装依赖： ``` python -m pip install z3-solver ``` 该包安装时的名称为 `z3-solver`，但在导入时使用： ``` from z3 import * ``` 请勿安装名为 `z3` 的无关软件包。 ## 项目结构 ``` dissertation code/ ├── Rules encoder/ │ ├── rule_parser_z3.py │ ├── FIXDRIVE strategy repair.txt │ ├── formatted_rules.json │ ├── variables.json │ ├── variable_types.json │ ├── z3_rules.json │ ├── single_rule_results.json │ ├── conflict_results.json │ ├── conflicts_only.json │ └── conflict_report.txt └── README.md ``` JSON 和报告文件会在解析器运行时自动创建。 ## 条件转换 Z3 无法自动理解 DSL 名称的含义，例如： ``` front_vehicle_closer_than(10) ``` 因此，必须在 `CONDITION_DEFINITIONS` 中将每个条件映射到 ADS 变量、类型和运算符。 ``` CONDITION_DEFINITIONS = { "front_vehicle_closer_than": { "variable": "front_distance", "type": "Int", "operator": "<", }, "traffic_light_distance_leq": { "variable": "traffic_light_distance", "type": "Int", "operator": "<=", }, "is_traffic_light": { "variable": "traffic_light_color", "type": "String", "operator": "==", }, } ``` 示例： ``` front_vehicle_closer_than(10) -> front_distance < 10 ``` ``` traffic_light_distance_leq(10) -> traffic_light_distance <= 10 ``` ``` is_traffic_light(red) -> traffic_light_color == "red" ``` 要支持新的条件，请添加另一个条目： ``` "vehicle_speed_greater_than": { "variable": "vehicle_speed", "type": "Int", "operator": ">", } ``` ## 动作转换 动作会转换为等式约束。 ``` follow_dist(10) -> follow_dist == 10 ``` 默认情况下，每个动作都被视为一个独立的变量： ``` ACTION_ALIASES = {} ``` 这一点很重要，因为不相关的参数绝不能被合并。 例如： ``` dynamic_obstacle_stop_dist(10) traffic_light_stop_dist(5) ``` 通常应转换为： ``` dynamic_obstacle_stop_dist == 10 traffic_light_stop_dist == 5 ``` 这些约束是兼容的，因为它们引用了不同的变量。 只有当 ADS 源码分析确认两个动作名称修改的是同一个底层参数时，才应添加别名。 ``` ACTION_ALIASES = { "action_name_a": "shared_parameter", "action_name_b": "shared_parameter", } ``` 使用此映射后： ``` action_name_a(10) action_name_b(5) ``` 将变为： ``` shared_parameter == 10 shared_parameter == 5 ``` Z3 随后会报告冲突，因为一个变量不能同时等于两个不同的值。 ## 冲突检测逻辑 对每一对规则执行两次检查。 ### 1. 条件兼容性 第一个求解器检查： ``` rule1 conditions AND rule2 conditions ``` - `sat`：两条规则可以同时被激活。 - `unsat`：这两条规则不可能在同一场景中出现。 如果条件为 `unsat`，该规则对不会被归类为动作冲突。 ### 2. 组合动作兼容性 当条件可满足时，第二个求解器检查： ``` rule1 conditions AND rule2 conditions AND rule1 actions AND rule2 actions ``` - `sat`：无冲突。 - `unsat`：冲突。 因此，只有当两条规则可以同时被激活，但它们的动作无法同时成立时，才会报告冲突。 ## 运行程序 从项目根目录运行脚本： ``` python -u "Rules encoder/rule_parser_z3.py" ``` 输入文件在程序顶部附近进行配置： ``` INPUT_FILE = Path( "Rules encoder/FIXDRIVE strategy repair.txt" ) ``` 当使用其他规则文件时，请更改此路径。 ## 生成的输出 ### `formatted_rules.json` 存储解析后的规则结构。 ### `variables.json` 存储 Z3 模型中使用的所有变量。 ### `variable_types.json` 存储每个变量推断出的类型。 ``` { "follow_dist": "Int", "front_distance": "Int", "traffic_light_color": "String" } ``` ### `z3_rules.json` 存储原始的 DSL 表达式及其 Z3 表示。 ### `single_rule_results.json` 报告每条规则自身是否可满足。 ### `conflict_results.json` 包含所有已检查的规则对，包括冲突和不冲突的结果。 ### `conflict_report.txt` 提供可读的摘要。 不冲突结果的示例： ``` NO CONFLICT: S1 rule1 vs S1 rule2 Reason: The conditions and actions can all be satisfied at the same time. Condition result: sat Combined result: sat ``` 冲突示例： ``` CONFLICT: Rule A vs Rule B Reason: The rules can be activated together, but some resulting constraints cannot hold together. Exact conflicting constraints: - Rule: Rule A Section: then Original: shared_distance(10) Z3: shared_distance == 10 - Rule: Rule B Section: then Original: shared_distance(5) Z3: shared_distance == 5 ``` ## 故障排除 ### `ImportError: cannot import name 'Bool' from 'z3' 移除错误的包并重新安装正确的包： ``` python -m pip uninstall -y z3 z3-solver python -m pip install --no-cache-dir z3-solver ``` 测试安装： ``` python -c "from z3 import Bool, Int; print(Bool('test'), Int('number'))" ``` ### 某一对规则被错误地报告为冲突 检查 `ACTION_ALIASES`。 推荐默认设置： ``` ACTION_ALIASES = {} ```

标签：Z3求解器, 云安全监控, 云计算, 冲突检测, 形式化验证, 自动驾驶, 规则引擎, 逆向工具, 静态分析