pIML -- An Interrupt Program Modelling Language for Real-Time and Embedded Systems

In the design of dependable software for real-time and embedded systems, the quantitative analysis of program behavior and system performance is a crucial but extremely difficult issue, the challenge of which is exacerbated due to the random city and nondeterminism of interrupt events and the corresponding handling behaviors. Moreover, time analysis is also need to be taken into account for such kinds of systems. Thus the research on a theory which integrates interrupt behaviors and time analysis seems to be important and challenging. In this paper, we propose an interrupt modeling language pIML including the probabilistic feature to describe the programs with interrupts. We explore a probabilistic operational semantics to depict the actions of pIML. Meanwhile, we also implement this operational semantics we proposed on Maude platform, which fill the gap between the theory and practice. Maude supports rewriting logic, equational logic, and etc. The rewrite rules of rewriting logic can very well implement the transition rules of probabilistic operational semantics. Based on this implementation, it is very convenient to simulate the program written in pIML and analyze the behaviors of program in the presence of interrupts quantitatively.