Abstract Boolean satisfiability (SAT) solving is a fundamental problem in computer science. Finding efficient algorithms for SAT solving has broad implications in many areas of computer science and beyond. Quantum SAT solvers have been proposed in the literature based on Grover’s algorithm. Although existing quantum SAT solvers can consider all possible inputs at once, they evaluate each clause in the formula one by one sequentially, making the time complexityO(m), linear to the number of clausesm,per Grover iteration. In this work, we develop aparallelquantum SAT solver, which reduces the time complexity in each iteration to constant timeO(1) by utilising extra entangled qubits. To further improve the scalability of our solution in case of extremely large problems, we develop a distributed version of the proposed parallel SAT solver based on quantum teleportation such that the total qubits required are shared and distributed among a set of quantum computers (nodes), and the quantum SAT solving is accomplished collaboratively by all the nodes. We prove the correctness of our approaches and evaluate them in simulations and real quantum computers.

With the explosive growth of mobile data traffic, roadside-unit (RSU) caching is considered an effective way to offload download traffic in vehicular ad hoc networks (VANETs). Many existing works investigate the content placement of RSU caching. However, few of them consider the download deadline constraint when caching the content in the RSUs. In this paper, the main objective is to maximize the hit rate of downloading the requested content from the RSUs before the deadline expires. We propose a Markov-based mobility model and a Markov clustering-based content placement algorithm to group the RSUs into clusters and allocate the content to the cache of the RSUs in the cluster. We also investigate the impact on the cache hit rate under different simulation parameters, such as the total number of RSUs, the cache size, and the number of RSUs visited by vehicles during the download period. According to the simulations conducted, when the region of interest (RoI) is small, the MVP method increases the cache hit rate by at least 21.40% compared to the existing methods. When the RoI is large, our approach outperforms other existing methods by at least 26.16% and at most 337.77%, which significantly increases the efficiency of the download session in VANET.

Satisfiability modulo theories (SMTs), an extension of Boolean satisfiability (SAT) problem, is widely used in many application domains because of its rich expressiveness. Thus, there are many works trying to speedup the process of SAT/SMT solving. In this work, we develop a framework by proposing a new hardware architecture to solve the SMT problem for the theory of quantifier free linear real arithmetic (QF-LRA) to speedup the SMT solving process. The new proposed architecture framework consists of a hardware SAT solver and a hardware Simplex solver. Our hardware SAT solver has an optimized Boolean constraint propagation process with a pipeline structure and a nonchronological backtracking mechanism, while our hardware Simplex solver supports parallel operation flow inside the Simplex iteration to execute the selection operations parallelly with the pivot operation and the row selection mechanism to avoid unnecessary row computation and increase the resource utilization. According to our experimental results, the proposed framework can achieve from 2.539 up to 1561.181 times speedup compared with software SMT solvers in our selected 40 benchmarks.

In model checking a system design against a set of properties, coverage estimation is frequently used to measure the amount of system behavior being checked by the properties. A popular coverage estimation method is to mutate the system model and check if the mutation can be detected by the given properties. For each mutation and each property, a full model check is required by some state-of-the-art coverage estimation methods. With such repeated model checking, mutation-based coverage estimation becomes significantly time-consuming. To alleviate this problem, a partial model checking (PMC) technique is proposed to recheck only those system states that were affected by a mutation, thus unnecessary rechecking of a large portion of the system states is avoided and time is saved. The PMC method has been integrated into the State Graph Manipulators model checker. Applying the proposed method to several examples showed that PMC has a saving of 50% to 70% in the coverage estimation time, and a reduction of 90% in mode visits.

To accurately detect deadlocks in Network-on-Chip (NoC) as early as possible, a novel deadlock detection mechanism called Backward-probing Deadlock Detection (BDD) is proposed in this work, which can detect and resolve all existing deadlocks. It was realized using probe systems that generate probes for deadlock detection. A probe system includes a probe System Manager (SM) for turning on probe system, a probe Generator (GEN) for generating probes, a Link Selection (LS) connected to a Switch Allocation (SA), which is used for copying the generated probes, transmitting probes backward, and discarding probes when the probes find that the traversal path is just a congestion not a deadlock or when probe congestion occurs. There is also a TB Calculation (TBC) in LS for TB settings. Finally, a probe comparator (PB Comparator) is used for claiming deadlocks. Note that each port except the local one in a router has its own probe system.

Network-on-Chip (NoC) is becoming a promising communication architecture in place of dedicated interconnections and shared buses for embedded systems. Nevertheless, it has also created new design issue such as communication congestion and power consumption. A major factor leading to communication congestion is mapping of application tasks to NoC. Latency, throughput, and overall execution time are all affected by task mapping. As a solution, an efficient run-time Congestion-Aware Scheduling (CWS) is proposed for NoC-based reconfigurable systems, which predicts traffic pattern based on the link utilization. The proposed algorithm alleviates the overall congestion, instead of only improving the current packet blocking situation. Our experiment results have demonstrated that compared to other existing congestion-aware algorithm, the proposed CWS algorithm can reduce the average communication latency by 66%, increase the average throughput by 32%, reduce the energy consumption by 23%, and decrease the overall execution by 32%.

With rapid developments in science and technology, we now see the ubiquitous use of different types of safety-critical systems in our daily lives such as in avionics, consumer electronics, and medical systems. In such systems, unintentional design faults might result in injury or even death to human beings. To avoid such mishaps, we need to verify safety-critical systems thoroughly and formal verification techniques such as model checking are a very promising approach. However, modeling the systems formally is a challenging task, which is further aggravated by the necessity to model faults and automatic repairs in safety-critical systems. Currently, there is no automatic technique in formal verification that can aid system designers in formally modeling the faults and repairs. This work contributes by proposing an extension to the Safecharts model so that faults and repairs are easily modeled and then the Safecharts are transformed into semantically equivalent Extended Timed Automata models that can be directly model checked. In this way, automatic failure analysis techniques are integrated into the SGM model checker. Application examples show the feasibility and benefits of the proposed model-driven verification of safety-critical systems.

With rapid developments in science and technology, we now see the ubiquitous use of different types of safety-critical systems in our daily lives such as in avionics, consumer electronics, and medical systems. In such systems, unintentional design faults might result in injury or even death to human beings. To make sure that safety-critical systems are really safe, there is a need to verify them formally. However, the verification of such systems is getting more and more difficult because designs are becoming very complex. To cope with high design complexity, currently, model-driven architecture design is becoming a well-accepted trend. However, existing methods of testing and standards conformance are restricted to implementation code, so they do not fit very well with model-based approaches. To bridge this gap, we propose a model-based formal verification technique for safety-critical systems. In this work, the model-checking paradigm is applied to the Safecharts model, which was used for modeling but not yet used for verification. Our contributions listed are as follows: first, the safety constraints in Safecharts are mapped to semantic equivalents in timed automata for verification. Second, the theory for safety constraint verification is proven and implemented in a compositional model checker (that is, the state-graph manipulator (SGM)). Third, prioritized and urgent transitions are implemented in SGM to model the risk semantics in Safecharts. Finally, it is shown that the priority-based approach to mutual exclusion of resource usage in the original Safecharts is unsafe and corresponding solutions are proposed. Application examples show the feasibility and benefits of the proposed model-driven verification of safety-critical systems