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在另一种论文中提出了在并发系统上下文中提高了效率的进一步提高，其中识别了每个Contracexample片段的最小冲突约束（这使得片段无效），并用于说明放松。我们采用了上述LHAVRF的关键思路，增加了额外的功能，如它自动组成并发子系统模型。每当满足到不安全状态的可达性时，输出提供了一个具体的反例，其中值分配给变量。 LHAVRF通过应用于Fischer互斥协议来说明。
展开▼
