Modeling and verification of real-time embedded systems with urgency

Tunghai University Institutional Repository > 工學院 > 資訊工程學系所 > 期刊論文 > Item 310901/22686

jsp.display-item.identifier=請使用永久網址來引用或連結此文件: http://140.128.103.80:8080/handle/310901/22686

题名:	Modeling and verification of real-time embedded systems with urgency
作者:	Hsiung, P.-A.a, Lin, S.-W.a, Chen, Y.-R.b, Huang, C.-H.a, Shih, C.c, Chu, W.C.
贡献者:	Department of Computer Science, Tunghai University
关键词:	Formal verification;Modeling;Urgency
日期:	2009
上传时间:	2013-05-21T09:14:24Z (UTC)
摘要:	Real-time embedded systems are often designed with different types of urgencies such as delayable or eager, that are modeled by several urgency variants of the timed automata model. However, most model checkers do not support such urgency semantics, except for the IF toolset that model checks timed automata with urgency against observers. This work proposes an Urgent Timed Automata (UTA) model with zone-based urgency semantics that gives the same model checking results as absolute urgency semantics of other existing urgency variants of the timed automata model, including timed automata with deadlines and timed automata with urgent transitions. A necessary and sufficient condition, called complete urgency, is formulated and proved for avoiding zone partitioning so that the system state graphs are simpler and model checking is faster. A novel zone capping method is proposed that is time-reactive, preserves complete urgency, satisfies all deadlines, and does not need zone partitioning. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces. ? 2009 Elsevier Inc. All rights reserved.
關聯:	Journal of Systems and Software Volume 82, Issue 10, October 2009, Pages 1627-1641
显示于类别:	[資訊工程學系所] 期刊論文

文件中的档案:

档案	大小	格式	浏览次数
index.html	0Kb	HTML	131	检视/开启

在THUIR中所有的数据项都受到原著作权保护.

数据加载中.....