Abstract:Automatic diagnostic information generation is one of the remarkable advantages of model checking methods. It is very important to understand the reason for the failure and fix the problem. In this paper, how to generate effective diagnosis in model checking value-passing processes is discussed. Two diagnostic forms, proof graph and witness, are defined. Moreover, algorithms are proposed to construct them from the search states space in model checking process. By this way, useful diagnoses are generated from the existing information by less calculation. Besides above, the algorithms have been implemented and used to analyze several cases. The experimental results show that this method is efficient.

Abstract:The relationships among various quantum automata are clarified, and in particular, variously equivalent characterizations of quantum automata are established. The G-quantum automata, g-quantum automata, (generalized) quantum automata, G-quantum grammars and g-quantum grammars are presented, and their connections to some of the other existing quantum automata are expounded. Under a certain condition, the equivalence between the G(g)-quantum automata and G(g)-quantum grammars is discussed. Therefore the problem of quantum grammars generating quantum regular languages is solved. The relation between quantum and regular languages is dealt with, and particularly, two open problems proposed by Gudder are answered. Finally, the method of decreasing the dimensions of spaces of states on quantum automata is given.

Abstract:Action calculi is introduced as a mathematical framework for expressing different interactive behaviors, which shows the advantages in representing different interactive models with some common features. In this paper, action calculi is used to include γ-calculus (a computational calculus for higher-order concurrent programming) in its setting. First, a concrete action calculus AC(K_γ) is defined. Then the formal compositional translation of the γ-calculus into AC(K_γ) is presented. Finally, upon definitions of the observability, the weak barbed bisimularity as well as the weak barbed congruence for AC(K_γ), it is proved that such translation preserves the weak behavioural equivalence of the γ-calculus with the π-calculus as intermediate. This work not only shows the expressiveness of action calculi, but also provides precondition for uniting and comparing γ-calculus with other concurrent models under the theory of action calculi.

Abstract:In this paper, a fundamental framework of automata and grammars theory based on quantum logic is preliminarily established. First, the introduce quantum grammar, which is called l valued grammars, is introduced. It is particularly showed that the language (called quantum language) generated by any l valued regular grammar is equivalent to that recognized by some automaton with e moves based on quantum logic (called l valued automata), and conversely, any quantum language recognized by l valued automaton is also equivalent to that generated by some l valued grammar. Afterwards, the l valued pumping lemma is built, and then a decision characterization of quantum languages is presented. Finally, the relationship between regular grammars and quantum grammars (l valued regular grammars) is briefly discussed. Summarily, the introduced work lays a foundation for further studies on more complicated quantum automata and quantum grammars such as quantum pushdown automata and Turing machine as well as quantum context-free grammars and context-sensitive grammars.

Abstract:In order to solve massive data sort in digital library and dataware house, a new highly efficient algorithm based on serpentine tape, named STESort (serpentine tape external sort), is provided in this paper. Taking full advantage of the characteristics of serpentine tape, the STESort algorithm reduces the whole seek time on tapes compared with traditional 2-way merge tape sort algorithm. Besides increasing the efficiency of tape sort, the STESort algorithm prolongs the duration of tapes by reducing the times of tape header moving on tape surface. The theoretical analysis and the experimental results show that the STESort algorithm is more efficient than the traditional tape sort algorithms. The STESort is suitable for massive data sort.

Abstract:The TSP (traveling salesman problem) is one of the typical NP-hard problems in combinatorial optimization problem. The fast and effective approximate algorithms are needed to solve the large-scale problem in reasonable computing time. The known approximate algorithm can not give a good enough tour for the larger instance in reasonable time. So an algorithm called multilevel reduction algorithm is proposed, which is based on the analysis of the relation of local optimal tour and global optimal tour of the TSP. The partial tour of the global optimal tour is obtained by a very high probability through simply intersecting the local optimal tours. Using these partial tours it could contract the searching space of the original problem, at the same time it did not cut the searching capability down, this is the so-called reduction theory. And then the scale of the instance could be reduced small enough by multi-reduction. Finally it could solve the small-scaled instance using the known best algorithm and get a good enough tour by putting the partial tours together. The experimental results on TSPLIB (traveling salesman problem library) show that the algorithm could almost get optimal tour every time for instance in reasonable time and thus outperformed the known best ones in the quality of solutions and the running time.

Abstract:The technology of cooperative checkpointing and rollback recovery as an effective method of fault tolerance, has been widely used on the parallel or distributed computer systems, such as cluster of computers. In order to reduce the overhead of time and space, a cooperative checkpointing algorithm based on message counting is given in this paper. While reducing a message complexity during synchronization from O(n²) to O(n), improving system's efficiency and scalability, this algorithm is also fit for those non-FIFO message passing systems.

Abstract:DTD (distributed termination detection) is an important problem in the field of distributed algorithm research. If the termination of a computation can not be detected, the algorithm will lose its realistic significance. The credit-recovery algorithm proposed by Mattern is message optimal, but it is limited to centralized computation. In this paper, this algorithm is improved to be available in decentralized computation, which makes it more applicable to distributed environment.

Abstract:XYZ/E is used to specify and verify the triple-modular redundancy fault-tolerant system. Assuming that each computer is loaded with a determined sequential program P which continuously outputs data to the outer environment, the case P running on single processor is illustrated by an XYZ/E program SingleProcess_P, and the property of program P is specified by a temporal logical formula Spec_P. Finally, it is proved that the program TripleProcessors_P obtained from the triple-modular redundancy way can still satisfy Spec_P in spite of hardware errors.

Abstract:Supporting dynamic changes and flexibility is required when workflow management systems are employed. Related research work are all focused on some special changing issues. A process meta-model is proposed to guide the design of workflow process model. The process meta-model supports dynamic changes of workflow process. Its dynamic characteristics of workflow process from the points of view of time and process levels are surveyed, and the workflow meta model proposed by workflow management coalition is extended. This process meta-model enables the dynamic characteristics to be described in build-time and enables the changes of a process to be handled with these pre-defined characteristics. Based on this meta-model, a workflow management system possesses the flexibility without losing the control of workflow process.

Abstract:An important issue of real-time software development is to analyze and predict the execution time of real-time software. A kind of visual prediction and analysis framework of the execution time of real-time software based on program flowchart is proposed in the paper. The key issues of implementing the framework are discussed in detail, including creating the mapping between intermediate code segment and statement line of source code, retrieving the time of any given program segment from the perspective of CPU cycles of goal machine instruct, calculating CPU cycles of statement lines of source code, point-to-point WCET_C (worst case execution time calculated) analysis algorithm based on program flowchart, and transforming CPU cycle into physical time. Based on the framework, a practical tool has been developed to predicate and analyze visually the program execution time. Finally, conclusion and comparison between the work in this paper and others is given.

Abstract:Nowadays, all access control models take a system-centric view of protecting resources, and they don’t take the context into account when controlling the permissions. However, with the development of databases, networking, and distributed computing, it causes people to shift the focus on security issues from the protection of individual objects and subjects in isolated computer systems, to the protection of dynamically authorization with different task. In this paper, an access control mechanism called TBAC (task-based access control) is introduced, which models from the tasks in workflow and dynamically manage the permissions through tasks and tasks’ status. The TBAC is well suited for distributed computing, information processing activities with multiple points of access, and decision making in workflow and distributed process and transaction management system. The basic concepts of TBAC are introduced and a formalization description and an analysis are given. It is clear that TBAC will be used widely in many fields, such as OA, business, and so on.

Abstract:As the applications of real-time systems are becoming more and more popular, the system scheduling mechanism faces new requirements and challenges because of the coexistence of different kinds of real-time and non-real-time tasks. The open real-time system has been paid attention because of giving a way to solve the problem and also brings new ideas to scheduling theory and approach. Firstly, the basic concepts and theories of open real-time system are described. And then, a hiberarchy model for scheduling objects is presented. It adapts to the scheduling environment of open real-time system. Several related scheduling approaches are compared in detail, and their functional features, the applying scope, and some of their common characters are pointed out. The result come out that it is feasible to integrate different kinds of approaches, and this would be a direction. In the integrated scheduling mechanism, the advantages of each approach can be kept, therefore, the application requirements of open real-time system can be met better.

Abstract:SHI Wen-Chang+;SUN Yu-Fang (Institute of Software;The Chinese Academy of Sciences;Beijing 100080;China) 　Supporting for the security policy flexibility is one of the goals of modern secure operating systems. The DTOS (distributed trusted operating system) program put forth a concept of security policy lattice, which provides a good way for the research on security policy flexibility. However, it is claimed in the DTOS program抯 description of security policy lattice that MLS (multi-level security) policies are static policies. First, an enforcement scheme for a MLS policy is constructed theoretically, which shows that MLS policies are of history sensitivity and hence have dynamic characteristics, and so that MLS policies can not be simply taken as static policies. Then, an implementation algorithm for the constructed enforcement scheme is given. It is illustrated that the constructed enforcement scheme is of the same complexity as the ordinary enforcement scheme and so is an applicable scheme. As a result, it can be affirmed that reasonable, flexible and practically feasible schemes are available to make MLS policies to be of history sensitivity. Consequently, the improperness of the assertion that MLS policies are static policies is exhibited.

Abstract:The research and implementation of JBOO (Jade Bird object-oriented) software modeling tool is discussed in the paper. The Jade Bird object-oriented standard which the software modeling tool JBOO supports is explained briefly, the system structure and functions of JBOO are expatiated, and a method of implementing object-oriented software modeling tools is presented. At last, JBOO is compared with the similar representative tools.

Abstract:In this paper, a UML approach applied in the CBC (constraint-based codesign) of embedded systems, which is presented by Chonlameth Arpnikanondt, is analyzed. Some deficiencies of the method when it is applied in the complicated embedded systems codesign are proposed. According to these deficiencies, the meaning of constraint is extended, and a solution is proposed to improve the efficiency in hardware/software codesign and is explained in detail with the example of mart phone system, which is developed by the Institute of Software, the Chinese Academy of Sciences.

Abstract:Internet measurement and analysis provides a technique platform for improving network management, increasing network availability and avoiding large-scale network attack. So it has become an important issue widely considered by researchers, industries and government. In this paper, the chief research of the network measurement and analysis and its research trend in the world are introduced. And the key techniques and the difficult problems are explored. Three typical application examples are also given.

Abstract:In this paper, the state-of-the-art DWSS (distributed Web server system) technologies are described, including their mechanisms, advantages and disadvantages. Then a new algorithm TB-CCRD (tag based cache cooperative Web requests distribution) for Web requests distribution is presented. Based on it, a scalable high performance DWSS is constructed. In this new architecture of DWSS, the front-end server organizes the caches of each backend Web server into a virtual large cache to improve the hit rate of cache and the response time of the DWSS. The operation of TCP connection handoff is distributed among the backend servers to prevent the front-end from becoming a bottleneck of the system. Tags are used to indicate where the content of a URL is cached, so as to avoid extra communications within the system. Through this mechanism, the TB-CCRD DWSS achieves both higher performance and better scalability.

Abstract:In this paper, the generalized multi-rate multicast weight-based fair rate allocation problem is studied. First, a multi-rate multicast network model is formalized, and the minimum rate requirement and weight of each virtual session is considered in the model. Based on the model, the concept of generalized multi-rate multicast weight-based max-min fairness is defined, and the theory of generalized multi-rate multicast weight-based max-min fair rate allocation is established. At last, a centralized algorithm to solve the generalized multi-rate multicast weight-based fair rate allocation problem is presented, and its correctness is also proved.

Abstract:The MANET (mobile Ad hoc network) is a new mobile wireless communication network. Comparing with the other communication network, the unique properties of MANET add the difficulties and challenges to the network management. Recently, the network management on MANET is on the initial stage and more accurate standards are not defined and in addition, some existing problems such as unidirectional links and relative mobility of nodes are ignored. Hence, a clustering algorithm based on graph with the token mechanism and node minimum identifier applied to hierarchical network management on MANET is proposed, as well as the amelioration to MIB (management information base) suggested. The algorithm puts the special unidirectional links and relative mobility into consideration, improves the flexibility and scalability in network management, and suggests a new idea to the network management as well.

Abstract:For transactions’ mobility and the inherence limitations of wireless network, traditional real-time transaction management mechanisms are incompetent to support the execution of mobile distributed real-time transactions in mobile distributed computing environment. In this paper, the commit mechanism for mobile real-time transactions is studied. First, a nested transaction model based on functional alterative tasks is given by analyzing the characteristics of real-time transactions in mobile distributed environment. Then a three-tier commit structure supporting the suggested model is presented. And a three-phase real-time commit protocol 3PRTC (three-phase real-time commit) is also proposed, which can guarantee the atomicity and structural correctness of the mobile real-time transactions. By performance testing, it is shown that the suggested transaction model and its commit mechanism can improve the successful ratio of real-time transactions.

Abstract:The cheat-proof method in threshold secret sharing scheme is researched. The threshold secret sharing scheme is integrated with RSA and one-way function. And the RSA and one-way function are fully utilized to verify the validity of data. A threshold secret sharing scheme based on RSA is proposed, at which the cheating is equal to attacking RSA scheme. A threshold secret sharing scheme based on RSA and one-way function is also presented, at which the cheating is equal to attacking RSA scheme or one-way function. These two schemes have so strong power to identify cheaters that they can restrict the probability of successful cheating to a very small value no matter how skilled cheaters are, so they are unconditionally secure. In addition, the schemes proposed in this paper have very high information rate.

Abstract:Key management system is an important part of secure multicast, while the number of keys held by each user and the cost of re-keying are crucial factors which closely related to the performance of key management system. The key management system with less number of keys held by each user and less cost of re-keying is efficient. In this paper, the key management problem is investigated based on the user probability model by using the source coding theory. And it is proved that in the key management system using Huffman hierarchy, the average cost of re-keying and the number of keys held by each user are minimal. Meanwhile, the lower bounds of the average cost of re-keying and the number of keys held by each user in theory are provided.