Runtime Verification of Operating Systems Based on Abstract Models

Runtime Verification of Operating Systems Based on Abstract Models

연구 분야: Verification

학회: Programming and Computer Software

Because of high complexity of a modern operating system (OS) one has to use complex models in high-level languages even when specifying some separate aspects of OS functionality, such as, security functions. The problem of verifying the conformity between an OS and these models requires the establishment of a rather complex relationship between elements of OS implementation and elements of the model. In this paper, we present a method to establish and support this relationship, which can be effectively used in OS testing and monitoring. This method was successfully used in testing and monitoring the conformity between Linux kernel components and Event-B models.