Barrier certificate generation is an efficient and powerful technique for formally verifying safety properties of cyber-physical systems. Feed-forward neural networks (FNNs) are commonly used to synthesize barrier certificates, but the fixed activation functions limit their efficiency and scalability. In this paper, we propose a novel method for generating barrier certificates using Fourier Kolmogorov-Arnold Networks (KANs). Specifically, it utilizes Fourier KANs to replace FNNs as the template of barrier certificates. Since Fourier KAN has learnable activation functions and uses trigonometric functions as its basis functions, it can efficiently improve the representation power and is easy to train for neural barrier certificates. Then, it formally verifies the validity of the candidate Fourier KAN barrier certificates using both the Lipschitz method and the Satisfiability Modulo Theories, improving the efficiency and success rate of verification. We implement the tool KAN4BC, and evaluate its performance over a set of benchmarks. The experimental results demonstrate the effectiveness and efficiency of our method.

Information leakage easily occurs in large-scale information interactions and brings harm to individuals, enterprises, and society. As a well-known security policy, Chinese Wall (CW) provides a security guideline, which combines mandatory and discretionary access control to avoid information leakage. Colored Petri nets (CPNs) are a widely used formal method, well suited for verification of CW policy due to the capability of characterizing the concurrency. However, CPN easily suffers from the problem of state space explosion due to the interleaving semantics. The unfolding techniques can effectively alleviate this problem. In this article, we apply simplified CPN and their unfolding techniques to detect information leakage against CW policy. Specifically, we define a CPN-based CW model, propose an algorithm to generate the merged process of CPN, and detect the potential information leakage by analyzing the structural behaviors of its unfoldings. Furthermore, we conduct a case study and several experiments to show the advantages of our method. The results exhibit that our method can effectively detect information leakage against CW policy and alleviate the state space explosion.

The Petri-net-based information flow analysis offers an effective approach for detecting information leakage by the concept of non-interference. Although the related studies propose efficient solutions, they lack quantitative evaluation on information leakage. In this paper, we propose a novel method for quantitative evaluation of information security based on stochastic labeled Petri nets (SLPNs) and information flow analysis. Specifically, we introduce four different levels of security metrics, and provide a methodology for evaluating the information security. Furthermore, a case study is presented to show the feasibility of our method.

Synchronous Dataflow graphs (SDFGs) are widely used to model streaming applications that exhibit data-driven and iterative execution patterns. Graph conversion techniques such as retiming, unfolding, and pipelining are commonly used to optimize the iteration periods (IPs) of SDFGs. In this paper, we propose an extension of the graph conversion based pipelining approach for single-rate SDFGs to multi-rate SDFGs. A new perspective on pipelining is introduced, where the pipelining of a general-time SDFG can be viewed as the retiming of a unit-time SDFG. Based on this perspective, we prove that optimal pipelining can always achieve an IP less than 1 time unit longer than the optimal IP for an SDFG. Furthermore, an efficient optimal SDFG pipelining algorithm called GCP-SDFG is presented. Experimental results show that GCP-SDFG has significant advantages in IP minimizing and runtime relative to three state-of-the-art retiming or pipelining algorithms.

At present, the advancement of science and technology has contributed to the emergence of various network parallel environments, web service concurrency environments and massively parallel processors. In order to abstract some practical systems into concurrent system models, it is necessary to conduct model analysis, and to perform deadlock detection of the concurrent system. Despite prior studies on the control problem of the synchronous concurrent system, there remains room for improvement in terms of workload, time, and efficiency. Some very practical methods are explored by introducing locking and unlocking to synchronize the concurrent system, and the algorithm that involves the specific regulation is provided. The Petri net model of the controller is developed to provide an effective method applicable to find the deadlock and to prevent and eliminate the deadlock for synchronous concurrent systems.

Missing-data errors easily occur in cyber-physical systems (CPSs). Although many business process modeling notation (BPMN)-based methods are proposed to model CPSs and detect errors, it is hard to automatically verify their correctness, especially in the data flows, due to their lack of formal specifications. By comparison, Petri nets, as a formal method, are widely used to detect data-flow errors. However, these methods easily suffer from the state-space explosion problem. This is mainly because their reachability graphs or state transition graphs are based on the interleaving semantics. As an unfolding technique of Petri net, a merged process can characterize concurrency relations and alleviate this problem. Thus, we utilize the merged process of Petri net with data (PD-net) to check the missing-data errors of the CPS. We first transform a BPMN of the CPS into a PD-net and generate its merged process. Meanwhile, we analyze its structural behaviors and data-adjacent events. Furthermore, we propose an algorithm for checking missing-data errors. In addition, a case study and some experiments are done to show the practicality and effectiveness of our method.

How to guarantee the consistency between different systems has become a bone of contention in model-driven software development. Behavioral relations are a prominent technique/method to analyze the consistency degree of two workflow systems. There are four kinds of behavioral relations, i.e., strict order relation, exclusiveness relation, interleaving order relation, and inverse order relation. An activity in a module may be in different behavioral relations with activities in another module. We call the latter module aspecial modulein this article. However, the existing measuring methods for behavioral consistency do not consider special modules at all. Thus, if we conduct a consistency analysis of different systems by these methods, we may get an inaccurate consistency degree, or obtain no results. In order to solve this problem, we use workflow nets (WF-nets) to model workflow systems and re-explore their behavioral relations. Then, their behavioral relation matrices (BRMs) are constructed. Based on BRMs, some new measurement methods are proposed to calculate the behavioral consistency degree of two WF-net systems. Finally, a group of experiments is done to show the effectiveness of our methods.

With the development of smart devices and mobile communication technologies, e‐commerce has spread over all aspects of life. Abnormal transaction detection is important in e‐commerce since abnormal transactions can result in large losses. Additionally, integrating data flow and control flow is important in the research of process modeling and data analysis since it plays an important role in the correctness and security of business processes. This paper proposes a novel method of detecting abnormal transactions via an integration model of data and control flows. Our model, called Extended Data Petri net (DPNE), integrates the data interaction and behavior of the whole process from the user logging into the e‐commerce platform to the end of the payment, which also covers the mobile transaction process. We analyse the structure of the model, design the anomaly detection algorithm of relevant data, and illustrate the rationality and effectiveness of the whole system model. Through a case study, it is proved that each part of the system can respond well, and the system can judge each activity of every mobile transaction. Finally, the anomaly detection results are obtained by some comprehensive analysis.

The correctness of workflow systems is dependent on not only their control-flows but also their data-flows.WFD-nets(Workflow net with data) can model both control-flow and data-flow of workflow systems, and are used to analyze/verify their correctness. The existing methods of analyzing/verifying WFD-nets are based on their reachability graphs. However, the reachability-graph-based methods have two flaws: state space explosion and pseudo states, since the guard functions are not handled perfectly. Note that every transition of a WFD-net is labeled by a guard function, which is a Boolean expressionw.r.t.data and can determine the progress of control-flow. In order to solve these problems, we propose aguard-driven reachability graphthat can both alleviate the state space explosion problem and avoid pseudo states. We describe the related algorithms and develop a tool. A group of experiments illustrate the advantage and effectiveness of our approach, and an example of property loan shows its usefulness.

Petri nets are used to detect the errors of data inconsistency in concurrent systems. The detection methods usually apply a breadth-first or depth-first search to the reachability graphs of Petri nets. However, they spend too much space and time due to the blind search strategy. In this paper, we propose a heuristic method that can save lots of space and time. First we define structural data inconsistency of Petri nets which is more likely to cause the errors of data inconsistency. Then, in order to detect the errors as fast as possible, a heuristic function is proposed to guide the construction of a reachability graph. Furthermore, we propose a detection algorithm and develop a tool. Our experiments illustrate the advantage and effectiveness of our method.

The errors of data inconsistency occur in a concurrent system when some concurrent operations are conducted improperly. The model-checking technique is widely used to detect them based on the state transition graph. However, the state space explosion problem is the biggest obstacle for this technique, since the state transition graph is based on the interleaving semantics that can result in a rapid increase of the graph scale. In addition, data inconsistency is closely related with concurrent operations, but the state transition graph hardly characterizes concurrency due to its interleaving semantics. The unfolding technique of Petri nets can both alleviate the state explosion and characterize concurrency because it is based on the concurrent semantics. In this paper, we define Petri net with data to model concurrent systems with three kinds of data operations: read , write, and delete, and then formalize data inconsistency. We propose an unfolding method to produce a finite complete prefix (FCP) for each PD-net. Then, a matrix that represents all concurrency relations of transitions is constructed in view of FCP. Furthermore, the error of data inconsistency can be detected via this matrix. The related algorithms and the developed tool are introduced, and experiments illustrate their effectiveness and advantages. An example of industrial information system shows the usefulness of our study.

The general Petri nets are not suitable to model the data operations of concurrent read and coverable write. Therefore, Petri net with data operations (PN-DO) is defined, which extends contextual nets with write arcs and some other components. Its execution semantics are defined, and a new method is proposed to construct its reachability graph that is of a smaller scale than traditional reachability graph. Based on this kind of reachability graph, we propose a method to check the errors of inconsistent data and missing data. Meanwhile, case studies are given to illustrate the effectiveness of our methods.