TY - GEN
T1 - Analysis of Interrupt Behavior Based on Probabilistic Model Checking
AU - Hou, Gang
AU - Kong, Weiqiang
AU - Zhou, Kuanjiu
AU - Wang, Jie
AU - Cao, Xun
AU - Fukud, Akira
N1 - Funding Information:
ACKNOWLEDGMENT This work is supported by the National Nature Science Foundation of China (Grant No. 61402073, 61572097, 61472100), the Fundamental Research Funds for the Central Universities (Grant No. DUT17JC26, DUT18JC08) and the JSPS KAKENHI (Grant No. 15H05708).
Publisher Copyright:
© 2018 IEEE.
PY - 2018/7/2
Y1 - 2018/7/2
N2 - Vehicles automated driving system belongs to real-time embedded system, which is an important application in the field of intelligent transport. In the design of trustworthy real-time embedded systems, the interrupt mechanism plays an important role. Due to the randomness and non-deterministic of interrupt handling, the behaviors of interrupt are difficult to be analyzed. To solve this problem, we propose an interrupt behavior model based on extended deterministic and stochastic Petri nets (EDSPN). In order to analyze the EDSPN model, we presented the formal definition of labeled Markov regenerative processes (LMRGP) for EDSPN. On the basis of LMRGP, we put forward a probabilistic model checking method of continuous stochastic logic (CSL). Finally, by analyzing the multi-level interrupt model, the non-deterministic behaviors of interrupt are quantitatively analyzed, and effectiveness of the proposed method is proved.
AB - Vehicles automated driving system belongs to real-time embedded system, which is an important application in the field of intelligent transport. In the design of trustworthy real-time embedded systems, the interrupt mechanism plays an important role. Due to the randomness and non-deterministic of interrupt handling, the behaviors of interrupt are difficult to be analyzed. To solve this problem, we propose an interrupt behavior model based on extended deterministic and stochastic Petri nets (EDSPN). In order to analyze the EDSPN model, we presented the formal definition of labeled Markov regenerative processes (LMRGP) for EDSPN. On the basis of LMRGP, we put forward a probabilistic model checking method of continuous stochastic logic (CSL). Finally, by analyzing the multi-level interrupt model, the non-deterministic behaviors of interrupt are quantitatively analyzed, and effectiveness of the proposed method is proved.
UR - http://www.scopus.com/inward/record.url?scp=85065201449&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85065201449&partnerID=8YFLogxK
U2 - 10.1109/IIAI-AAI.2018.00026
DO - 10.1109/IIAI-AAI.2018.00026
M3 - Conference contribution
AN - SCOPUS:85065201449
T3 - Proceedings - 2018 7th International Congress on Advanced Applied Informatics, IIAI-AAI 2018
SP - 86
EP - 91
BT - Proceedings - 2018 7th International Congress on Advanced Applied Informatics, IIAI-AAI 2018
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 7th International Congress on Advanced Applied Informatics, IIAI-AAI 2018
Y2 - 8 July 2018 through 13 July 2018
ER -