本文選題：模型檢驗 + 時間自動機��； 參考：《電腦知識與技術(shù)》2016年28期

【摘要】：模型檢驗是一種對有限狀態(tài)系統(tǒng)的性質(zhì)進行自動檢驗的技術(shù),能夠?qū)ο到y(tǒng)設(shè)計的正確性進行驗證。線性時段不變式是一類重要的時段演算公式,它用來描述實時系統(tǒng)的安全性質(zhì)。而擴展線性時段不變式通過命題邏輯和"切變"運算對線性時段不變式進行了擴展,是更有表達力的時段演算公式。由于擴展線性時段不變式不能通過其離散語義下的滿足性來等價于其連續(xù)語義下的滿足性,離散時間下的模型檢驗算法并不適用于連續(xù)時間的情況,因此研究連續(xù)時間下擴展線性時段不變式的模型檢驗方法對于實時系統(tǒng)的性質(zhì)檢驗具有重要的實用意義。該文提出了連續(xù)時間下針對擴展線性時段不變式的有界模型檢驗算法,根據(jù)離散化方法將連續(xù)時間下的問題轉(zhuǎn)化為離散情況,通過迭代地調(diào)用離散時間下線性時段不變式的有界模型檢驗算法,來解決研究的問題。實驗表明,該文提出的算法能夠有效地對連續(xù)時間下的擴展線性時段不變式進行有界模型檢驗。
[Abstract]:Model checking is a kind of automatic verification technology for the properties of finite state system, which can verify the correctness of system design. Linear time invariant is a kind of important time interval calculus formula, which is used to describe the security property of real time system. The extended linear time invariant extends the linear period invariant by propositional logic and "shear" operation, which is a more expressive formula of time interval calculus. Because the extended linear time invariant can not be equivalent to the satisfaction under its continuous semantics by the satisfaction of its discrete semantics, the model checking algorithm in discrete time is not suitable for continuous time. Therefore, it is of great practical significance to study the model checking method of extended linear time invariant in continuous time for the property test of real time systems. In this paper, a bounded model checking algorithm for the invariant of extended linear time period in continuous time is proposed. According to the discretization method, the problem under continuous time is transformed into discrete case. The problem is solved by iteratively calling the bounded model checking algorithm of linear time invariant in discrete time. Experiments show that the proposed algorithm can effectively test the extended linear time invariant in continuous time.
【作者單位】： 同濟大學(xué);
【基金】：擴展的線性時段不變式的模型檢驗(項目編號:F020106)
【分類號】：TP311.53

【相似文獻】

相關(guān)期刊論文 前5條

1 李曉山，周巢塵;時段演算綜述[J];計算機學(xué)報;1994年11期

2 梁愛麗;朱嘉奇;王捍貧;屈婉玲;;一種新的時段演算及其驗證[J];計算機研究與發(fā)展;2008年S1期

3 吳鋒;;定性/定量集成優(yōu)化控制器的形式化設(shè)計方法[J];化工學(xué)報;2010年08期

4 侯建民,李宣東,鄭國梁;離散時段演算的符號模型驗證[J];計算機學(xué)報;1998年02期

5 ;[J];;年期

，

本文編號：1949238