Analysis of Interrupt Behavior Based on Probabilistic Model Checking

Gang Hou, Weiqiang Kong, Kuanjiu Zhou, Jie Wang, Xun Cao, Akira Fukud

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2018 7th International Congress on Advanced Applied Informatics, IIAI-AAI 2018
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages86-91
Number of pages6
ISBN (Electronic)9781538674475
DOIs
Publication statusPublished - Jul 2 2018
Event7th International Congress on Advanced Applied Informatics, IIAI-AAI 2018 - Yonago, Japan
Duration: Jul 8 2018Jul 13 2018

Publication series

NameProceedings - 2018 7th International Congress on Advanced Applied Informatics, IIAI-AAI 2018

Conference

Conference7th International Congress on Advanced Applied Informatics, IIAI-AAI 2018
CountryJapan
CityYonago
Period7/8/187/13/18

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Communication
  • Information Systems
  • Information Systems and Management
  • Education

Cite this

Hou, G., Kong, W., Zhou, K., Wang, J., Cao, X., & Fukud, A. (2018). Analysis of Interrupt Behavior Based on Probabilistic Model Checking. In Proceedings - 2018 7th International Congress on Advanced Applied Informatics, IIAI-AAI 2018 (pp. 86-91). [8693475] (Proceedings - 2018 7th International Congress on Advanced Applied Informatics, IIAI-AAI 2018). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/IIAI-AAI.2018.00026