%0 Journal Article
%T Improved SMT-Based Bounded Model Checking for Real-Time Systems<br>改进的以SMT为基础的实时系统限界模型检测
%A XU Liang
%A <br>徐亮
%J 软件学报
%D 2010
%I 
%X SAT-Based bounded model checking (BMC) has high complexity in dealing with real-time systems. Satisfiability modulo theories (SMT) solvers can generalize SAT solving by adding the ability to handle arithmetic and other decidable theories. This paper uses SMT in BMC for real-time systems instead of SAT. The clocks can be represented as integer or real variables directly and clock constraints can be represented as linear arithmetic expressions. These make the checking procedure more efficient. TCTL (timed computation tree logic) is used to specify the properties of real-time systems and improvement of the encodings has been done.
%K bounded model checking
%K satisfiability modulo theories
%K real-time system
%K timed automata
%K timed Kripke structure
%K TCTL (timed computation tree logic)<br>限界模型检测
%K 可满足性模块理论
%K 实时系统
%K 时间自动机
%K 时间Kripke结构
%K 带时间参数的计算树逻辑
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=B8193BAF4E38A8AB7914D6E3F0F48235&yid=140ECF96957D60B2&vid=659D3B06EBF534A7&iid=DF92D298D3FF1E6E&sid=CBBCA10F35A35A94&eid=BD9BFF5428C0CED6&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=34