| FMS建模和形式化验证 |
| |
| 引用本文： | 徐刚,吴智铭.FMS建模和形式化验证[J].系统仿真学报,2004,16(9):1914-1917. |
| |
| 作者姓名： | 徐刚 吴智铭 |
| |
| 作者单位： | 上海交通大学浩然高科技大厦1416信箱,上海,200030 |
| |
| 基金项目： | 国家自然科学基金资助(59889505, 60074011, 70071017) |
| |
| 摘 要： | 提出了一种FMS的建模方法,此方法是基于时间自动机模型。运用模型检查工具UPPAAL来进行建模,仿真和验证。由于时间的因素被考虑到建模方法中,因此FMS的调度和控制问题可以被集成到这个模型中。在系统的行为被控制的同时,可以保证系统的性能指标。从而最优调度和最优控制可以得到检查和验证。
|
| 关 键 词： | 柔性制造系统 死锁 UPPAAL 自动机 甘特图 |
| 文章编号： | 1004-731X(2004)09-1914-04 |
| 修稿时间： | 2003年7月3日 |
Formal Modeling and Verification for FMS |
| |
| U Gang,WU Zhi-ming.Formal Modeling and Verification for FMS[J].Journal of System Simulation,2004,16(9):1914-1917. |
| |
| Authors: | U Gang WU Zhi-ming |
| |
| Abstract: | A modeling method for FMS is presented. This method is based upon the timed automata. Model checker tool UPPAAL is used to model, simulate and verify the FMS model. Because the time is included into the modeling method in this paper, the scheduling and controlling problems in FMS can be integrated into this model. The performance of the system can be guaranteed while the system behavior is controlled. Upon this model, the optimal scheduling and optimal controlling can also be checked and verified. |
| |
| Keywords: | FMS deadlock UPPAAL automaton Gantt chart |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
