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

【摘要】：模型檢驗(yàn)是一種對有限狀態(tài)系統(tǒng)的性質(zhì)進(jìn)行自動(dòng)檢驗(yàn)的技術(shù),能夠?qū)ο到y(tǒng)設(shè)計(jì)的正確性進(jìn)行驗(yàn)證。線性時(shí)段不變式是一類重要的時(shí)段演算公式,它用來描述實(shí)時(shí)系統(tǒng)的安全性質(zhì)。而擴(kuò)展線性時(shí)段不變式通過命題邏輯和"切變"運(yùn)算對線性時(shí)段不變式進(jìn)行了擴(kuò)展,是更有表達(dá)力的時(shí)段演算公式。由于擴(kuò)展線性時(shí)段不變式不能通過其離散語義下的滿足性來等價(jià)于其連續(xù)語義下的滿足性,離散時(shí)間下的模型檢驗(yàn)算法并不適用于連續(xù)時(shí)間的情況,因此研究連續(xù)時(shí)間下擴(kuò)展線性時(shí)段不變式的模型檢驗(yàn)方法對于實(shí)時(shí)系統(tǒng)的性質(zhì)檢驗(yàn)具有重要的實(shí)用意義。該文提出了連續(xù)時(shí)間下針對擴(kuò)展線性時(shí)段不變式的有界模型檢驗(yàn)算法,根據(jù)離散化方法將連續(xù)時(shí)間下的問題轉(zhuǎn)化為離散情況,通過迭代地調(diào)用離散時(shí)間下線性時(shí)段不變式的有界模型檢驗(yàn)算法,來解決研究的問題。實(shí)驗(yàn)表明,該文提出的算法能夠有效地對連續(xù)時(shí)間下的擴(kuò)展線性時(shí)段不變式進(jìn)行有界模型檢驗(yàn)。
[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.
【作者單位】： 同濟(jì)大學(xué);
【基金】：擴(kuò)展的線性時(shí)段不變式的模型檢驗(yàn)(項(xiàng)目編號:F020106)
【分類號】：TP311.53

【相似文獻(xiàn)】

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

1 李曉山，周巢塵;時(shí)段演算綜述[J];計(jì)算機(jī)學(xué)報(bào);1994年11期

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

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

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

5 ;[J];;年期

，

本文編號：1949238