| 一种基于时间自动机网络的实时系统形式化验证方法 |
| |
| 引用本文： | 刘传会,张广泉.一种基于时间自动机网络的实时系统形式化验证方法[J].苏州大学学报(医学版),2008,24(1):35-40. |
| |
| 作者姓名： | 刘传会 张广泉 |
| |
| 作者单位： | 苏州大学计算机科学与技术学院,江苏苏州215006 |
| |
| 基金项目： | 江苏省高校自然科学基金
,
重庆市自然科学基金 |
| |
| 摘 要： | 介绍了时间自动机形式模型，在此基础上给出了时间自动机网络的形式语法和语义，然后给出一种基于时间自动机网络的实时系统形式化验证方法，并采用基于时间自动机网络的模型检测工具UPPAAL对一个经典的实时系统实例进行了验证．
|
| 关 键 词： | 实时系统 模型检测 时间自动机网络 UPPAAL |
| 文章编号： | 1000-2073（2008）01-0035-06 |
| 收稿时间： | 2007-06-15 |
| 修稿时间： | 2007年6月15日 |
A formal verification method for real-time system based on networks of timed automata |
| |
| Liu Chuanhui,Zhang Guangquan.A formal verification method for real-time system based on networks of timed automata[J].Journal of Suzhou University(Natural Science),2008,24(1):35-40. |
| |
| Authors: | Liu Chuanhui Zhang Guangquan |
| |
| Institution: | ( School of Computer Science and Technology, Suzhou Univ. , Suzhou 215006, China) |
| |
| Abstract: | On the basis of the formal model of the timed automatas,the formal syntax and semantics of networks of timed automatas are established. Then the method of formal verification of real-time systems based on the networks of automatas is introduced. Finally a well-known real-time system is verified by UPPAAL which is based on the networks of timed automatas. |
| |
| Keywords: | real-time system model checking networks of timed automatas UPPAAL |
| 本文献已被 维普 万方数据 等数据库收录！ |
