|
|||||
|
|
| 基于时间自动机的实时系统建模及验证 | |
| 引用本文： | 吴永刚,陆慧娟,程倬,陈江.基于时间自动机的实时系统建模及验证[J].计算机时代,2011(6):1-3. |
| 作者姓名： | 吴永刚 陆慧娟 程倬 陈江 |
| 作者单位： | 1. 中国计量学院信息工程学院,浙江杭州,310018 2. 中国计量学院信息工程学院,浙江杭州310018;中国矿业大学信息与电气工程学院 3. 浙江网新恒天软件技术有限公司 |
| 摘 要： | 实时系统必须在一个事先定义好的时间限制内对来自外部或内部的事件进行响应,如何有效验证实时模型的正确性和安全性是一个难点.文章通过多个时间自动机来模拟实时系统中的各个对象,并用UPPAAL对模型进行验证,减少了模型验证的状态搜索空间,为实时嵌入式系统开发和验证提供了一种可行、安全的控制机制.实验结果显示了系统的有效性. |
| 关 键 词： | 时间自动机 实时系统 UPPAAL 模型验证 |
Real-time system's modeling and verification based on Time Automata |
|
| WU Yong-gang,LU Hui-juan,CHENG Zhuo,CHEN Jiang.Real-time system's modeling and verification based on Time Automata[J].Computer Era,2011(6):1-3. | |
| Authors: | WU Yong-gang LU Hui-juan CHENG Zhuo CHEN Jiang |
| Affiliation: | 1.College of Information Engineering,China Jiliang University,Hangzhou,Zhejiang 310018,China;2.Insigma Hengtian Software Ltd.; 3.School of Information & Electronic Engineering;China University of Mining & Technology) |
| Abstract: | Real-Time system is the system that must response the external or internal events in a pre-defined time.Certificating the security and reliability of the model is one of the difficult.This paper uses time-automata to simulate the objects in real-time system,and uses UPPAAL to verify the model.It can reduce the search of the state space;provide a feasible and safe control method for real-time embedded systems development and verification.Experiment shows that the method is effective. |
| Keywords: | UPPAAL |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |
