FINITE-STATE MACHINE-BASED METHOD AND DEVICE FOR OPERATING SYSTEM REQUIREMENT LAYER FORMAL MODELING

摘要

A finite-state machine-based method and device for operating system requirement layer formal modeling, related to the field of embedded operating systems. The method: in response to a request to model an operating system requirement layer, from an operating system functional module database, acquiring multiple functional modules corresponding to an operating system, at least two sub-states corresponding to the functional modules, and at least one operation causing changes in the sub-states of the functional modules, where the operating system functional module database stores correlations between operating systems, functional modules, functional module sub-states, and operations causing changes in the sub-states (101); determining a system state of the operating system on the basis of the sub-states of the functional modules, and determining, on the basis of the operation causing changes in the sub-states corresponding to the modules, a trigger event causing a change in the system state (102); and establishing a finite-state machine-based operating system requirement layer formal model on the basis of the system state determined and of the trigger event causing the change in the system state (103). The method allows the accurate description of a working process of the operating system, thus laying the foundation for a formal verification in the next step, allowing the early discovery of the presence of any potential error, and facilitating the completion of the formal verification of the entire operating system.