Institutional Repository
| model checking linear duration invariants of networks of automata | |
| Zhang Miaomiao; Liu Zhiming; Zhan Naijun | |
| 2010 | |
| Conference Name | 3rd IPM International Conference on Fundamentals of Software Engineering, Conference, FSEN 2009 |
| Source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 244-259 |
| Conference Date | April 15, |
| Conference Place | Kish Island, Iran |
| Indexed Type | EI |
| Publish Place | Germany |
| ISSN | 3029743 |
| ISBN | 3642116221 |
| Department | (1) School of Software Engineering, Tongji University, Shanghai, China; (2) International Institute of Software Technology, United Nations University, China; (3) Lab. of Computer Science, Institute of Software, CAS, Beijing, China |
| English Abstract | Linear duration invariants (LDIs) are important safety properties of real-time systems. In this paper, we reduce the problem of verification of a network of timed automata against an LDI to an equivalent problem of model checking whether a failure state is never reached. Our approach is first to transform each component automaton Ai of the network A to an automaton Gi. The transformation helps us to record entry and exit to critical locations that appear in the LDI. We then introduce an auxiliary checker automaton S and define a failure state to verify the LDI on a given interval. Since a model checker checks exhaustively, a failure of the checker automaton to find the failure state will prove that the LDI holds. © 2010 Springer. |
| Keyword | Computer Software Model Checking Permanent Magnets Real Time Systems Robots Safety Engineering Translation (Languages) |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/8830 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | Zhang Miaomiao,Liu Zhiming,Zhan Naijun. model checking linear duration invariants of networks of automata[C]. Germany,2010:244-259. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| model checking linea（318KB） | 开放获取 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment