半形式化设计验证：Petri网与系统模拟
1. 模拟启动与停止的时机
1.1 启动时机
在模拟过程中，简单的模拟示例通常不会出现复杂模拟中常见的启动错误。一般来说，模拟包含等待服务器处理的事务队列（如等待通信栈处理的传入数据包队列）和多个服务器。初始时，队列是空的，服务器处于空闲状态。在模拟运行一段时间之前，它对真实系统稳态行为的建模是不准确的。
因此，通常的做法是让模拟达到稳态，然后重置所有统计数据（如队列长度、服务器利用率等），再重新开始收集统计数据。然而，确定何时进行重置是很困难的：重置过早，结果会不准确；重置过晚，则会浪费处理时间。
1.2 停止时机
确定何时停止收集统计数据比确定何时开始更困难。例如，在某些模拟中运行了500年，而不是10年或1000年。如果系统存在罕见事件，这将成为一个特殊问题。如果模型中大多数事件每毫秒发生一次，但某个特定事件（如故障）每5年才发生一次，为了使该罕见事件具有统计意义，可能需要运行50年的模拟时间。在这段时间里，每毫秒发生的事件将发生约$10^{12}$次。建模者的任务就是避免这种情况。
决定模拟运行时长的主要实际标准是监控关键统计数据，并观察它们是否不再有显著变化。
2. 定时Petri网
2.1 标准中的Petri网
IEC 61508 - 3在表A.1中推荐使用半形式化方法，并参考了表B.7，其中列出了几种在规范中被认为是半形式化的方法，包括定时Petri网（IEC 61508称之为时间Petri网）。ISO 26262虽未明确提及Petri网，但第6部分表4中对“设计动态部分的模拟”的引用及其附
