LDPChecker——一个实时和混成系统模型检验工具  

LDPChecker-A Model Checking Tool for Real-Time and Hybrid System

作　　者：裴玉[1,2] 李宣东[1,2] 郑国梁[1,2] 

机构地区：[1]南京大学计算机软件新技术国家重点实验室 [2]南京大学计算机科学与技术系 南京 210093

出　　处：《计算机研究与发展》2005年第1期38-46,共9页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60073031;60233020)国家"八六三"高技术研究发展计划基金项目(2001AA113203)国家"九七三"重点基础研究发展规划基金项目(2002CB312001)江苏省自然科学基金项目(BK2001033)

摘　　要：混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模.虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机,其对于线性时段性质的满足性能够通过线性规划方法加以检验.为了实现自动检验正环闭合自动机对线性时段性质的满足性,设计并实现了工具LDPChecker.工具LDPChecker能够识别正环闭合自动机并对其进行相应的检验,其主要特色在于它能够对实时和混成系统检验包含可达性在内的许多实时性质,并且能够自动给出诊断信息.Hybrid systems are real-time systems that allow both continuous state changes over time periods of positive durations and discrete state changes in zero time. Being an important subclass of hybrid systems, linear hybrid systems are usually modeled using linear hybrid automata. Linear hybrid automata are undecidable in general, but for a subclass of linear hybrid automata called positive loop-closed automata, the satisfaction problem for linear duration properties can be solved by linear programming. To support automatic checking of linear hybrid automata for linear duration properties, a tool named LDPChecker implementing the checking algorithm has been developed. The tool LDPChecker can identify positive loop-closed automaton and perform checking on it. Its key features includes its ability to check real-time and hybrid system for many real-time properties including reachability property, and to generate diagnostic information automatically.

关 键 词：实时和混成系统 混成自动机 线性时段性质 模型检验 

分 类 号：TP302.1[自动化与计算机技术—计算机系统结构]