基于UPPAAL的实时嵌入式系统构件间协同行为的验证方法

摘要

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

主权项

一种基于UPPAAL的实时嵌入式系统构件间协同行为的验证方法，其特征在于该方法是：将实时嵌入式系统建模形成的MARTE模型转化为工具UPPAAL能够验证的时间自动机，然后使用UPPAAL工具对时间自动机验证，并得出验证结果；具体包括以下步骤：a、实时嵌入式系统MARTE模型转化为时间自动机ⅰ)、对于MARTE模型中有CCSL约束的MARTE构件图，根据CCSL语义将构件模型转化为仿真自动机； ⅱ)、对于MARTE模型中没有CCSL约束的MARTE构件图，首先，将模型中的MARTE顺序图转化为监控自动机；然后，将模型中的MARTE状态图转化为对象时间自动机； b、使用工具UPPAAL对转化好的时间自动机模型进行验证并输出验证结果。