Open AccessRuntime Verification of Operating Systems Based on Abstract Models
Author(s) -
Denis Efremov,
Viktoria Vladimirovna Kopach,
Е. В. Корныхин,
Victor V. Kuliamin,
Alexander K. Petrenko,
А. В. Хорошилов,
Ilya Shchepetkov
Publication year - 2021
Publication title -
trudy instituta sistemnogo programmirovaniâ ran/trudy instituta sistemnogo programmirovaniâ
Language(s) - English
Resource type - Journals
eISSN - 2220-6426
pISSN - 2079-8156
DOI - 10.15514/ispras-2021-33(6)-2
Subject(s) - computer science , runtime verification , relation (database) , programming language , embedded system , operating system , formal verification , database
High complexity of a modern operating system (OS) requires to use complex models and high-level specification languages to describe even separated aspects of OS functionality, e.g., security functions. Use of such models in conformance verification of modeled OS needs to establish rather complex relation between elements of OS implementation and elements of the model. In this paper we present a method to establish and support such a relation, which can be effectively used in testing and runtime verification/monitoring of OS. The method described was used successfully in testing and monitoring of Linux OS core components on conformance to Event-B models.