Is LTL model-checking effective for Diagnosability Verification?
IFAC-PapersOnLine(2020)
摘要
In this work we propose a model checking approach to deal with the problem of the diagnosability verification. In this approach we consider the normal and the faulty behavior of a transition system (TS). We describe the diagnosability property by using an unique linear temporal logic (LTL) formula. Using LTL model checking we can test if the system is not diagnosable if it does not satisfy our proposed LTL-formula. Our approach can be carried out in SPIN model checker which is a tool used for formal verification of models. One advantage of SPIN is that it can handle a large state space which can be useful for diagnosability verification of complex system. We illustrate the effectiveness of our approach by means of a scalable benchmark of a railway level crossing system for n tracks and compare the results found with the ones found using typical tools for verification of diagnosability of Discrete Event Systems (DES).
更多查看译文
关键词
Diagnosis,Model-Checking,Transition Systems,Linear Temporal Logic,Discrete approaches for hybrid systems,Tools
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要