高级检索

    潘国强, 虞慧群. 线性混合系统符号模型验证中的参数分析方法[J]. 华东理工大学学报(自然科学版), 2000, (5): 477-480.
    引用本文: 潘国强, 虞慧群. 线性混合系统符号模型验证中的参数分析方法[J]. 华东理工大学学报(自然科学版), 2000, (5): 477-480.
    Parametric Analysis of Linear Hybrid Systems by Symbolic Model-checking[J]. Journal of East China University of Science and Technology, 2000, (5): 477-480.
    Citation: Parametric Analysis of Linear Hybrid Systems by Symbolic Model-checking[J]. Journal of East China University of Science and Technology, 2000, (5): 477-480.

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

    Parametric Analysis of Linear Hybrid Systems by Symbolic Model-checking

    • 摘要: 说明了HYTECH工具中采用的参数分析方法对系统描述能力的限制,提出了分离参数变量和系统状态变量的符号模型检查算法,并对用HYTECH不能分析的Fischer互斥算法的时钟偏移的界进行了分析。

       

      Abstract: 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.

       

    /

    返回文章
    返回