# test-framework

**Repository Path**: liang63600/test-framework

## Basic Information

- **Project Name**: test-framework
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2025-11-04
- **Last Updated**: 2025-11-17

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# 模型检查指导的测试
模型检查指导的测试核心思想是 对一个系统进行正确建模，有了模型后，看系统实际行为和模型中的行为是否一致。比如模型中在状态1执行动作A到达状态2，
那么实际系统也应该在状态1执行动作A到达状态2，如果实际系统不是到达状态2而是状态3，那么发现了实际系统中的缺陷。

模型检查指导的测试主要分成以下步骤
## 1 对系统的行为进行形式化建模
对系统构建一个期望的模型，例如用形式化语言TLA+表达

## 2 利用模型检查器检查模型生成状态图
有了TLA+编写的模型后，可以使用TLC模型检查器对模型进行检查，验证模型正确，验证后会生成一个状态图。
状态图本质是一个状态机，包含了系统在模型层面的所有状态转移。
当前状态图用`.dot`文件表示，可以参见`mystate.dot`。

## 3 遍历状态图自动生成测试用例
一个测试用例是一个期望的“状态和动作序列”，例如测试用例"状态s1 -Sub(N1, t1)-> s2 -Join(N1,N2)-> s3"表示系统从初始状态s1开始，先执行N1订阅topic t1后
到达状态s2，然后执行N1 join N2动作后到达s3状态。

* 如何自动生成测试用例 
  
  执行命令`python testcase_generator_dfs.py mystate.dot ./myOutput/`生成测试用例，参数`mystate.dot`表示状态图文件名，`./myOutput/`表示生成的测试用例所在路径

## 4 自动执行测试用例
对于每个测试用例，按照动作顺序在实际系统中通过curl命令执行。例如测试用例"状态s1 -Sub(N1, t1)-> s2 -Join(N1,N2)-> s3"执行时，先让实际系统处于初始状态，然后利用curl执行Sub(N1,t1)动作，
执行完后收集实际系统状态sImpl和期望状态s2比较，如果不一致，则发现可能的缺陷。

* 如何自动执行测试用例
  
  * 执行参数配置，执行前，需要配置一下`test_framework.py`中的一个参数`WORKDIR`，当前是`WORKDIR = "/home/work/remoteProject/fleet-merge/crates/fleet-datamgr/build/public-api/"`，

    需要将路径前缀`/home/work/remoteProject/`替换成你现在`fleet-merge`项目所在的实际路径，其余参数可以不变（需要保证端口14001-1400i与15001-1500i处于空闲，其中i表示总共集群节点数，保证不了的话，需要修改端口配置）

  * 执行命令`python test_framework.py`，执行结束后，发现的缺陷将保存在目录`$WORKDIR$/results`下。

* 缺陷记录说明

  若第i个测试用例（从0开始）出错，那么会在目录`$WORKDIR$/results`下生成一个bug报告文件（例如`15_TimeoutExpired`表示第15个测试用例，报的python执行error是TimeoutExpired） 
  和一个触发bug时系统状态的文件夹（例如`15`），文件夹下分为Ni（表示节点Ni的数据所在文件夹）,NiLog（表示节点Ni日志所在文件夹）,cmdout_Ni.log（表示节点Ni命令行输出的内容）