科技视界
科技視界
과기시계
Science&Technology Vision
2013年
34期
149-151,176
,共4页
形式化验证%线性时段不变式%时间自动机%反向系统
形式化驗證%線性時段不變式%時間自動機%反嚮繫統
형식화험증%선성시단불변식%시간자동궤%반향계통
Formal verification%Timed automata%Linear duration invariants%Backward system
线性时段不变式是一类重要的时段演算公式，可以用来描述实时系统的时段性质，对其验证算法的研究具有相当高的理论意义和实际应用价值。文献[3]中提出的算法在验证某些公式时需要引入韵（遭）个辅助变量，庞大的变量数目会限制该算法在实际工业领域的应用。针对该问题，本文提出了一种新颖的解决思路---通过反转原系统得到其反向系统，然后在反向系统上验证对应的反向公式。它与在原系统上验证正向公式的结果等价，但只需引入韵（1）个辅助变量，扩大了文献[3]所提算法在实际工业领域的适用范围。
線性時段不變式是一類重要的時段縯算公式，可以用來描述實時繫統的時段性質，對其驗證算法的研究具有相噹高的理論意義和實際應用價值。文獻[3]中提齣的算法在驗證某些公式時需要引入韻（遭）箇輔助變量，龐大的變量數目會限製該算法在實際工業領域的應用。針對該問題，本文提齣瞭一種新穎的解決思路---通過反轉原繫統得到其反嚮繫統，然後在反嚮繫統上驗證對應的反嚮公式。它與在原繫統上驗證正嚮公式的結果等價，但隻需引入韻（1）箇輔助變量，擴大瞭文獻[3]所提算法在實際工業領域的適用範圍。
선성시단불변식시일류중요적시단연산공식，가이용래묘술실시계통적시단성질，대기험증산법적연구구유상당고적이론의의화실제응용개치。문헌[3]중제출적산법재험증모사공식시수요인입운（조）개보조변량，방대적변량수목회한제해산법재실제공업영역적응용。침대해문제，본문제출료일충신영적해결사로---통과반전원계통득도기반향계통，연후재반향계통상험증대응적반향공식。타여재원계통상험증정향공식적결과등개，단지수인입운（1）개보조변량，확대료문헌[3]소제산법재실제공업영역적괄용범위。
Linear duration invariants (LDI) form an important class of duration calculus formulae, which can be used to describe duration properties of real-time systems. The research on verification algorithms of LDIs has profound theoretical significance and extensive applied value. The literature[3] has proposed a verification algorithm which needs to introduce O(b) auxiliary variables when verifying some formulae. This will strongly restrict its application in practical industrial fields. To solve this problem, this paper presents a novel idea which firstly reverses the original system into its backward version and then verifies the corresponding backward formulae over it. And this doesn't change the original verification result and only needs to introduce O(1)variables, which greatly extends the scope of industrial application of the algorithm proposed in [3].
