Formal Verification And Design Development Of Embedded Operating System Kernel Services

With the rapid development of science and technology,the Internet of Things tech-nology has been applied to all aspects of our work and life.People pay more and more attention to the security and stability of Io T devices.The embedded operating system's importance as the most basic software for embedded devices of the Internet of Things is beyond doubt.Kernel service is the most basic functional service provided by the operat-ing system.Only when the security and correctness of the kernel service are guaranteed can the operating system run stably.Designing efficient and safe kernel services is the key to building an excellent embedded operating system.As an important core service of the operating system,the programming model deter-mines the system's scheduling operation strategy and application development flexibility.How to ensure the correctness of the embedded operating system's programming model is a very important task.Formal methods can effectively verify operating system kernel services,and the Event-B method has gradually been recognized as an effective formal method for verifying complex systems.The Event-B method adopts a top-down develop-ment strategy.The initial requirements are rewritten to obtain the rewrite requirements.Then the refinement strategy is designed according to the rewrite requirements,and then the model construction work is carried out according to the refinement strategy.Using model refinement methods,a deeper model realizes more specific requirements,and fi-nally,an implementation model that meets all requirements is obtained.Memory allocation is one of the most basic and important kernel services provided by embedded operating systems.Memory allocation is divided into static memory alloca-tion and dynamic memory allocation.The dynamic memory allocation service has a great influence on the performance of the embedded operating system.If the additional memory allocation consumes too much,the embedded operating system cannot provide stable ser-vices when there are multiple requests.If memory allocation's execution efficiency is not high enough,the embedded operating system cannot respond to requests within a limited time.If these problems occur on important occasions such as transportation and medical treatment,they will have serious consequences.In the increasingly complex Io T environ-ment,it is imperative to use efficient and low-consumption dynamic memory allocation algorithms.The research work and contributions of this article mainly include:· Propose and verify Event-Bus hybrid programming model Proposed a mixed programming model of Event-Bus.The Event-Bus combines the multithreading model with the publish-subscribe model,and realizes two programming models:multithreading and event-driven.The advantage of the Event-Bus is that the pro-gramming mode of the system program can be flexibly configured to adapt to dif-ferent situations.This article uses the Event-B method to formally model and verify the Event-Bus,and completes the proof of its safety and activity in each layer of the model.Through clear model description and meticulous refinement strategy design,the automatic verification rate of this work reached 91%.· Design and develop DLSF dynamic memory allocation algorithm A dynamic memory allocation algorithm for adaptively organizing memory management re-sources: DLSF is proposed.In addition to the constant-time and complex operating efficiency,the DLSF algorithm can also readjust the system configuration accord-ing to the actual workload and the operating conditions of the application.The DLSF algorithm can make full use of memory resources in different embedded sys-tem environments,improving the resource utilization of memory allocation and the success rate of memory allocation in the case of resource scarcity.