论文部分内容阅读
时间自动机是具有时间约束的有限状态转换系统,在实时系统进行形式化证明的过程中,先用它建模,然后再检验某些不安全状态是否可达。所以研究时间自动机及其验证技术,主要研究它的状态可达性问题。然而由于在它的语义描述中时间自动机的状态是无穷的,因而计算它的状态可达性关系显得尤为复杂。时间自动机中各时钟的值可以取连续的正实数值,为状态可达性关系的计算带来了许多不便,所以本文在R.Alur和D.L.Dill提出的时间转换系统等价转化的基础上给出了在时间自动机中可以通过等价转化将所有的时钟约束转化为仅含有整数值约束常量的约束,并且分析了这种转化对时间自动机两类转换的影响及其等价性证明。求解时间自动机状态可达性关系的关键问题在于对各个时钟的时间约束关系的处理。R.Alur和D.L.Dill提出的域自动机构造方法通过对状态空间进行等价划分构造有限自动机,然后通过对有限自动机的分析求解状态可达性关系。JohanBengtsson提出了含有形如x-y~n(其中,~∈{<,>,=,≤,≥})的时间自动机状态可达性关系的计算方法。Felice Balarin提出的近似计算方法实际上计算出的只是可达状态集的超集,这种超集有时候会证明一个正确的系统是不正确的,但是它不会使得一个不正确的系统被证明是正确的。Catalin Dima将复位点语义应用于时间自动机,通过对原子关系的合成、并和自反传递闭包进行运算求解可达状态集。本文研究分析了上述几种求解方法。然后针对符号化的时间自动机语义在对所有大于时钟约束常量最大值的那些时钟值进行等价处理时不能处理形如x-y~n的时钟约束这种情况,提出了一种改进算法,这种算法将两个不同时钟之间的相互约束看成一个独立的时钟来处理,在进行等价处理之前,首先求出所有任意两个时钟之间的约束的最大常量矩阵,然后据此矩阵再求解时间自动机的可达状态集便可以得出正确的结果。本文通过分析指出了这种改进算法的可行性及正确性。这种算法的优点在于,它不仅考虑到了任意两个时钟约束的最大常量,而且此算法还具有一定的通用性。