基于UPPAAL的实时嵌入式系统构件间协同行为的验证方法专利登记公告

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

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

专利类型：发明专利

专利号：CN201110423095.4

专利申请（专利权）人：华东师范大学

专利发明（设计）人：杜德慧;温岩;冯曙光;包丹珠;徐亚祎;杜丽

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

专利地区：上海