Hits:

Indexed by:会议论文

Date of Publication:2018-01-01

Included Journals:CPCI-S、EI

Page Number:86-91

Key Words:real-time embedded system; interrupt behavior; continuous stochastic logic; probabilistic model checking

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.