摘要
说明了 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.
出处
《华东理工大学学报(自然科学版)》
EI
CAS
CSCD
北大核心
2000年第5期477-480,共4页
Journal of East China University of Science and Technology
基金
国家自然科学基金! ( 6970 30 0 8
6990 30 0 4 )
上海市高等学校青年科学基金! ( 98Q16)
南京大学计算机软件新技术国家重点实验室
关键词
混合系统
混合自动机
符号模型检查
参数分析
hybrid systems
hybrid automata
symbolic model checking
parametric analysis