Abstract:Performance and cost analysis are the two main purposes of business process modeling, where the Petri net extended with time information is an effective tool for performance analysis, but not for cost analysis. This paper proposes a time Petri net extended with price information—Price Time Petri Net. Firstly, this paper associates a price with a time transition, and gives the semantics for price time Petri net in terms of priced timed transition systems. Then it defines a priced state class as an extension of state class, and discusses the soundness and completeness for this extension. An algorithm is given to prove that the minimum-cost reachability problem for bounded price time Petri net is decidable. Finally, this paper gives an example and draws a conclusion that incorporating price information in time Petri net and applying price time Petri net to business process management are feasible.

Abstract:TCPN (timing constraint Petri nets) is an important kind of time-related Petri nets. Some basic concepts are redefined to enrich and perfect corresponding the theory of TCPN. Firstly, the rigorous definitions for weak and strong schedulability of a transition are redefined to correct the irrationality of the original ones. The verification method for the strong schedulability is presented in the form of a theorem. Secondly, the definition of schedulability of TCPN is given and the corresponding necessary and sufficient condition is proposed. Finally, the characteristic of TCPN along with Petri nets and other time-related Petri nets is analysed. It is of certain illumination and referrence, both in research of time-related Petri nets and in modeling real-time systems.

Abstract:Petri net synthesis can avoid the state exploration problem, which is of exponential complexity, by guaranteeing the correctness in the Petri net while incrementally expanding the net. To solve the resource-sharing problem, Jiao L, et al., investigate the transformation of merging a set of places of an asymmetric choice (AC) net satisfying siphon-trap-property (ST-property), and present the conditions for it to preserve liveness, boundedness and reversibility. The major motivation of this paper is to generalize the results of Jiao’s research and to extend the place-merging problem to subnet-sharing synthesis problem on AC nets or Petri nets beyond AC nets. The conditions of liveness preservation, boundedness preservation and reversibility preservation are presented. The conditions are also presented to show that the synthesis net of AC nets is an AC net. These results are useful for studying the static and dynamic properties of Petri synthesis nets, and for analyzing properties of large complex system.

Abstract:In order to establish a graded reasoning mechanism and provide a possible framework for approximate reasoning in n-valued propositional logic, this paper introduces the concept of α-truth degrees of propositions in n-valued Gdel logical system by using the infinite product of uniformly distributed probability spaces of cardinal n. It is proved that the general inference rules with truth degrees hold, and a sufficient and necessary condition to judge α-tautology is obtained. Moreover, an intrinsic pseudo-metric on the set of propositions is defined by means of the similarity degree between propositions, which makes it possible to develop approximate reasoning in n-valued propositional logic. The graded method proposed in this paper lays a foundation for the algorithmic realization of approximate reasoning and serves as a guideline for the graded reasoning about knowledge.

Abstract:The structure of feedforward inverses is a fundamental problem in the invertibility theory of finite automata. The characterization of the structure of feedforward inverses with delay steps ≥3 is a long-term unsolved problem. This paper deals with this topic. For a binary weakly invertible semi-input memory finite automaton C(M_af ) with delay 3, where the state graph of M_a is cyclic, the characterizations of the structures are given when its minimal 3-output weight is 1, 2, and 8, respectively. Because C(M_af ) is weakly invertible with delay 3 iff it is weakly inverse with delay 3, a partial characterization of the structure of binary feedforward inverses with delay 3 is obtained.

Abstract:Components with redundant functionalities, especially with undesired functionalities, can not be used properly by users. Therefore, the scenario-based behavior derivation of components is a significant problem that needs to be solved, where the scenario specifies the user’s desired behavior. An approach is proposed to derive the desired behavior specified by a scenario specification from components. The main idea of this approach is that by constructing a special environment, i.e., supremum-inclusive environment (SIE), for a component, all behavior specified by a scenario specification can be extracted from the component to the composition of the component and its SIE, and other behavior of the component is discarded to the most extent. This paper uses interface automata to model the behavior of components and a set of action sequences to abstract the scenario specification in Message Sequence Charts (MSCs). The composition of the components is modeled by the product of interface automata. This paper gives the relevant algorithm in this approach and illustrates it by an example.

Abstract:This paper provides an approach to test real-time systems modeled by timed input/output automata (TSIOA), which is a variant of TA (timed automata). This method consists of three steps. Firstly, system model depicted by TSIOA is transformed into an USTGSS (untimed stable label transition graph of symbolic state) which does not contain abstract time delay transitions. Then, the testing methods based on LTS (labeled transition system) are used to the generate transition sequences from USTGSS according to structural coverage criteria. Finally, a process of constructing and executing the test cases is given, in which object functions of time delay variables are imported, and time delay variables used in the transition sequences are solved dynamically by linear programming techniques.

Abstract:Exception handling is a technology that tests and handles exception. Exception propagation induces a control flow other than the main control flow, so it changes the data flows of programs. For data flow analysis of C++ programs to be correct and precise, the flows induced by exception propagation must be properly analyzed. Firstly, based on analyzing the exception handling mechanism and the effects of exception propagation on data flow analysis, the paper proposes a precise and efficient representation for C++ programs with exception handling constructs—control flow graph that contains exception propagation. The control flow graph can represent precisely the implicit control flow for a raised exception and exception propagation path. Then this paper proposes an efficient method to analyze the data flow of the programs that contain exception propagations, and some efficient algorithms are also presented. This method overcomes the limitations of previous incorrect analysis due to failing to account for the effects of exception propagation, and also provides a basis for automatic data flow analysis that contains exception propagation. Finally, it validates the usability of the method by a case study. The method can provide related informations for software engineering tasks such as structure testing, regression testing and program slicing.

Abstract:With the growing number of available Web Services, it is an imperative task to study how to compose Web Services based on the requirements of the customers, which is the main focus of this paper. The proposed method automatically composes Web Services directly according to the customers’ requirements, and then executes the composed services to achieve the customers’ goals. Based on the historic records of Web Services compositions, this method uses a heuristic approach to adjust the composition scheme. Experimental results show that the method is well fits for the volatile environment and yields better performance over other algorithms.

Abstract:To adapt to continually changing businesses, many software systems have to undergo evolutions through plugging new extensions into common base subsystems. Although it can facilitate concurrent development and deployment, this evolution strategy faces the problem of unexpected feature interactions between extensions. So far, formal method is still one of the most effective methods to detect feature interaction problems. The method has been proved to be successful by some small scale experiments. However, it also faces some challenges, e.g., the non-monotonicity of extension, the fast increase of extension combinations and the lack of extension details due to market competitions. Actually, many feature interactions are caused by the inappropriate modifications to the base subsystem and the existing extensions by new extensions. Based on this observation, the paper proposes a new approach for analyzing the causes of feature interactions and for formulating the corresponding constraints such that the conflicts with the same reason can be avoided. The approach has been applied to the analysis of the feature interactions of telecom systems. The experimental results show that most of the conflict-prone behaviors can be discovered quickly. In addition, the approach can help preserve the stability of the original base model and extension models, bypass the problem of extension combinations, and eliminate the requirement to publish the details of all extension models.

Abstract:Replication is an effective way to improve the scalability, fault-tolerance, and availability as well as to reduce the query responding time in P2P system. With the P2P applications transferring from read-only static files sharing to read-write dynamical files interacting, maintaining consistency between frequently-updated files and their replicas is a fundamental reliability requirement for P2P system. This paper presents a trace label based consistency maintenance algorithm. It modifies the message datagram by attaching the address list of peers to which message has been sent. This can help to tell the duplicated message from the source peer by the aid of the attached address list in message datagram. Considering that the address list can become longer with the update time lapsing and the degree of P2P increasing, this paper presents a new Bloom Filter denoting the address list algorithm. The Bloom Filter can succinctly present the address list and simplify the query actions in the list by “OR” operations. The experimental results show that the new trace label based consistency maintenance algorithm can largely reduce the number of the duplicated messages. Moreover, the higher the degree of P2P, the more reduction of the number of duplicated messages and bandwidth utilization. The idea of consistency maintenance in this paper can also be applied to sensor network and other ad hoc networks.

Abstract:More and more network security applications depend on inspecting the content of the packets to detect the malicious attacks. To detect these attacks online, packet inspection demands exceptionally high performance. A lot of research works have been done in this field, and yet there is still significant room for improvement in throughput and scalability. This paper proposes a fast packet inspection algorithm based on state-based Bloom filter engines (SABFE). To achieve high throughput, parallel design is adopted when searching in one Bloom filter engine and between multiple Bloom filter engines. In addition, specific lookup table and prefix register heap are constructed in SABFE to keep the state of the matched prefix for the sake of detecting long patterns. The analysis and the evaluation show that the high throughput of the algorithm can satisfy the wire speed detection requirement when the low resource consumption in hardware resource further improves the scalability of SABFE.

Abstract:Since wireless sensor networks consist of a large number of tiny sensors with limited power supply, it becomes a major concern that how to extend sensor network lifetime and maintain sufficient sensing area at the same time. To achieve this goal, a broadly used strategy is to select some sensor nodes as working nodes to cover the deployment area and at the same time turn off redundant nodes. This paper proposes a mathematical model in which only if the proportion of the sensing range of nodes to the range of the deployment area is known, the number of the nodes needed to reach the expected coverage fraction can be calculated. This work is different from the most literature studying the coverage problem because it is not based on location information of sensor nodes, and thus the cost of hardware and the energy consumption on sensor nodes for deriving and maintaining location information can be considerably reduced. The simulated experiment suggests that in random deployment strategy, the error between the expected coverage fraction and the coverage fraction derived from the simulated experiment is no larger than 2% of the expected coverage fraction; when the expected coverage fraction and the coverage fraction derived from the simulated experiment is the same, the error between the number of working nodes derived from the calculation and the number of working nodes derived from the simulated experiment is less than 5% of the number derived from the calculation. It suggests that the results are identical to the experimental results. The analytical results in this paper can be widely adopted in handling sensor deployment, topology control, and other issues.

Abstract:To assess the security risk of network information systems, this paper proposes a risk propagation model including a risk network and a risk propagation algorithm. A representative example is given to illustrate the application of this model to network risk assessment and validate the correctness of the propagation algorithm. The analysis of the example indicates that the evaluating method using the risk propagation model is superior to the traditional methods in the accuracy of evaluating conclusions and making cost-effective security advices.

Abstract:A new surrogate placement strategy, CCSP (capacity-constrained surrogate placement), is proposed to enhance the performance for content distribution networks (CDNs). CCSP aims to address surrogate placement in a manner that minimizes the communication cost while ensuring at the same time the maximization of system throughput. This work differs from the existing works on the resource allocation problem in communication networks, CCSP considers load distribution and processing capacity constraints on surrogates by modeling the underlying request-routing mechanism, thus guaranteeing a CDN to have minimum network resource consumption, maximum system throughput, and better load balancing among surrogates. An efficient greedy algorithm is developed for a simplified version of the CCSP problem in tree networks. The efficiency of the proposed algorithm is systematically analyzed through the experimental simulations.

Abstract:In decentralized peer-to-peer file-sharing networks, due to the anonymous and self-organization nature of peers, they have to manage the risk involved with the transactions without prior knowledge about each other’s reputation. SWRTrust, a global trust model, is proposed to quantify and to evaluate the trustworthiness of peers, which includes a mathematical description and a distributed implementation. In SWRTrust, each peer is assigned a unique global trust value, computed by aggregating similarity-weighted recommendations of the peers who have interacted with it. Previous global trust models are based on the assumption that the peers with high trust value will give the honest recommendation. This paper argues that this assumption may not hold in all cases. Theoretical analyses and experimental results show that SWRTrust is still robust under more general conditions where malicious peers cooperate in an attempt to deliberately subvert the system, converges more quickly, and decreases the number of inauthentic files downloaded more effectively than the previous models.

Abstract:This paper studies the Verifiable Signature Sharing (VΣS) introduced by Franklin and Reiter, which enables the recipient of a signature to share it among n proxies so that a subset of them can reconstruct it later. By the use of secure distributed key generation based on discrete-log, threshold cryptosystems and verifiable secret sharing scheme, new protocols for RSA VΣS are presented. The protocols are efficient and provable secure and can tolerate the malicious behavior of up to half of the proxies.