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

混成系统是一类复杂系统,线性混成系统作为其重要子类,在形式方法中,人们通常使用线性混成自动机来对它建模．虽然线性混成自动机的模型检验问题总的来说还是不可判定的,但对于其中的正环闭合自动机．其对于线性时段性质的满足性能够通过线性规划方法加以检验．为了实现自动检验正环闭合自动机对线性时段性质的满足性,设计并实现了工具LDPChecker．工具LDPChecker能够识别正环闭合自动机并对其进行相应的检验,其主要特色在于它能够对实时和混成系统检验包含可达性在内的许多实时性质,并且能够自动给出诊断信息．

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

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.