李明楚

个人信息Personal Information

教授

博士生导师

硕士生导师

主要任职:Director of Academic Committee at Kaifa District

其他任职:开发区校区学术分委员会主任(Director of Academic Committee at Kaifa Campus)

性别:男

毕业院校:多伦多大学

学位:博士

所在单位:软件学院、国际信息与软件学院

学科:软件工程. 运筹学与控制论

办公地点:开发区(Kaifa District Campus)

联系方式:mingchul@dlut.edu.cn

电子邮箱:mingchul@dlut.edu.cn

扫描关注

论文成果

当前位置: 中文主页 >> 科学研究 >> 论文成果

Embedded system modeling and verification based on deterministic and stochastic Petri net

点击次数:

论文类型:期刊论文

发表时间:2014-06-15

发表刊物:Journal of Computational Information Systems

收录刊物:EI、Scopus

卷号:10

期号:12

页面范围:5051-5058

ISSN号:15539105

摘要:Embedded systems are interrupt-driven systems, which achieve interactions with peripherals and environment through the interrupt mechanism, and handle exceptions. However, due to the randomness of trigger method, response with priority, and preemptive execution, interrupt behaviors are hard to accurately predict and interrupt defects are difficult to track. Once a program error is caused by interrupt, it will lead to crashes of the entire embedded system. In this paper, a modeling method of embedded system is proposed based on deterministic and stochastic Petri net (DSPN), which can simulate interrupt processing through three types transitions of DSPN. The upper limit processing time calculation methods of interrupt service are provided for the determinate timed transition. In addition, a model verification method based on the continuous stochastic logic (CSL) for DSPN model is given to analyze the influences of interrupt nesting for embedded system performance, and functional verification and performance evaluation of interrupt-driven embedded systems in one model are also implemented. 1553-9105/Copyright ? 2014 Binary Information Press.