Runtime Verification Of Embedded Operating System

Computer software which has been widely used in various kinds of key fields, suchas aerospace, transportation, finance, weapons, and etc. plays a soul role in our daily life.Any failures of software in these areas will cause fatal losses of security, economic andeven life in our country. However, due to the complexity of software itself, failure isinevitable even if various methods and technologies are used in the development phase.Thus, the reliability and safety of computer software especially crucial software are stillthe daunting challenges we are facing with. As an effective supplement of testing andmodel checking, runtime verification inspects whether the software’s actual executiontrace meets a specific demand, and hope to find the execution exceptions in time. Aspeople’s gradual emphasis on software quality in the key areas, this technology is alsoclosely watched.Different from the traditional monitoring approach which mainly focuses on thecorrectness of system states, runtime verification pays more attention about systemexecution’s satisfaction with some complicated properties. Usually, these properties aredescribed by temporal logic, in particular, linear temporal logic (LTL). In the process ofruntime verification, we use the temporal logic properties to generate a monitor whichare used to check whether processes executions fulfill the system’s requirements.However, the current runtime verification technology is mainly used for applicationsoftware. Very few are specialized for monitoring running state of an operating system.For some key areas such as aerospace and weapons, requirements of the embeddedoperating system’s process of scheduling, memory allocation, interrupt handling andinterface operations are extremely strict. Current methods and tools are incapable todeal with the software failure caused by an operating system. To solve this problem, thispaper studies the runtime verification framework and key techniques for embeddedoperating system. And we realize a demo tool combined with an open source embeddedoperating system FreeRTOS. Contents of this paper include:First, this article introduces an embedded operating system oriented framework forruntime verification and feedback adjustment which is based on the forecastingsemantic theory. To avoid the occurrence of failure, this framework monitors the wholesystem through information provided by the supervising interfaces and adjusts thesystem’s scheduling and execution process by the feedback interfaces wheneverpossible faults are found.Second, this article defines the syntaxes and semantics that are applicable todescribe the operating system’s time sequence characteristic. These syntaxes andsemantics which bring in support for atomic events definition and time sequentialoperations are an extension and improvement to exist event definition language PEDL and MEDL.Third, this article presents an automatic approach to generate a monitoring program.In this way, we create a corresponding monitor automaton model from the monitoringproperties first. Then a monitoring program will be generated by the automaton model.Finally, we design and realize the monitoring interfaces, feedback control interfaces and theautomatic tool for a monitoring program creation based on the FreeRTOS. And we also have a teston a case.