| Title: | model checking linear duration invariants of networks of automata |
| Author: | Zhang Miaomiao
; Liu Zhiming
; Zhan Naijun
|
| Source: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
|
| Conference Name: | 3rd IPM International Conference on Fundamentals of Software Engineering, Conference, FSEN 2009
|
| Conference Date: | April 15,
|
| Issued Date: | 2010
|
| Conference Place: | Kish Island, Iran
|
| Keyword: | Computer software
; Model checking
; Permanent magnets
; Real time systems
; Robots
; Safety engineering
; Translation (languages)
|
| Publish Place: | Germany
|
| Indexed Type: | EI
|
| 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. |
| Content Type: | 会议论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/8830
|
| Appears in Collections: | 计算机科学国家重点实验室 _会议论文
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| model checking linear duration invariants of networks of automata.pdf（318KB） | -- | -- | 限制开放 | -- | 联系获取全文 |
|
| Recommended Citation: | |
Zhang Miaomiao,Liu Zhiming,Zhan Naijun. model checking linear duration invariants of networks of automata[C]. 见:3rd IPM International Conference on Fundamentals of Software Engineering, Conference, FSEN 2009. Kish Island, Iran. April 15,.
|
|
|
