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

作     者：裴玉 李宣东 郑国梁 Pei Yu;Li Xuandong;ZHENG Guoliang

作者机构：南京大学计算机软件新技术国家重点实验室 南京大学计算机科学与技术系 南京 210093 

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

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2005年第42卷第1期

页      码：38-46页

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

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

学科分类：0810[工学-土木类] 0808[工学-自动化类] 0839[0839] 08[工学] 0835[0835] 0811[工学-水利类] 081201[081201] 0812[工学-测绘类] 

核心收录：

D　O　I：10.1360/crad20050105

馆 藏 号：203479502...