[发明专利]基于UPPAAL的实时嵌入式系统构件间协同行为的验证方法有效
| 申请号： | 201110423095.4 | 申请日： | 2011-12-16 |
| 公开（公告）号： | CN102567163A | 公开（公告）日： | 2012-07-11 |
| 发明（设计）人： | 杜德慧;温岩;冯曙光;包丹珠;徐亚祎;杜丽 | 申请（专利权）人： | 华东师范大学 |
| 主分类号： | G06F11/26 | 分类号： | G06F11/26 |
| 代理公司： | 上海蓝迪专利事务所 31215 | 代理人： | 徐筱梅;张翔 |
| 地址： | 200241 *** | 国省代码： | 上海;31 |
| 权利要求书： | 查看更多 | 说明书： | 查看更多 |
| 摘要： | 本发明公开了一种基于UPPAAL的实时嵌入式系统构件间协同行为的验证方法，该方法是:将对实时嵌入式系统建模形成的MARTE模型转化为工具UPPAAL能够验证的时间自动机，然后使用UPPAAL工具对时间自动机验证，并得出验证结果；根据得出的验证结果可对实时嵌入式系统构件之间交互行为一致性和时间正确性的判断；并对模型采取相应的动作，减少了由模型生成的实时嵌入式系统在运行和操作过程中错误发生的概率。 | ||
| 搜索关键词： | 基于 uppaal 实时 嵌入式 系统 构件 协同 行为 验证 方法 | ||
【主权项】：
一种基于UPPAAL的实时嵌入式系统构件间协同行为的验证方法，其特征在于该方法是：将实时嵌入式系统建模形成的MARTE模型转化为工具UPPAAL能够验证的时间自动机，然后使用UPPAAL工具对时间自动机验证，并得出验证结果；具体包括以下步骤：a、实时嵌入式系统MARTE模型转化为时间自动机ⅰ)、对于MARTE模型中有CCSL约束的MARTE构件图，根据CCSL语义将构件模型转化为仿真自动机； ⅱ)、对于MARTE模型中没有CCSL约束的MARTE构件图，首先，将模型中的MARTE顺序图转化为监控自动机；然后，将模型中的MARTE状态图转化为对象时间自动机； b、使用工具UPPAAL对转化好的时间自动机模型进行验证并输出验证结果。
下载完整专利技术内容需要扣除积分，VIP会员可以免费下载。
该专利技术资料仅供研究查看技术是否侵权等信息，商用须获得专利权人授权。该专利全部权利属于华东师范大学，未经华东师范大学许可，擅自商用是侵权行为。如果您想购买此专利、获得商业授权和技术合作，请联系【客服】
本文链接：http://www.vipzhuanli.com/patent/201110423095.4/，转载请声明来源钻瓜专利网。
- 上一篇：一种分布式文件系统数据访问优化的方法
- 下一篇：一种一体式光衰减器
