A concurrent linear hybrid automaton is composed of a set of linear hybrid automata and is used to model linear hybrid systems. Each component's behavior exhibits both discrete and continuous dynamics. We have developed LhaVrf, a symbolic verifier for the reachability verification of concurrent linear hybrid automata. The implementation is based on the algorithm proposed in S. Jiang's papers. In his paper, reachability problem of linear hybrid automata was first reduced to one for linear transition systems, whose reachability analysis was then performed by using counterexample fragment based specification relaxation. S. Jiang proposed in another paper further enhancement in efficiency in context of concurrent systems, where for each counterexample fragment, a minimal conflicting constraints set was identified (that makes the fragment invalid), and used for specification relaxation. We adopted the above key ideas in the implementation of LhaVrf, with added features such as it automatically composes the concurrent subsystem models. Whenever the reachability to an unsafe state is satisfied, the output provides a concrete counterexample with values assigned to the variables. The LhaVrf is illustrated via an application to the Fischer mutual exclusion protocol.
展开▼
机译：并发线性混合自动机由一组线性混合自动机组成，用于建模线性混合系统。每个组件的行为都表现出离散的和连续的动态。我们已经开发了LhaVrf，这是用于并行线性混合自动机可达性验证的符号验证器。该实现基于S. Jiang的论文中提出的算法。在他的论文中，对于线性过渡系统，线性混合自动机的可达性问题首先被简化为一个问题，然后通过使用基于反例片段的规范松弛来执行其可达性分析。 S. Jiang在另一篇论文中提出了在并发系统中进一步提高效率的方法，在该系统中，对于每个反例片段，都将识别出一个最小的冲突约束集（使该片段无效），并将其用于规范松弛。我们在LhaVrf的实现中采用了上述关键思想，并添加了诸如自动组合并发子系统模型之类的功能。只要满足了到不安全状态的可达性，输出就会提供一个具体的反例，并将值分配给变量。通过应用到Fischer互斥协议的方式说明了LhaVrf。
展开▼
