线性混合系统的一种验证方法

混合系统是指嵌入于物理环境中的数字实时系统．由于计算机技术的快速发展，混合系统在各行各业中都得到广泛应用，但是由于混合系统涉及到连续时间，因此其验证问题始终没有得到完善的解决．近年来，人们普遍采用模型检验方法对混合系统进行验证．由于线性混合系统在实际应用中可以表示大多数的嵌入式实时系统，因此我们着重研究这类混合系统的验证算法．本文首先介绍了混合系统的模型—混合自动机，然后提出了一种针对线性混合系统的基于区域的先划分再遍历的半确定性验证方法．经实例检验，该方法能够有效地验证线性混合系统．最后将本文的方法同有关的其它算法进行了比较

A VERIFICATION PROCEDURE FOR LINEAR HYBRID SYSTEMS

Hybrid systems are the digital real time systems embedded in physical environment. Due to rapid development of computer technology, there are a lot of applications of hybrid systems, automobiles, air planes and nuclear stations for example. However, the verification of hybrid systems is not well solved because they involve continuous time. Recently, model checking is used to verify these systems. Model checking is a practical verification technique which enumerates the whole state space of system model from initial state in order to find a final state which satisfies the specification of the system. Model checking originally was proposed to verify some small scale protocols and hardware designs. Those cases all had the finite state spaces. There were a lot of successful cases using model checking in those fields. When systems consist of many concurrent processes or involve continuous time, state explosion problem hinders model checking directly, especially the infinite state space in the continuous time real time systems. Then symbolic presentation and region methods are proposed successively to reduce the whole state space into finite one. We focus on the verification algorithm for linear hybrid systems because they are the most usual applications in industry and most hybrid systems can be directly or approximately described by them. This paper first introduces hybrid automaton, which is the model of a hybrid system. Then it introduces linear hybrid automaton and two types of transitions in hybrid automaton, which are state transition and time passing transition. In order to attack infinite state space, we reduce infinite state space into finite region. Region is constructed by constraint of node. Different states in the same region can be transferred only by time passing transition and they are in the same node of automaton. State transition results in region transition. According to state trajectory in automaton, we introduce region trajectory. Based on region, we propose an effective verification procedure, which is semi decidable. The procedure first splits the whole state space according to constraints at each node and calculating its foreword state region. If the calculated foreword state region coincides with the original relevant state region, calculation continues. Otherwise original relevant state region must be divided into two new regions. If the partition calculation can terminate, the infinite state space can be reduced into finite regions. Otherwise this system cannot be verified. Then the procedure tries to search a reachable region trajectory. An benchmark, which is called temperature controlling system, is used to test our procedure. At last, this procedure is compared with other relevant algorithms.