文献类型：期刊文献

中文题名：线性混合系统符号模型验证中的参数分析方法

英文题名：Parametric Analysis of Linear Hybrid Systems by Symbolic Model-checking

作者：潘国强[1];虞慧群[1];宋国新[1];邵志清[1]

机构：[1]华东理工大学计算机科学与工程系,上海200237

年份：2000

卷号：26

期号：5

起止页码：477

中文期刊名：华东理工大学学报（自然科学版）

外文期刊名：Journal of East China University of Science and Technology

收录：CSTPCD;;国家哲学社会科学学术期刊数据库;EI(收录号：2001015500644);Scopus;北大核心:【北大核心1996】；CSCD:【CSCD2011_2012】；

基金：国家自然科学基金! ( 6970 30 0 8;6990 30 0 4 );上海市高等学校青年科学基金! ( 98Q16);南京大学计算机软件新技术国家重点实验室

语种：中文

中文关键词：混合系统;混合自动机;符号模型检查;参数分析

外文关键词：hybrid systems; hybrid automata; symbolic model checking; parametric analysis

摘要：说明了 HYTECH工具中所采用的参数分析方法对系统描述能力的限制 ;提出了分离参数变量和系统状态变量的符号模型检查算法 ,并对用 HYTECH不能分析的 Fischer互斥算法的时钟偏移的界进行了分析。
In the model checking of linear hybrid systems, the implementation of parameteric analysis depends on maintaining the parameters in symbolic form. In this direction, parametric variables can be kept with the system variables, or stored and considered separately. The first method is usually used because it is easy to implement, but it restricts the descriptive capability of the system. By analyzing the symbolic model checking process, we choose to store the parametric variables separately in symbolic form and we give a model checking algorithm for this description. As an example, the limit to clock skew in a Fischer mutex system is analyzed.