Abstract:The pigeon-hole formula PH_nⁿ⁺¹, defined from the pigeon hole principles, is one of the hardest examples on resolution. The research of the formula’s constructions and properties is helpful for constructing other hard examples. It is shown that PH_nⁿ⁺¹ is a minimal unsatisfiable formula. The two normal forms of maximal satisfiable truth assignments for PH_nⁿ⁺¹ are presented by the minimal unsatisfiability of PH_nⁿ⁺¹, which one of normal forms is used in Haken’s proof of hardness for PH_nⁿ⁺¹. The formula PH_nⁿ⁺¹ has well isomorphics properties on substructures. For the modified DPLL algorithm introduced by the isomorphism rule, the complexity of refutation proof of PH_nⁿ⁺¹ can be reduced to O(n³).

Abstract:This paper presents a sentence generation algorithm, which takes as input a context-free grammar and produces a set of sentences that achieves branch coverage for the grammar. The algorithm incorporates length control, redundancy elimination, and sentence-set size control strategies into a sentence generation process such that the generated sentences are short and simple, and the sentence set is small with no redundancy. The paper also investigates the application of this algorithm to test data generation for grammar-based systems. Experimental results show that the generated test data not only has high fault detection ability, but can also help testers improve the testing speed.

Abstract:Software architecture is represented by different views that are derived from architectural concerns. However, when different design methods are applied to generate different views, implicit conflicts might happen between views, due to neglecting the concern conflicts behind each view. To solve this problem, this study uses the software architecture documentation as a common communication platform and derives the implicit conflicts between different views through a procedure of four activities. In this approach, a guideline is suggested to model the relationship between the concerns and views and a set of mathematical representation that is defined for precisely presenting the relations in order to support the automation of the approach.

Abstract:This paper addresses the service selection issue via a service agent framework coupled with a computational model based on trust ontology. The trust ontology proposed from the socio-cognitive view can offer a more insightful understanding in the trust relationships among service agents. A set of trust computational rules have been given to support the trust analysis and reasoning. Also the structure of the service agents has been given. Finally, a case study is used to illustrate how the service agents infer the trustworthiness of their partners by using the set of trust reasoning and computational rules.

Abstract:Debugging, performance tuning, and trustworthy evolution are big challenges for the ultra large distributed software system. Aiming at these challenges, a monitoring enabled distributed software construction method is proposed, by which a user can understand the software system better. Based on publish/subscribe model, a runtime architecture is given, which separates the business logic and monitoring logic. Based on AOP, monitoring enabled software construction tools are designed which can reduce the production cost of the monitoring software and enhance the maintainability of the code. Based on the runtime framework, a dynamic customizable deployment method on monitoring system is proposed. Monitoring enabled distributed software construction method can reduce the tanglement of function logic and non-function logic at system development, which reduces the cost of code maintenance; It can ensure loose coupling between monitoring system and monitored object at deployment; Besides, It collects runtime information from multi-part of the system and gather them together on demand, which makes programmer and system operator able to understand system behavior as comprehensively as possible, and affect the business running as little as possible.

Abstract:To ensure the reliability of UML2.0 sequence diagrams (SD), which are used in software analysis and design, propositional projection temporal logic (PPTL) model checking is adopted in this paper. First, event deterministic finite automata (ETDFA) are proposed and used to describe the formal models of SD. Furthermore, an algorithm for model checking ETDFA with PPTL formulas being the properties is presented. Finally, based on the implementation of PPTL model checker, the ETDFA models of SD are verified. Experimental results show that the proposed method is useful in ensuring the reliability of SD.

Abstract:Traditional approaches tangle the error handling concerns with the primary functional code, which inevitably increase the degree of coupling and decreases the understandability and the maintainability of programs. This paper presents an empirical study of a real-world Satellite Orbit Forecasting system by refactoring error handling policies as methods of classes and aspects, respectively. A set of experiments are constructed to evaluate the original version with the two refactored versions. Based on the results of experiments from the refactoring process, it can be concluded that the modularity and maintainability of the program have been improved without a noticeable compromise in performance by encapsulating computational error handling polices as aspects.

Abstract:This paper presents a group of strategies based on transaction mechanism for the coordination of the multi-services’ dynamic updating in a service-oriented distributed system. These strategies included a selection strategy for choosing of security updating time-point and a 2PC (two-phase-commit) strategy for controlling the multi-services’ updating. With the analysis of time, needed by related updating operation steps, this paper suggests that the basic updating operations (including creation of service instances, orderly execution of multiple service instances’ runtime state-convertion, redirection of service-request-message and activation of new services) should be controlled in a short updating transaction, and multiple persistent data conversions should be controlled orderly under a long transferring transaction (every persistent data conversion should be controlled in a short transaction). The goal is that with the help of transaction mechanism, the world will expect to ensure system state’s ACID properties before and after updating it as efficiently as possible. Furthermore, to make of the most of the correct updating of system, this paper researches about automatically producing and updating transaction, data conversion transaction, and serializing among application transactions and conversion transactions. In the last section, this paper gives a prototype validation of the strategies based on Apache CXF-DOSGi.

Abstract:The aim to improve deficiency of current research on components retrieval is based on behavior specification matching, a multi-level component behavior matching model based on finite automata, which is presented in this paper. The study uses finite automata to model the behavior of components, refers to the idea of graph matching in graph theory, proposes six kinds of behavior matching relationships: equivalence behavior matching, extended behavior matching, compatible behavior matching, contain behavior matching, weak contain behavior matching and weak compatible behavior matching, analysis the implication relationships among these behavior matching relationships, and gives corresponding decision algorithms and adaptation methods of each behavior matching relationship. Based on these algorithms, a universal decision algorithm is proposed to reduce the complexity of subsequent component adapter and assembly. The matching model proposed in this paper provides a favorable technical support for components retrieval, based on behavior specification matching.

Abstract:During the derivation of the business process execution language (BPEL) from graph-oriented process modeling languages, there exist structures called overlapped patterns, which mix sequential and parallel structures together. The existing duplication approach lacks systematical analysis and formal presentations. In view of this problem, a transformation of UML activity diagrams to BPEL based on WF-nets is proposed. By choosing free choice WF-nets as the foundation of activity diagrams and by utilizing the synthesis rules of live and bounded free choice systems, two types of overlapped patterns are defined. For one type of patter, the duplication method is formally represented, and the transformation equivalence is proved using the concurrent regular expressions of Petri nets. For the other type, the applicable range of the duplication method is described. This method presents a solution in formal representations to the transformation of overlapped patterns in BPEL modeling, and distinguishes the derivation of the block-oriented modeling languages from graph-oriented ones.

Abstract:This paper proposes a process algebra called PPPA (priced probabilistic process algebra) by extending an existing process algebra with QoS modeling capability. This paper presents its syntax and semantics to prove that it can model not only functionality, but also non-functionality, such as reliability, performance, and cost. Finally, this paper moves to model and analyze both functionality and QoS of Web services composition in a united way based on PPPA. The paper illustrates the effectiveness with an example to prove that PPPA can support formal modeling and analyzation of QoS of web services composition.

Abstract:On the basis of traditional FSA (finite state automaton), system objects can be resolved from the parameters of system call, and a Software Behavior model based on system object (SBO) is presented. This model defines the software state as all states of system objects, which are owned by the software, and then each state in the model has been assigned semantic information. Therefore, SBO can solve a problem of irrelevant semantics between different traces using the semantic information, and it can detect data semantic attacks, which directly or indirectly modifies system call parameters. Finally, a software anomaly intrusion detection prototype system based on SBO (SBOIDS) is implemented. The experimental and analysis results show that SBO can effectively detect data semantic attack and control the flow-based and mimicry attacks.

Abstract:In order to solve the security threats that dependent tasks scheduling problems face under the heterogeneous grid environment, this paper takes into account the inherent safety and behavior of security of the grid resource node and the reliability of measurement functions in the grid resource node. In addition, the behavior in credibility assessment strategies are also constructed. In order to establish the subordinate relationship between the security requirements of the task nodes and resources security attributes, security benefits of the membership functions are defined. Hence, a grid task scheduling model for security integration is established. On this basis, the requirement representation model and the grid resource topology model are defined; thus, the models of doubleobjective optimization of grid task scheduling are proposed. In order to solve this model, the definition of depth values and the sort of coupling is introduced when dealing with the constraints between tasks. A particle evolution equation is re-defined and re-designed to consider the specific characteristics of the grid task scheduling problem. At the same time, a selection strategy is defined, based on the uniformly distributed vector and concentration of particles. Thus, this paper presents a multi-objective optimization of grid task scheduling particle algorithm, and the algorithm is proved to be viable by applying the relevant knowledge of a probability theory. Simulation results show that compared with similar algorithms, under the same conditions, this algorithm has a faster convergence speed and a better performance in double-objective optimization.

Abstract:In contrast to traditional model-based component software reliability analysis approaches, rate-based simulation approaches can flexibly trace the dynamic failure procedure of software. Consequently, they have been tentatively applied to analyze the reliability procedure of component software in recent years. However, existing simulation approaches are based on excessively simple assumptions in terms of the fault correction procedure in component software testing and are not able to describe the practical reliability procedure of the software system. Therefore, a simulation approach is proposed. It models the fault correction procedure with a hybrid queueing model, in which it takes the fault repair policy and the limitations of debugging resources into account. On this basis, a simulation procedure is developed to realize the simulation of component software reliability procedure. Finally, the evaluation experiment shows the potential of the simulation approach.

Abstract:In this paper, a Two-Phase Clustering (TPC) for the data sets with complex distribution is proposed. TPC contains two phases. First, the data set is partitioned into some sub-clusters with spherical distribution, and each clustering center represents all the members of its corresponding cluster. Then, by utilizing the outstanding clustering performance of the Manifold Evolutionary Clustering (MEC) for acomplex distributed data, the clustering centers obtained in the first phase are clustered. Finally, based on these two clustering results, the final results are obtained. This algorithm is based on an improved K-means, and the MEC. Manifold distance is introduced in evolutionary clustering to make the algorithm competent for the clustering of complex data sets. At the same time, the novel method reduces the computational cost brought by manifold distance. Experimental results on seven artificial data sets and seven UCI data sets with different structure show that the novel algorithm has the ability to identify clusters with simple or complex, convex, or non-convex distribution efficiently, compared with the genetic algorithm-based clustering, the K-means algorithm, and the manifold evolutionary clustering. Furthermore, TPC outperforms MEC obviously in terms of computational time.

Abstract:This paper proposes a ranking model that trains different hyperplanes for different queries and optimizes hyperplanes with the order relations. It aims at solving the problem of most existing rank methods that do not consider the significant differences between queries and only resort to a single function that is time consuming. Next, a weighted voting method is proposed to aggregate the ranking lists of the hyperplanes as the final rank. The weights reflect the degree of precision. Effectiveness is tested by the benchmark data set LETOR OHSUMED and is compare with other ranking models. The proposed method shows improved ranking performance with a significant reduction of training time.

Abstract:In this article, a Resource Control Model for QoS (RCMQ) is presented, based on the former work on Trustworthy and Controllable Network Architecture (TCNA). The QoS mechanisms are distributed into four logical planes in RCMQ: QoS decision plane, QoS discovery plane, QoS data plane, and QoS interface plane. Deployment of RCMQ includes independent and centralized resource control within an Autonomous System and consensus distributed control among ASes. RCMQ is scalable because it decouples all network level QoS control mechanisms from the data plane, and it is robust because RCMQ is a simple and effective close loop control structure. Finally RCMQ in SSFNet environment are implemented, and experimental results show that RCMQ can provide a more stable QoS transmission and maintain fewer flow states than InterServ, which from the other point of view proves that TCNA is more controllable.

Abstract:An adaptive session-granularity admission control (SGAC) method, which combines the session and request granularities, is proposed for flash crowd control. In SGAC, the average response delay is used to measure, detect, and control the flash crowd. Once a session is allowed to access the server, it will be served until it ends. Besides preventing a server from overloading, SGAC can protect the sessions’ integrity. By regulating the session served number adaptively, SGAC can improve the server’s utilization. The performance of SGAC with real HTTP log are evaluated, and the result show that SGAC can effectively prevent servers from overloading, protect sessions’ integrity, improve server’s utilization, reduce the request arrival rate, reduce the access router’s computing overhead, and protect valuable transaction sessions.

Abstract:The current weak state routing schemes cannot facilitate in-network queries effectively. When a query is given for an item at an arbitrary node, disturbance in unrelated routing entries are likely stronger than the useful information in the right routing entries. Consequently, the majority of queries are moved towards wrong nodes. To solve this problem, this paper presents DWalker, an efficient weak state routing scheme-based design based on decaying bloom filters. DWalker uses a bloom filter to represent the summary information of resources at each node and then propagated a bloom filter within a propagation range. The amount of information in each bloom filter decreases exponentially with the distance from the source. DWalker makes the max propagation range less than the expected distance between any two nodes; hence, effectively tackling the problem of multi-path propagation of a decaying bloom filter. DWalker replaces a single bloom filter with multiple bloom filters as a routing entry and holds more routing information. DWalker can ensure that any query can be forwarded in the right direction with high a probability that is based on the proportion of bits set to 1 in a bloom filter and the least number of bits set to 1 in an entry bloom filter for a query. The analysis and simulation of results show that DWalker can make many queries that can be forwarded in the right direction to achieve a high query hit rate with low cost and low delay.

Abstract:Through constructing and utilizing non-malleable, extractable, and weak simulation-sound trapdoor commitment schemes and corresponding smooth projective hash function familes, this paper proposes an efficient two-party password authenticated key exchange (PAKE) protocol within the universal composable (UC) framework, which is the optimal two-round PAKE protocol in this setting. Rigorous security proofs based on standard assumptions in the presence of static corruption adversary are then given out. Comparisons with previously proposed protocols show that, this protocol avoids the use of zero-knowledge protocols, and achieves a higher performance in terms of communication efficiency while attaining a comparable computational complexity.

Abstract:This paper considers the application of network coding to reduce the number of retransmission by combining the lost packets from different receivers with network coding in a wireless broadcast network. In particular, the study propses an algebraic expression to define the coding conditions of retransmission packets by matrix and vector operations. According to the graph constructed by correlation matrix, an algorithm is presented to find more coding opportunity based on maximum matches in graph theory. The proposed algorithm has the ability to find the maximum pairwise coding opportunities, meanwhile, it takes into account the probability of coding the lost packets as possible to more than one retransmission packet to minimize the number of retransmissions by coding optimization, and increase the network bandwidth efficiency and throughput.

Abstract:A pairing-free certificateless two party key agreement scheme (CL-KA) is proposed. This work is able demonstrates all existing CL-KA schemes (except for Lippold’s scheme) are insecure in the eCK model. The scheme is secure in the eCK model as long as each party has at least one uncompromised secret. The scheme has proven to be secure in the random oracle model (ROM), assuming that the computational Diffie-Hellman assumption hold even if the key generation centre (KGC) learns the ephemeral secrets of both parties, or reveal secret values/replace public keys, but not both. The scheme eliminates pairing computation. It achieves efficiency in computational cost when compared with all the other known certificateless key agreement schemes. The scheme is more suitable for the restricted bandwidth of the communication environment, such as ad hoc networks, wireless sensors, and so on.