[00049800]基于UPPAAL的实时嵌入式系统构件间协同行为的验证方法
技术详细介绍
摘要：本发明公开了一种基于UPPAAL的实时嵌入式系统构件间协同行为的验证方法，该方法是:将对实时嵌入式系统建模形成的MARTE模型转化为工具UPPAAL能够验证的时间自动机，然后使用UPPAAL工具对时间自动机验证，并得出验证结果；根据得出的验证结果可对实时嵌入式系统构件之间交互行为一致性和时间正确性的判断；并对模型采取相应的动作，减少了由模型生成的实时嵌入式系统在运行和操作过程中错误发生的概率。
摘要：本发明公开了一种基于UPPAAL的实时嵌入式系统构件间协同行为的验证方法，该方法是:将对实时嵌入式系统建模形成的MARTE模型转化为工具UPPAAL能够验证的时间自动机，然后使用UPPAAL工具对时间自动机验证，并得出验证结果；根据得出的验证结果可对实时嵌入式系统构件之间交互行为一致性和时间正确性的判断；并对模型采取相应的动作，减少了由模型生成的实时嵌入式系统在运行和操作过程中错误发生的概率。
