Abstract:To relieve the state space explosion problem, and accelerate the speed of model checking, this paper introduces the concept of finite precision timed automata (FPTAs) and proposes a data structure to represent its symbolic states. FPTAs only record the integer values of clock variables together with the order of their most recent resets to reduce the state space. The constraints under which the reachability checking of a timed automaton can be reduced to that of the corresponding FPTA are provided, and then an algorithm for reachability analysis is presented. Finally, the paper presents some preliminary experimental results, and analyzes the advantages and disadvantages of the new data structure.

Abstract:A scheme is obtained by using some kinds of Petri net refinement, according to the design of flexible manufacturing system. Two kinds of refinement are obtained. Dynamic properties have been investigated. The sufficient and necessary conditions of liveness preservation, boundedness preservation and reversibility preservation are presented. A flexible manufacturing system has been designed and verified. These results are useful for studying the static and dynamic properties of Petri nets and analyzing properties of large complex system. The refinement method is especially fit for the design of flexible manufacturing system and practical to use in reality.

Abstract:The relationship of description logic ALNUI and ER model is analyzed, especially how to translate ER model into ALNUI knowledge bases for reducing the reasoning on ER model to model reasoning on ALNUI knowledge bases is investigated, and the problem of fuzzy ER modeling with description logic is further studied. Aiming at the characteristics and requirement of fuzzy ER model and based on the description logic ALNUI, the description logic ALNUI is generalized through fuzzy logic. And a kind of new description logic, i.e., fuzzy description logic FALNUI (fuzzy ALNUI), is presented. The fuzzy ER modeling with description logic FALNUI is studied to translate fuzzy ER model into FALNUI knowledge bases. The reasoning problem of satisfiability, redundancy, and subsumption relation of fuzzy ER model may reason automatically through reasoning mechanism of fuzzy description logic FALNUI, and the correctness of these reasoning problems is proved.

Abstract:J2EE is the primary middleware platform for distributed enterprise applications. Current J2EE (Java 2 platform enterprise edition) transaction scheduling to entity beans is still a simple First-Come First-Served (FCFS) policy. Due to this simple policy, transaction manager is unable to distinguish the key tasks from the trivial ones and the performance of the key tasks is reduced when the server’s load is heavy. Since some characteristics of J2EE middleware, the traditional scheduling algorithms can not be applied to J2EE directly. This paper puts forward a scheduling algorithm named TMPBP (threaded multi-queue priority-based protocol). The algorithm includes a heuristic priority assignment algorithm named HRS, which can recognize the key tasks dynamically. TMPBP improves the Quality of Service (QoS) of the key tasks effectively under heavy load. It is safe and has no starvation or priority inversion. The performance experiments indicate that a considerable improvement on QoS of key tasks has been achieved under the proper parameters of the algorithm.

Abstract:Component-Based development method is thought to be an effective technique to tackle software crisis, but in practice it didn’t reach the expectation, and currently there lack of normal forms and normalized methods to support identification and design of components with high reusability. This paper tries to solve this problem with feature space as a tool. Theory of feature and feature space is firstly introduced, and by analysis of dependencies between features’ variability, the concept of feature dependency (FD) and four types of FDs are elaborated. Then a component specification model based on feature space is presented, in which component reusability is expressed by feature’s ‘type-value’ variation mechanism and feature dependencies. After that, goals of component design and several reusability metrics are briefly discussed, and four component normal forms and the corresponding normalization algorithms based on feature space decomposition are presented in detail. A practical case is finally shown to validate the methods. The normal forms and normalized design methods realize the multi-grained and multi-form components’ co-existence and the loosely composition-based coupling between components, which result in higher reusability, higher reuse efficiency, and lower reuse cost. The methods have been widely applied in the design and implementation of component-based Enterprise Resource Planning (ERP) systems, and have shown great theoretical and practical significance to component design.

Abstract:For real-time software systems, this paper considers the problem of checking component-based designs for timing scenario-based specifications, which is one of the challenges in real-time computing domain. Firstly the timing scenario-based specifications are specified by UML sequence diagrams with a set of boolean expressions, then the interface automata for modeling real time systems through adding time intervals on the actions is extened. The component-based designs are modeled by a real-time interface automaton network which contains a set of real-time interface automata synchronized by shared actions. Based on analyzing the compatible integer state space of a real-time interface automata network, a corresponding reachability graph is constructed and finally an algorithm for checking the consistency between the real-time component-based designs and the timing scenario-based specifications is developed.

Abstract:To improve the practicability and rationality of enterprise process structure optimization, an optimizing method based on directed hypergraph and resource constraint is presented. It models the resource-added process by a directed hypergraph. Based on the directed hypergraph theory and the process meaning added to the hypergraph, the process-structure-optimizing problem is transformed into the directed hypergraph cutting problem, and a set of formal optimizing rules of the process is given too. Then a process whose structure and supporting resource are optimized is obtained. Finally, an example is given to prove the feasibility and effectiveness of this method.

Abstract:Pen-Based user interface software is widely applicable due to its natural and efficient interaction style, whose important characteristics are interaction-centered and individual by user-required. In order to map the intention of users into the designs exactly and efficiently, PUIDM(Pen based User Interfaces software Domain Model) is presented, which is described and analyzed from the aspects of context, component, UI features and architecture, and implemented based on XML. Moreover, a user-centered design process based on the PUIDM is introduced. Experiments show that PUIDM can guide the process of design exactly and efficiently and make the designed software achieve the demand of usability.

Abstract:Mobile communication is playing an increasing role in our lives. Mobile users expect similar kinds of applications to static ones. Multicast not only brings attractive applications, but also has the benefit of saving scarce bandwidth in wireless environment. It would be fruitful to combine these two technologies. This paper proposes a framework to provide multicast in mobile environment called Fast Multicast Handoff Based Hierarchical Mobile Multicast Architecture (FHMM). It uses a hierarchical mobile multicast architecture to isolate the local movement from outside, and improve the stability of the main multicast delivery tree. It introduces a fast multicast handoff mechanism which can reduce handoff latency and packet loss rate for inter-domain handoff and intra-domain handoff. Furthermore, FHMM is a universal solution because it can still work even if the access network does not support multicast. Simulation results show that FHMM is effective with low packet loss rate, high multicast packet delivery efficiency and little multicast maintenance overhead.

Abstract:Trust is multi-faceted and the peer’s needs are different in different situations. A peer may need to consider its trust in a specific domain of another peer’s capability or in a combination of multiple domains. Current Peer-to-Peer trust model could not promise the trust computation of different domains. This paper presents a novel Peer-to-Peer multiple-grain trust model and gives a distributed implementation method, which considers the trust computation of different domains. Mathematical analyses and simulations show that, compared to the current trust model, the proposed model is more precise on trust computation of multiple domains and more robust on trust security problems.

Abstract:A majority of current bandwidth estimation methodologies rely on the principle of the bottleneck spacing effect. Based on the concept of packet dispersion, many packet pair/packet train techniques were presented to estimate capacity/available bandwidth. However, these methods failed for measurement on high capacity path, because they could not measure bandwidth beyond the source node’s maximum sending rate. In addition, current methodologies do not consider the effect of cross traffic routing on available bandwidth estimation. This paper analyzes the effect of the routing of cross traffic packets on available bandwidth measurement in detail. Then based on Monte Carlo Method, a novel methodology fundamentally different in the basic idea from the previous methods is presented to measure end-to-end available bandwidth. This method sends small single packet randomly instead of sending packet pair/train back-to-back. It could work on network whose capacity is far beyond the maximum sending rate of the sender. Analysis and simulations show that besides end-to-end available bandwidth, this method could measure the capacity and idle ratio of targeted link, and then calculate the change of traffic flow on each node and the percentage of different cross traffic on each link.

Abstract:Monitoring infrastructure should be reconfigured at a minimum cost to obtain up-to-date status information as the network evolves. This paper addresses the problem of optimally upgrading the existing monitoring infrastructure. It tries to minimize the total cost of upgrading the monitoring infrastructure, including adding new pollers and reconfiguring the existing pollers. It is shown that this problem is NP-hard. An approximation algorithm is proposed, and its time complexity and approximation ratio are analyzed.

Abstract:The proliferation of the Internet has given opportunities on different entities to share resources or conduct business transactions. However, how to establish trust among strangers without prior relationship and common security domain poses much difficulty for these activities. To resolve these problems, a promising approach known as Automated Trust Negotiation (ATN), which establishes the trust between strangers with iterative disclosure of credentials and access control policies, is proposed. In this paper, a comprehensive survey of research on ATN is presented, and some basic techniques, e.g. negotiation model and architecture, access control policy specification, credential description and credential chain discovery, are introduced and compared. Then based on the analysis of the shortcomings and problems of the techniques, the trend of research and application is discussed. All these work may contribute to the further work on trust establishment for entities with privacy protection and autonomy in open internet.

Abstract:The publish/subscribe system is adapted to the dynamic large-scale distributed computing environment well and will be used widely due to its asynchronous, many-to-many and loosely-coupled communication properties. This paper analyzes the state-of-art of publish/subscribe systems. Many existing systems are classified according to the criteria, such as topology structure, event model and subscription model. Then the key techniques, such as matching algorithm, content-based routing algorithm, formal modeling, quality of service, are explained. Typical pub/sub prototypes and products are compared, and their shortcomings and limitations are discussed. The challenge of enhancing the system intelligence by introducing the event semantic and approximate matching, and the trends of supporting the mobile computing and P2P computing environment is forecasted.

Abstract:Authentication Test is a new type of analysis and design method of security protocols based on Strand space model, and it can be used for most types of the security protocols. However, as a Strand space model, it is inclined to be used for the proof of correctness, and is relatively weaker for incorrectness analysis. This paper proposes the concepts of Enhanced Authentication Test (EAT) and the correspondence function that can solve the problem. Compared with the original concept, the new approach is more formal and can make protocol analysis easier both by hand and automatically.

Abstract:Ownership proofs of digital works allow to justify the copyright claim to the buyers without revealing any secret information and prevent the owner from deceiving without the assumption of the trus ted individual. This paper proposes an ownership proofs scheme for digital works based on proactive verifiable secret sharing and secure multiparty computation. In the proposed scheme, verifiable secret sharing ensures the correctness of ownership secrets and achieves security against cheating participants. Proactive security provides an automatic recovery feature to maintain the integrity and security of secret throughout the lifetime of the scheme. Furthermore,the ownership verification is implemented by using secure multiparty computation and zero-knowledge proofs with homomorphic commitments. Without the assumption of the existence of a trusted individual, the proposed scheme can provide effective computation and discover the dishonesty if not too many individuals collude.

Abstract:Multi-Constrained QoS routing in GMPLS (generalized multiprotocol label switching) network is to find an optimal path satisfying several constraints, such as bandwidth, cost and delay. The problem has been considered as a NP-Complete problem. Based on SRLG heuristic information, the paper provides a MPAS algorithm (Multi-constrained Precomputation Algorithm with SRLG), which includes the precomputation and searching procedures. The precomputation i s able to create and update the routing tables in each node. Then, the searching procedure can select an optimal path satisfying several constraints in the hierarchical architecture. The results of extensive simulation based on the self-similar traffic show that the corresponding methods can achieve satisfactory performance and efficiently solve the problem of multi -constrained QoS routing in GMPLS network.