调试或映射出大型状态机？

Question

我正在尝试调试一段代码，它主要是一个简单的 16 状态状态机，尽管在某些情况下转换不是很简单（状态更改操作的数据大约是 200 字节的数据）几个 C++ 类）。

我们发现机器比预期更早地进入“最终”状态。由于我对代码还不是很熟悉，我希望我可以尝试找出不同的状态和转换，以便我更容易快速识别和调试不同的转换路径。

是否有任何有用的工具或技术可以映射出这样的状态机？

值得注意的是，我是从逆向工程的角度来做这件事的，所以我没有可用的系统规划文档。

Answer 1

您可以查看正式的模型检查工具，例如 UPPAAL。该工具可用于建模和验证任何可以建模为定时自动机网络的系统 - 这包括状态机。我以前用它来验证例如可能状态的不变量和可达性。