| With the rapid development of the computer industry, real-time and embedded sys-tems have been widely used in various areas, such as manufacturing, domestic appliances, automobile, aviation and aircraft, etc. Both logical correctness and time properties should be considered for the dependability of such systems. The interrupt mechanism is intro-duced as an interface between the kernel and devices, which ensures the system to interact with its environment timely. Due to the fact that the trigger of interrupt requests is usually random and nondeterministic, it makes extremely difficult for reasoning about the behav-iors of systems and time analysis. It also brings some more problems and challenges, such as stack overflow, interrupt overload, real-time analysis, etc.In this paper, we focus on the interrupt mechanism of real-time and embedded sys-tems. We propose modelling languages to analyze the program behaviors in the presence of interrupts. These languages contain time or probability information to analyze the time problems from a quantitative angle. Our research can help the designers and program-mers acknowledge the interrupts, improve the dependability and safety of systems. We also use our research to investigative the performance of the operating system and engine management system based on AUTOSAR OS, and help the programmers complete and improve the implementation.The main contributions of our works include:We present three kinds of modelling languages to describe the interrupt mechanism-s of real-time and embedded systems. These three kinds of languages are the interrupt modelling language (IML), the guard interrupt modelling language (gIML) and the proba-bilistic interrupt modelling language (pIML). gIML is the extend of IML, and pIML is the extend of gIML. All thses langauges contain some ordinary program constructs and some interrupt program constructs, i.e., enable interrupts, disable interrupts and probabilistic interrupt program. With the help of probability information, pIML supports quantitative analysis about program behaviors and time problems in the presence of interruptsWe provide two kinds of semantics for three kinds of languages:operational seman-tics and denotational semantics. The operational semantics specifies how these programs can be executed by a series of steps. We suggest a denotational semantics to describe the meaning of programs in a given environment. Compared with the operational semantics which emphasizes the execution of each step of programs, the denotational semantics is better at analyzing and predicating time problems of programs in the presence of inter-rupts due to the composability of programs predicates. We also define the equivalence of programs based on the operational semantics, and list some algebra laws which have been proved by denotational semantics. At last, we provide an approach to derive denotational semantics from operational semantics. It shows the consistency of these two semantics of our languages.We suggest some utilities of pIML. We implement the operational semantics of pIM-L in Maude, which bridge the gap between theory and practice. It proves the completeness of the operational semantics, and also shows the execution of programs written in pIM-L. We can analyze program behaviors in the presence of interrupts via the denotational semantics of pIML. Moreover, we can calculate the execution time of program and the corresponding probability. We introduce probabilistic distributions to simulate the real interrupts scenes, which help the programmers predict the performance of system. At last, we use pIML to model the operating system and engine management system based on AUTOSAR OS to illustrate the importance of the interrupt mechanism and the utilities of our works. |
PDF Full Text Request