Tactical Data Link (TDL) has been widely used to enhance communication and coordination among different parties in various scenarios. Recently, there has been growing interest in leveraging blockchain technology to address the challenges faced by traditional TDL systems, particularly in terms of trust, information sharing, and data consistency. In this paper, we employ process algebra Communicating Sequential Processes (CSP) to model and verify a blockchain-based TDL communication mechanism. Our approach captures the core features of the system, with a focus on the consensus achievement mechanism among TDL nodes and systemic issues arising when the system reaches its fault tolerance threshold. We analyze and verify key properties such as deadlock-freedom and liveness to ensure system reliability, as well as linearizability and data consistency to evaluate system security guarantees. Our results demonstrate that while the system maintains functional correctness within the fault tolerance threshold, its vulnerabilities beyond this limit require further investigation and enhancement.

IC3 and its variants are SAT-based model-checking methods that play a critical role in hardware verification. Efficient management of proof obligations, which track states that need to be proven unreachable, is essential for improving verification performance. This paper presents a novel approach that utilizes Critical Proof Obligations (CPOs) to improve proof obligation management. We propose two techniques, CPO-Driven UNSAT Core Generation and CPO-Driven Proof Obligation Propagation, to promote lemma propagation and frame refinement. Experimental results on HWMCC benchmarks demonstrate significant improvements in CPO discovery and lemma propagation, resulting in notable performance gains.

This paper proposes a term-level generalized symbolic trajectory evaluation (GSTE) to tackle parameterized hardware verification. We develop a theorem-proving technique for parameterized GSTE verification. In our technique, a constraint is associated with a node in GSTE graphs to specify reachable states. Generalized inductive relations between nodes of GSTE graphs are formulated; instantaneous implications are formalized on the edges of GSTE graphs. Based on this formalization, parameterized GSTE are verified. We moreover formalize our techniques in Isabelle. Furthermore, once a parametrized design is verified at the term level, we can convert the generally parameterized invariants into concrete ones, which can be used to verify a synthesized netlist of an instance of the parameterized design at the Boolean level. We demonstrate the effectiveness of our techniques in case studies. Interestingly, subtleties between different implementations of FIFOs are discovered by our parameterized verification, although these circuits have been extensively studied previously.

The interaction and fusion of cross-domain features and feature semantics are crucial for obtaining cross-domain generalized feature representations in Network Intrusion Detection (NID) tasks. Existing interaction methods typically treat features within a single domain as independent entities, utilizing various feature engineering techniques for intra-domain feature selection, interaction, and fusion. Although these methods perform well in domain-specific NID tasks, their cross-domain generalization capabilities remain limited. To address these challenges, this paper proposes a novel Cross-Domain Semantic Fusion (CDSF) framework, which integrates cross-domain feature semantic matching, multi-task mapping, and multi-granularity feature fusion into a unified process. This framework ensures effective transformation and fusion of discrete and continuous features across domains. Comprehensive experiments on multiple benchmark NID datasets demonstrate that the proposed method achieves competitive performance in terms of both accuracy and cross-domain generalization.

Parameterized systems play a crucial role in the computer field, and their security is of great significance. Formal verification of parameterized protocols is especially challenging due to its "parameterized" feature, which brings complexity and undecidability. Existing automated parameterized verification methods have limitations, such as facing difficulties in automatically deriving parameterized invariants constrained by mixed Forall and Exists quantifiers, or having challenges in completing the parameterized verification of large and complex protocols. This paper proposes a formal verification framework for parameterized systems based on induction, named wiseParaverifier. It starts from small concretizations of protocols, analyzes inductive counterexamples, and constructs counterexample formulas to guide the entire process of parameterized verification. It also presents a heuristic Generalize method to quickly find auxiliary invariants, a method for promoting complex mixed quantifiers and merging parameterized invariants, and uses symmetric reduction ideas to accelerate the verification process. Experimental results show that wiseParaverifier can successfully complete automatic inductive verification on 7 cache coherence protocols and 10 distributed protocols. It has strong verification capabilities and migration capabilities, and can provide concise and readable verification results, which is helpful for learners to understand protocol behaviors.

Parameterized verification is a challenging problem that is known to be undecidable in the general case. ‍is a widely-used method for parameterized verification, originally proposed by Chou, Mannava and Park in 2004. It involves abstracting the protocol to a small fixed number of nodes, and strengthening by auxiliary invariants to refine the abstraction. In most of the existing applications of CMP, the abstraction and strengthening procedures are carried out manually, which can be tedious and error-prone. Existing theoretical justification of the ‍method is also done at a high level, without detailed descriptions of abstraction and strengthening rules. In this paper, we present a formally verified theory of ‍in Isabelle/HOL, with detailed, syntax-directed procedure for abstraction and strengthening that is proven correct. The formalization also includes correctness of symmetry reduction and assume-guarantee reasoning. We also describe a tool AutoCMP for automatically carrying out abstraction and strengthening in , as well as generating Isabelle proof scripts showing their correctness. We applied the tool to a number of parameterized protocols, and discovered some inaccuracies in previous manual applications of ‍to the FLASH cache coherence protocol.

In distributed systems, modelling and implementing effective coherence protocols is indispensable for resolving issues related to inconsistency. This presents formidable challenges in both modeling and implementing these protocols correctly. This paper introduces Murphi2Chisel, a compiler that establishes connections between the modelling level to implementation level, as well as between event-driven and clock-driven models. The scope of this paper unfolds in two key stages. In the initial phase, a compiler is developed to transform the Murphi-specified coherence protocol into Chisel circuits automatically. Subsequently, we implement a multi-verifying engine for verification of the protocol implementation in Chisel. As a byproduct, we compare the application of various methods involved in both explicit State model checking and symbolic model checking on coherence protocols.

Verification of parameterized protocols is of great interest in the area of formal verification, mainly due to the practical importance of such systems. Explicit-state model checking is an essential approach in which states for a system are maintained in explicit form, as are all state transitions. In order to reduce the search space to a minimum, we propose a local search strategy. In detail, first, heuristic functions are designed to guide the searching of bugs more effectively, which exploits information extracted from invariants and rulesets, to improve the calculation of a distance between two states. Second, candidate solutions with poor scores are dropped for further compression of the state space explored. Especially, we apply successfully our local search algorithm to the reachable analysis of a real-world implementation of TileLink protocol.

Security protocols are essential to ensure privacy, integrity, and authentication. However, to guarantee the security objectives of a protocol, formal tools are necessary. Currently, existing formal tools employ specific input languages to model protocols. Typically, protocols are presented in strand space specification format in textbooks, which depict the messages shared among trusted communication participants during a correct protocol operation. Strand space specifications prioritize conciseness and readability over formal preciseness, and their formal semantics are only considered and clarified in specific contexts. Therefore, a gap exists between strand space specifications and the modelling languages of formal tools. To address this issue, we propose a verified security scheme with the operational semantics of strand space. We successfully tested our framework on several typical protocol benchmarks using the model checker Murphi and identified potential attacks on them. In summary, our framework offers an innovative and comprehensible scheme for model checking security protocols.

With the development of edge computing, a large number of tasks can be offloaded to the edge server for computing, among which the dispatching and scheduling of dependent tasks has attracted extensive attention.The offloading of dependent tasks mainly has the following problems: how to select an appropriate edge server for dispatching, how to arrange the scheduling order of edge servers to better schedule tasks, and how to solve the task dependency problem.In this paper, we proposal a dispatching and scheduling method DAMD, based on reinforcement learning and multi-agent reinforcement learning, to solve the above three problems.Specifically, as the first step of DAMD, a reinforcement learning approach is designed to estimate the network load and dynamically dispatch tasks to the appropriate edge servers.Each edge server is regarded as an agent by a multi-agent reinforcement learning method, the second step of DAMD, which comprehensively considers the dependency relationship between tasks and the scheduling relationship between servers to achieve the efficiency and fairness of task scheduling.Finally, the results show that our method can better complete the task within the deadline and greatly reduce the average response time according to the time sensitivity requirement.

Pronoun anaphora ambiguity is very common in natural language descriptions, especially in specilized fileds such as computing, medicine and aerospace.When multiple antecedents appear before a pronoun word, readers with different background knowledge often have completely different understandings on a same word.In order to reduce such misunderstandings caused by ambiguity in the process of document propogation, we usually use manual methods to check the ambiguity of reference, which however cannot meet the increasing needs of detection with the development of various disciplines.In this paper, we propose a method to intelligently detect sentences with anaphora ambiguity.First of all, we identify criteria for ambiguous sentences and then use word embeddings to further detect ambiguity.Specifically, we propose a pronoun substitution strategy based on coreference resolution, and combine this strategy with word embedding techniques to generate a cross-domain anaphora ambiguity detection method.Finally, we carry out experiments on aerospace documents, which verify the effectiveness of our proposed method in anaphora ambiguity detection.

Modern digital hardware is becoming ever more complex. And agile development, an efficient idea in software development, has been introduced into hardware. Furthermore, as a new hardware construction language, Chisel helps to raise the level of hardware design abstraction with the support of object-oriented and functional programming. Chisel plays a crucial role in future hardware design and open-source hardware development. However, the formal verification for Chisel is still limited. In this paper, we propose ChiselFV, a formal verification framework that has supported detailed formal hardware property descriptions and integrated mature formal hardware verification flows based on SymbiYosys. It builds on top of Chisel and uses Scala to drive the verification process. Thus the framework can be seen as an extension of Chisel. ChiselFV makes it easy to verify hardware designs formally when implementing them in Chisel.

The Responsibility-Sensitive Safety (RSS) model is a state-of-the-art parametrizable approach to facilitating safety planning and control, which has been widely used in autonomous driving systems. However, the current RSS model neither considers perceptual risks, nor can adaptively adjust its parameter settings according to different scenarios. These limitations may lead to unsafe or inefficient behavior of the autonomous vehicles. Therefore, this paper proposes a novel perceptual risk-aware adaptive RSS approach, which trains the interpretable perceptual risk assessment model to evaluate the risk level of different scenarios and provides interpretable reasons for reference, then adaptively selects the corresponding parameters in the RSS model for safety monitoring according to the obtained perceptual risk level. This new risk-aware adaptive approach significantly reduces safety margins and increases traffic density, while maintaining risk limits. Our experiments illustrate that our approach can well balance the safety and practicality of autonomous driving systems for complex scenarios.

中国半导体产业在过去三十年的黄金发展期取得了巨大的成就,但相较于美国六十年的高速发展,仍有所不足.面对美国不断升级的半导体限制政策,本文提出,为推动我国半导体产业加快发展,应以金砖协作体系为根基,实施"走出去"发展战略,推动半导体产业跨境融合发展;应根据各方的优势,加快闽台在半导体产业及相关领域的全面深入合作与融合发展,从而突破美国的技术封锁.探讨建立包含闽台、粤港澳赣在内的广义海峡硅谷的战略可行性,希冀海峡硅谷能成为超越美国加州硅谷的"东方硅谷".

With the increasing complexity of hardware design requirements and the development of open-source hardware ecosystems, Chisel and RISC-V are becoming increasingly popular. As a domain-specific language of Scala, Chisel is gradually becoming the choice of hardware design development with the help of the features of high-level languages. Especially in the RISC-V open-source instruction set ecosystem, many representative projects are implemented with Chisel. In hardware development, the correctness verification of the design is essential. A promising stream for verifying the correctness of RISC-V designs is RISC-V Formal, which is at the SystemVerilog level. In this paper, we propose RVFC, a framework for formal verification of RISC-V designs at the Chisel level. It is based on the ability of ChiselFV to define formal properties and verify them at the Chisel level. We also reimplemented a textbook RISC-V five-stage pipeline design and found an oversight in the design through RVFC verification.

TileLink is a standard interface used for on-chip communication within the RISC-V open-source processor ecosystem. It offers a scalable, low-latency, and coherent method of exchanging data between various components of a System-on-Chip (SoC) design, such as processors, accelerators, and memory controllers. Certain components within the SoC may include caches, and TileLink Cached(TL-C) coherence protocols are implemented to ensure cache coherence among these components. The TL-C protocols are hierarchical and can be configured to operate in either inclusive or non-inclusive modes. Due to the complexity and difficulty of these protocols, our investigation focuses on utilizing model checking techniques. In this paper, we present a novel approach to construct a simple and flexible cache hierarchy in the model checking tool Murphi. We verified the generic formal models that adhere to the recent TL-C specifications proposed by SiFive with inclusive or non-inclusive policies for the first time. In particular, we have examined the shapes of cache coherence trees and their generation within the aforementioned inclusion policies.

Safety-critical traffic in Industrial Internet of Things (IIoT) requires real-time communications with high fault tolerance, bounded latency and low jitter.Time-Sensitive Software-Defined Network (TSSDN), which combines the deterministic transmission of Time-Sensitive Networking (TSN) with the centralized management of Software-Defined Networking (SDN), was recently proposed to support the real-time requirement in IIoT.The research on TSSDN has been receiving increasing interests, however, the existing work has limitations including 1) the functional safety of TSSDN cannot be guaranteed; and 2) the effect of the separation of data plane and control plane on the time-sensitivity of TSSDN has not been evaluated.Therefore, in this paper, we employ the timed model checker UPPAAL to formalize the TSSDN architecture.Firstly, we use the build-in checker in UPPAAL to verify deadlock-free property, functional safety property and starvation-free property of our model.Then, the total latency of frames forwarding and scheduling within a single switch is measured based on the model.We focus on the latency overhead of frames requesting processing rules from the controller, which is on average an additioanl 180µs latency in the worst case, but the impact of this delay on the time-sensitivity of TSSDN is tolerable.As far as we know, this is the first paper providing a formal verification and analysis approach for TSSDN architecture, which could benefit for both TSSDN designers as well as the researchers.

Multi-ported memories are essential modules to provide parallel access for high-performance parallel computation systems such as VLIW and vector processors, etc. However, the design of multi-ported memories are rather complex and error-prone, which usually causes the high implementation cost. Therefore, the designs and verification of multi-ported memories become challenging. In this paper, we firstly present a modular and parameterized approach based on Chisel to design and implement multi-ported memory concisely. Furthermore, to verify the correctness of the design, we formalize properties of multi-write-read operations of the memories by generalized symbolic trajectory assertion (GSTE) graphs and verified them by two kinds of approaches: SystemVerilog Assertions-based, and GSTE-based approaches. Our verification through SVA and STE/GSTE successfully finds an error caused by misusing one parameter in our high-level design.