The formal verification of the operating systems in power monitoring system is an important means to ensure the security of the operating system in power monitoring system. This paper introduces the verification principles and framework of formal verification of operating systems in power monitoring system, the languages and tools used in formal verification, and some classic projects of formal verification of operating systems. Through the introduction of the related content of the formalization of these operating systems, some ideas and future development trends of the formal verification of the current operating systems are explained. It has completed the verification process, beginning with weak type safety and progressing to functional correctness, proof of the high-level abstract protocol, and modification of the low-level code. These gain from the constant advancement and refinement of tools and technologies for formal verification of operating systems, but it is also subject to formal verification tools and techniques, and cannot genuinely go towards the last practical link of production. The automated research on formal verification tools and technologies will continue to be a significant advance in operating system formal verification.
Vehicle spare parts demand forecasting is crucial for optimizing inventory and improving maintenance efficiency. This study aims to explore a vehicle spare parts demand forecasting method based on the fusion of XGBoost and LightGBM models to enhance prediction accuracy and precision. In this paper, we first collected a large amount of historical spare parts demand data and associated feature data, followed by data preprocessing and feature engineering. Then, we constructed individual machine learning models as well as the XGBoost-LightGBM fusion model, and performed parameter tuning and optimization using the Optuna framework. Experimental results demonstrate that both XGBoost and LightGBM models achieve favorable performance in spare parts demand forecasting, but the fusion of these two models further enhances prediction accuracy. The fusion model exhibits lower MAPE values compared to individual models on the test set, confirming its superiority and effectiveness. This method leverages the strengths of both models and improves prediction accuracy through weight fusion, offering practical significance in achieving accurate spare parts demand forecasting, optimizing inventory, and improving maintenance efficiency. Future research can explore alternative machine learning algorithms and feature engineering methods to further enhance the accuracy and reliability of vehicle spare parts forecasting.
Lane detection has been one of the most important functions in the autonomous driving perception module. Most of the current research require complex post-processing and curve fitting processes before they can be used by subsequent regulation modules. In this paper, we propose the LLFormer algorithm combining CNN and Transformer structure, which is the first attempt to perform end-to-end lane detection based on laser point cloud and output its cubic polynomial coefficients. In addition, this paper modifies the structure of the conventional transformer and proposes the Generating Lane Query (GLQ) module. The output of encoder is plugged into GLQ for initialization of lane query in decoder, preserving the uniqueness of each frame of point cloud data. We test the performance of the proposed algorithm in the public dataset K-Lane, and the results show that the accuracy of the proposed LLFormer is close to the existing SOTA algorithm. The number of model parameters of LLFormer is only 9.01M, and the amount of operations is only 0.19GFLOPs, which are 1/26 and 1/2937 of the existing SOTA algorithm, respectively. The frequency of inference calculation is 35.9FPS, which can fully meet the real-time requirements for industrial deployment.
The line loss rate varies significantly among different substation areas due to diverse influencing factors. Consequently, a study is conducted to investigate the line loss index of a substation area by employing a cooperative game approach that considers multiple influencing factors. Firstly, utilizing the available fundamental data of the substation area, construct a substation area factor suitable for the calculation of "one substation area, one index". Subsequently, an initial low-voltage substation area line loss prediction model was constructed using Bi-LSTM. Finally, the weights of each influencing factor are calculated using a cooperative game strategy, and the attention mechanism is applied to Bi-LSTM. After the model is trained and optimized, the predicted value for the line loss index for each substation area is output. Experiments indicate that the algorithm can effectively enhances the accuracy of predicting the line loss index value in the substation area, and assist in customized and refined management of loss reduction in the low-voltage distribution substation area.
The multi-area economic dispatch (MAED) is a hot and vital research topic for energy saving and emission reduction. Multi-areal economic dispatch refers to the most economical distribution of load requirement among the output units under the premise of satisfying the physical and operational constraints of multiple areas. Each area is connected by a transmission line. In this paper, an improved algorithm (SA-TLBO), which uses adaptive teaching factor to replace the teaching factor in the original teaching-learning based optimization, is developed. Since, adaptive teaching factor can achieve a good balance between convergence speed and search ability, thus improving the overall performance of the algorithm. The method is tested on a system with ten areas, and each area has a 130-unit system. Compared with other two improved strategies and conventional algorithms, the proposed SA-TLBO is shown to yield better solutions for multi-area economic dispatch problems.
