In the context of intelligent coal mining faces, the strapdown inertial navigation system (SINS) serves as a pivotal technology for realizing the autonomous positioning of shearers. However, due to the complex underground environment, the positioning precision and stability of SINS have yet to meet the requirements for the normalized operation of intelligent mining faces. This limitation severely impedes the widespread application of SINS in coal mines. To address these challenges and enhance the performance of shearer SINS, this paper proposes a positioning accuracy improvement method based on the SINS and optical fiber sensing system (OFSS). By leveraging the spatial consistency between the shearer trajectory and the shape curve of the scraper conveyor, a SINS/OFSS integrated positioning model tailored to the shearer’s motion characteristics is established. Furthermore, a position mapping mechanism is introduced to achieve spatiotemporal consistency between the real-time position of the shearer and the discrete points on the scraper conveyor’s shape curve. Subsequently, a shearer trajectory time-series prediction model is constructed using historical states to predict future trajectories. This model serves to evaluate and perform a secondary correction on the positioning results, thereby further strengthening the error correction capability. Finally, simulation experiments and platform tests are conducted to validate the effectiveness of the proposed method. The results indicate that under both normal cutting and oblique cutting conditions, the positioning precision and stability of the proposed method significantly outperform comparative methods. The combination of the SINS/OFSS integrated positioning model and the TCN-BiLSTM-Attention (TBA) prediction model effectively mitigates SINS positioning errors, realizing a substantial improvement in shearer positioning accuracy.

The rapid development of the Internet of Things (IoT) spurs strong global demand for related applications and technologies, especially in enhancing system reliability and security. Communication security, mobility, and real-time are the three vital features for constructing secure and reliable IoT systems. Formal methods, based on rigorous mathematical theory, are widely used to describe, analyze, model, and verify software and hardware systems, significantly improving their security and reliability. However, the current research mainly focuses on the practical applications of IoT, and there are still few studies on applying formal methods to IoT systems. As a response, our recent work has proposed the SMrCaIT calculus, which is the only process calculus currently designed for IoT that can comprehensively describe the security, real-time, and mobile features of IoT. Applying the SMrCaIT calculus enables us to model and verify IoT systems before their actual implementation, thereby providing a solid theoretical foundation for building secure and reliable IoT systems. To verify the correctness of the SMrCaIT programs, this article presents a proof system for SMrCaIT calculus, based on the extended Hoare Logic considering time. Additionally, we explore the cooperation test between isolated proofs to further ensure that messages are delivered correctly between IoT entities. The soundness of the proof system is also confirmed. A Vehicle Ad Hoc Network case and a Multi-Unmanned Aerial Vehicle case demonstrate the usability of our proof system in analyzing IoT scenarios.

We introduce HBLLM, a wavelet-enhanced high-fidelity $1$-bit post-training quantization method for Large Language Models (LLMs). By leveraging Haar wavelet transforms to enhance expressive capacity through frequency decomposition, HBLLM significantly improves quantization fidelity while maintaining minimal overhead. This approach features two innovative structure-aware grouping strategies: (1) frequency-aware multi-parameter intra-row grouping and (2) $\ell_2$-norm-based saliency-driven column selection. For non-salient weights, a shared mean is employed across quantization groups within each frequency band to optimize storage efficiency. Experiments conducted on the OPT and LLaMA models demonstrate that HBLLM achieves state-of-the-art performance in $1$-bit quantization, attaining a perplexity of $6.71$ on LLaMA$2$-$13$B with an average weight storage of only $1.08$ bits. Code available at: https://github.com/Yeyke/HBLLM.

The recent interest in peptides incorporating non-canonical amino acids has surged within the scientific community, driven by their enhanced stability and resistance to proteolytic degradation. These so-called non-canonical peptides offer significant potential for modifying biological, pharmacological, and physiochemical characteristics in both native and synthetic contexts. Despite their advantages, there remains a notable gap in the availability of an efficient pre-trained model capable of effectively capturing feature representations from such intricate peptide sequences. This study herein introduces PepLand, a novel pre-training framework designed for the comprehensive representation and analysis of peptides, encompassing both canonical and non-canonical amino acids. PepLand leverages a general-purpose multi-view heterogeneous graph neural network to unveil the subtle structural representations of peptides. Our empirical evaluations demonstrate PepLand's proficiency in a range of peptide property prediction tasks, including cell penetrability, solubility, and protein-peptide binding affinity. These rigorous assessments affirm PepLand's superior capability in discerning critical representations of peptides with both canonical and non-canonical amino acids, and provide a robust foundation for transformative advances in peptide-focused pharmaceutical research. We have made the entire source code and datasets available at http://www.healthinformaticslab.org/supp/resources.php or https://github.com/zhangruochi/PepLand.

Abstract With the rapid popularization of smart devices, the applications and technologies of the Internet of Things (IoT) are in high demand worldwide, especially in improving development efficiency and ensuring system quality, reliability, and security. Formal methods have been successfully used to specify, verify, and analyze software and hardware systems, effectively alleviating the above problems in these systems. However, most of the existing works mainly focus on the practical applications of IoT, and there is a lack of research on modeling and analyzing IoT systems from the perspective of formal methods. In this paper, we first propose a secure mobile real‐time process calculus for specifying and reasoning about IoT systems, called SMrCaIT, which supports not only value‐passing communication but also name‐passing communication. In addition, this calculus can strictly separate process actions and mobility modeling by providing parametric mobility models. Subsequently, we present the operational semantics of this calculus, in particular, the rules on how to secure channel communication by closing the scope of a channel and handling scope extrusion. Taking vehicle ad hoc network (VANET) as a case, the application details of SMrCaIT and its operational semantics are fully demonstrated. By using the rewrite engine Real‐Time Maude, we further implement SMrCaIT and its operational semantics and verify some properties of the VANET case to indicate the effectiveness of our calculus in real‐world scenes.

The Internet of Things (IoT) is an important technology in IT industries.The wide adoption of IoT raises concerns about security and privacy.The Authenticated Publish/Subscribe (AUPS) model is an IoT system which aims to address the security and privacy issues in the IoT environment.AUPS is attracting more and more attention from industries.Hence, the reliability of AUPS is worth investigating.In this paper, we model AUPS using Communicating Sequential Processes (CSP).Five properties (Deadlock Freedom, Data Availability, Data Leakage, Device Faking and User Privacy Leakage) of the model are verified by utilizing the model checker Process Analysis Toolkit (PAT).The verification results demonstrate that AUPS cannot ensure the security of critical data.To solve the problem, we improve the model by using a digital certificate.The verification results of the improved model indicate that our study can enhance the security and reliability of the AUPS model.

Abstract Discriminative correlation filter is one of the quick and effective ways for studying visual tracking. However, discriminative correlation filter‐based methods still suffer from many challenging questions caused by environmental interferences, such as spatial boundary effect, temporal filter degradation, and tracking drift. A novel appearance optimisation model, named spatial and long–short temporal attention model, has been proposed based on a new spatial regularisation term and a long–short temporal regularisation term for learning the correlation filter to localise the target. On the one hand, our proposed method can improve the classical spatial regularisation term with a new weight matrix to alleviate the spatial boundary effect. On the other hand, two new temporal regularisation terms are designed: a short temporal regularisation term and a long temporal regularisation term. The short temporal regularisation term can enlarge the inner connections of the current frame and all foregoing frames to improve the tracking performances, and the long temporal regularisation term can address the influence of occlusion by using the similarity between the initial filter and the current one. Extensive experiments on various benchmarks illustrate that our proposed tracker performs favourably against several related popular trackers.

Abstract As a crucial component of intelligent transportation system, Internet of Vehicles (IoV) plays an important role in the smart and intelligent cities. However, current Internet architectures cannot guarantee efficient data delivery and adequate data security for IoV. Therefore, Named Data Networking (NDN), a leading architecture of Information‐Centric Networking (ICN), is introduced into IoV. Although problems about data distribution can be resolved effectively, the combination of NDN and IoV causes some new security issues. In this paper, we apply Communicating Sequential Processes (CSP) to formalize NDN‐based IoV. We mainly focus on its data access mechanism and model this mechanism in detail. By feeding the formalized model into the model checker Process Analysis Toolkit (PAT), we verify four vital properties, namely, deadlock freedom, data reliability, PIT deletion faking, and CS caching pollution. According to verification results, the model cannot ensure the security of data with the appearance of intruders. To solve these problems, we construct a blockchain‐based mechanism by creating a blockchain‐based distribution trusted platform on top of NDN‐based IoV. Through the analysis of the improved model, the blockchain‐based mechanism can truly guarantee the security of NDN‐based IoV.

As a key technology of the Internet of Things (IoT), middleware plays an important role in managing virtualized resources and services.However, traditional Internet architectures cannot ensure adequate data security and efficient data delivery for IoT middlewares.Therefore, Information-Centric Networking (ICN), a paradigm of the future network, is introduced into IoT middlewares.Since ICN-IoT middleware is attracting more and more attentions, its security is worth discussing.In this paper, we adopt Communicating Sequential Processes (CSP) to model the ICN-IoT middleware architecture.Five properties (deadlock freedom, data availability, action keys leakage, device faking and user faking) of the model are verified by utilizing the model checker Process Analysis Toolkit (PAT).According to the verification results, the model cannot guarantee the security of data.To solve the problems, we encrypt messages with the receiver's public key, and improve the model by introducing a method similar to the digital signature.The new verification results demonstrate that our study can assure the security of the ICN-IoT middleware architecture.

Hybrid systems are composed of physical components with continuous variables and discrete control components. Over time, the interacting laws of discrete and continuous dynamics manage the transition of states in hybrid systems. The operation of hybrid systems needs the combinations of computation and control. However, those combinations add the complexity of the system design and modelling. Therefore, a hybrid relational modelling language (HRML) was proposed to capture the features of hybrid systems.In this paper, we formulate a proof system for HRML to prove the correctness of hybrid systems. In our proof system, the specification and verification are based on Hoare Logic. To express the timing of observable actions, we extend the classical assertion language by adding primitives to it. Both terminating and non-terminating computations can be described in our proof system. In addition, some detailed examples are given to illustrate the application of our proof system.

As a leading architecture of Information-Centric Networking (ICN), Named Data Networking (NDN) plays an important role in the future network construction. NDN retrieves and identifies a data packet according to the packet's name instead of its IP address. Conventional protocols of TCP/IP Internet are unsuitable for NDN. Therefore, Named-data Link State Routing protocol (NLSR) is proposed as an intra-domain routing protocol for NDN. Although NLSR applies a five-layer trust model to guarantee its data security, there are still a lot of security issues in its data access mechanism, such as the fake and leakage of data. In this paper, we apply Communicating Sequential Processes (CSP) to formalize this mechanism. Using Process Analysis Toolkit (PAT), we verify four properties, including deadlock freedom, data availability, data security and data decryption. According to the verification results, the trust model cannot protect the data from fake and leakage once intruders appear. We adopt a method similar to digital signature in the first improved model. However, the process of obtaining keys still needs to be executed multiple times during the verification of a data packet. To further accelerate the key fetching and verification process, all the keys, needed to validate a data packet, are packaged in a special packet of the second improvement.