Research On Formal Modeling And Verification Methods For RTOS Core Attributes

With the development of Io T technology,real-time operating systems(RTOS)play an important role in connecting various devices and systems.Core key functions of RTOS,such as task scheduling,interrupt handling,and synchronous communication,once designed or implemented with errors,can lead to system crashes or unpredictable behavior.Formal modeling and verification of RTOS can reveal errors and vulnerabilities in system design,coding,and implementation,greatly improving system reliability and security.In addition,formal verification can help developers better understand the design and implementation of RTOS systems,enabling them to optimize and improve system performance and efficiency.This article focuses on the formal verification of core properties of RTOS and presents a set of universally applicable and scalable RTOS models using process algebra language Communicating Sequential Processes(CSP).The primary contributions of this article are as follows:(1)The CSP method was used to conduct in-depth formal analysis and modeling of representative RTOS kernel structures.The four modules-memory management module,task management module,interrupt control module,and synchronization and communication module-were abstracted and analyzed from multiple angles,each operation was characterized as a process,and channel communication management was used to establish a complete verification process for core properties of RTOS.(2)Core properties of RTOS were analyzed and researched,and safety property specifications were described using Linear Temporal Logic(LTL).The model checking tool Process Analysis Toolkit(PAT)was used to establish a system behavior model and verify safety property specifications.The verification results showed that the established RTOS universal model satisfies core properties such as deadlock-free,atomicity,consistency,isolation,and persistence.(3)The established RTOS universal model was extended and concretized,and μC/OSII was used as the experimental object for formal modeling and verification.The semaphore mechanism model of the synchronization and communication module was expanded,and in addition to verifying that the μC/OS-II model satisfies the core properties of the universal model mentioned above,its specific priority scheduling property was successfully verified.This experiment demonstrates the scalability and universality of the RTOS universal model proposed in this article,and provides a good technical method for developing safe and reliable RTOS.