Since the inception of Bitcoin in 2008, blockchain technology has had a significant impact on many fields. The lack of effective communication between heterogeneous and isolated blockchains, however, restricts the promotion and ecological development of blockchain industry. In this context, crosschain technology has rapidly developed and become a new research hotspot. Due to the decentralized nature of blockchain and the complexity of crosschain scenarios, crosschain technology faces huge security risks. In this paper, we propose formal analysis of the IBC protocol, one of the most popular crosschain communication protocols, aiming to help developers design and implement crosschain technologies more securely. We formalize three main components of the IBC protocol with TLA+, a temporal logic specification language, and verify some important requirements with model checking tool TLC. The verification results are analyzed comprehensively. Issues found through our formal analysis have been reported to the community, most of which have been acknowledged. We also propose some recommendations for removing potential risks.

The relation between automata and temporal logics has been widely studied, and as a consequence, automata theoretical approaches have been successfully applied to the checking of satisfiability of temporal logic formulas and the verification of temporal properties in various settings. Epistemic logics are natural formalisms for reasoning of knowledge in multi-agent systems (MAS) and are often combined with temporal logics for the reasoning of a combination of knowledge and temporal behaviors of MAS. However, the relation between automata and the logics combined with epistemic logic has not been sufficiently explored. In this paper, we explore the relation between them by developing a mechanism for handling epistemic operators. In particular, we present a definition of multi-agent automata, the construction of such automata from formulas of the linear dynamic epistemic logic (LDLK), which is an extension of epistemic logic and has high expressivity, and an approach for solving the satisfiability problem of LDLK. Experimental results on the translation of LDLK formulas to multi-agent automata are reported.

Model checking is considered one of the most practical applications of theoretical computer science in the verification of concurrent systems, and model checking tools are very important for such applications. This paper presents the model checking tool VERDS with the theoretical background, basic functionalities and modeling techniques with various examples. In particular, the tool includes an implementation of a bounded correctness checking approach which can be seen as an extension of bounded model checking and complementary to the traditional symbolic model checking. VERDS is also flexible for extension. We show how it is extended to handle discrete time models. We carry out case-studies of a kind of task scheduling problems, in which time specification is essential. The experimental results show that VERDS is not only feasible for solving practical problems but also with good performance in solving such problems.

Synchronous dataflow graphs (SDFGs) are widely used to model data driven programs, for which throughput is an important real-time requirement. Retiming and unfolding are important graph transformation techniques for performance optimization of SDFGs. Retiming improves the throughput of an SDFG by redistributing its initial tokens, while unfolding by scheduling several iterations of the graph. In this paper, we present an efficient and exact method to find feasible retiming and optimal retiming of an unfolded SDFG on its original SDFG, without converting it to its equivalent homogeneous SDFG (HSDFG) and therefore without further unfolding the HSDFG. The conversion procedures are usually time and space-consuming. We also extend two state-of-the-art retiming methods for SDFGs to deal with unfolding. We implement all the three methods and perform experiments on graphs with various structures and sizes to evaluate them thoroughly. The results show that the proposal method generally outperforms the extensions of existing retiming methods, especially for the large graphs and the graphs with complex structures.

Synchronous dataflow graphs (SDFGs) are widely used to model streaming applications. Unfolding is one of the most important techniques for performance optimization of SDFGs. It may reduce the iteration period (IP) without affecting functionality. We present a novel method to compute the IPs of SDFGs by state-space exploration, without converting them to their equivalent homogeneous SDFGs (HSDFGs), and without further unfolding the HSDFGs. The conversion procedures are time and space-consuming. We also consider the cases when there are resource constraints, which cannot be dealt with by existing methods. Combining with retiming technique, we further present a method to compute the reduced IP of unfolded SDFGs. Our experimental results show that the proposed method outperforms the existing methods significantly.

Streaming applications are an important class of applications in real-time embedded systems, which usually run under restricted resource constraints and with real-time requirement. They are often modeled with Synchronous data flow graphs (SDFGs) or Cyclo-Static data flow graphs (CSDFGs) at the design stage. A proper analysis of the models gives a predictable design for a system. In this paper, we focus on the throughput analysis of (C)SDFGs, taking into account memory constraints. Memory related analysis needs to choose a memory abstraction that decides when the space of consumed data is released and when the required space is claimed. Different memory abstractions may lead to different achievable throughputs. The existing techniques, however, consider only a certain abstraction. If a model is implemented according to other abstractions, the analysis result may not truly evaluate the performance of the system. In this paper, we present a novel unified framework for throughput analysis of memory constrained (C)SDFGs for different abstractions, aiming to provide evaluations matching up to the corresponding implementations. Our methods are exact. Experiments are carried out on several models of real streaming applications and hundreds of synthetic graphs to evaluate the effects and performance of our methods.

Streaming applications usually run on heterogeneous multiprocessor platforms and are required to have a high throughput, which in turn may increase the energy consumption. A trade-off between these two criteria is important for a system. Synchronous data flow graphs (SDFGs) are widely used to model streaming applications. In this paper, we propose a paralleled Pareto optimal scheduling method (PPOS) for SDFGs on heterogeneous multiprocessors. It deals with both time arrangement and processor allocation of computations. PPOS is an exact method to chart the Pareto space of energy consumption and throughput, and to find all Pareto optimal schedules of a system model. An approximation technique is presented to further increase the scalability of our methods. Our experiments are carried out on a practical multimedia application with different configurations and hundreds of synthesis graphs. The results show that the proposed methods are capable of dealing with large-scale models.

Synchronous dataflow graphs (SDFGs) are widely used to represent digital signal processing algorithms and streaming media applications. This paper presents several methods for binding and scheduling SDFGs on a multiprocessor platform. Exploring the state space generated by a self-timed execution (STE) of an SDFG, we present an exact method for static rate-optimal scheduling of SDFGs via implicit retiming and unfolding. By modeling a constraint as an extra enabling condition for the STE, we get a constrained STE which implies a schedule under the constraint. We present a general framework for scheduling SDFGs under constraints on the number of processors, buffer sizes, auto-concurrency, or combinations of them. Exploring the state space generated by the constrained STE, we can check whether a retiming, which leads to a rate-optimal schedule under the processor (or memory) constraint, exists. Combining this with a binary search strategy, we present heuristic methods to find a proper retiming and a static scheduling that schedules the retimed SDFG with optimal rate and with as few processors (or as little storage space) as possible. None of the methods explicitly converts an SDFG to its equivalent homogenous SDFG, the size of which may be tremendously larger than the original SDFG. We perform experiments on several models of real applications and hundreds of synthetic SDFGs. The results show that the exact method outperforms existing methods significantly; our heuristics reduce the resources used and are computationally efficient.

Synchronous dataflow graphs (SDFGs) are widely used to model digital signal processing (DSP) and streaming media applications. In this paper, we use retiming to optimize SDFGs to achieve a high throughput with low storage requirement. Using a memory constraint as an additional enabling condition, we define a memory constrained self-timed execution of an SDFG. Exploring the state-space generated by the execution, we can check whether a retiming exists that leads to a rate-optimal schedule under the memory constraint. Combining this with a binary search strategy, we present a heuristic method to find a proper retiming and a static scheduling which schedules the retimed SDFG with optimal rate (i.e., maximal throughput) and with as little storage space as possible. Our experiments are carried out on hundreds of synthetic SDFGs and several models of real applications. Differential synthetic graph results and real application results show that, in 79% of the tested models, our method leads to a retimed SDFG whose rate-optimal schedule requires less storage space than the proven minimal storage requirement of the original graph, and in 20% of the cases, the returned storage requirements equal the minimal ones. The average improvement is about 7.3%. The results also show that our method is computationally efficient.

This paper presents an exact method and a heuristic method for static rate-optimal multiprocessor scheduling of real-time multi rate DSP algorithms represented by synchronous data flow graphs (SDFGs). Through exploring the state-space generated by a self-timed execution (STE) of an SDFG, a static rate-optimal schedule via explicit retiming and implicit unfolding can be found by our exact method. By constraining the number of concurrent firings of actors of an STE, the number of processors used in a schedule can be limited. Using this, we present a heuristic method for processor-constrained rate-optimal scheduling of SDFGs. Both methods do not explicitly convert an SDFG to its equivalent homogenous SDFG. Our experimental results show that the exact method gives a significant improvement compared to the existing methods, our heuristic method further reduces the number of processors used.

Multirate digital signal processing (DSP) algorithms are often modeled with synchronous dataflow graphs (SDFGs). A lower iteration period implies a faster execution of a DSP algorithm. Retiming is a simple but efficient graph transformation technique for performance optimization, which can decrease the iteration period without affecting functionality. In this paper, we deal with two problems: feasible retiming-retiming a SDFG to meet a given iteration period constraint, and optimal retiming-retiming a SDFG to achieve the smallest iteration period. We present a novel algorithm for feasible retiming and based on that one, a new algorithm for optimal retiming, and prove their correctness. Both methods work directly on SDFGs, without explicitly converting them to their equivalent homogeneous SDFGs. Experimental results show that our methods give a significant improvement compared to the earlier methods.

Multi-rate digital signal processing(DSP) algorithms are usually modeled by synchronous dataflow graphs(SDFGs). Performing with high enough throughput is a key real-time requirement of a DSP algorithm. Therefore how to decrease the iteration period of an SDFG to meet the real-time requirement of the system under consideration is a very important problem. Retiming is a prominent graph transformation technique for performance optimizing. In this paper, by proving some useful properties about the relationship between an SDFG and its equivalent homogeneous SDFG(HSDFG), we present an efficient retiming algorithm, which needn't convert the SDFG to HSDFG, for finding a feasible retiming to reduce the iteration period of an SDFG as required.