Abstract:Hybrid System is an embedded computing system composed of computers and physical instruments. It allows the inclusion of continuous components in a reactive real-time system. XYZ/E is a temporal logic language based on Manna-Pnueli's Linear Time Temporal Logic. It combines both static and dynamic semantics in a unified framework and supports the whole procedure of stepwise refinement, i.e. from the abstract specifications to executable codes. In this article, the authors first specify and verify hybrid systems with XYZ/E, then introduce the computational model we selected for the hybrid systems and discuss the formal description of hybrid systems in the TLL XYZ/E. Finally the verification methodology in the framework is discussed. Compared with the related work, XYZ/E supports state transitions such that it can specify complex control algorithms in a convenient way.

Abstract:This paper considers the problem of combining the object-oriented and functional programming paradigms. Compared with most of the approaches in this direction, the combination has the following two advantages. First, the authors combine several important concepts as they are well known in widespread mainstream languages. In other words, the authors do not introduce new language concepts but try to interpret well-known language concepts based on the new ones. Second, the combination has the property that individual language concepts do not influence the whole language to the extent as they do traditionally, so that usually one needs to pay for a language concept only when he uses it. Concretely, a core language for functional object-oriented programming together with a straightforward operational semantics is proposed, where the properties mentioned above hold. The core language combines the following key language concepts from the languages Eiffel, Java, ML and Haskell：objects, classes, multiple inheritance, method redefinition, dynamic binding, static type safety, binary methods, algebraic data types, higher-order functions, ML-polymorphism.

Abstract:It is shown that there exists a diamond of high computably enumerable degrees preserving the greatest element 1.

Abstract:In this paper, the typical problems in distributed multimedia database systems, such as real-time requirements, synchronization, QoS specifications, are analyzed. Policies and methods to solve these problems are provided. And various implementation paradigms for distributed systems, such as RPC (remote process call), middleware, Agent, are investigated.

Abstract:The numerical instability in computing the parameters of the points on Nurbs curves/surfaces is a fatal disadvantage of Nurbs methods. In this paper, the authors introduce the moving affine frame (MAF) method for intersection calculation of parametric curves and surfaces. Based on the principle of a MAF method, a new method for computing the parameters of the points on Nurbs curves and surfaces is presented. The numerical stability and the efficiency of the method are better than all traditional iterative methods. The new method has been applied to the commercial 3D CAD system GEMS5.0.

Abstract:In this paper, the authors present an appearance-based approach to dynamic hand gesture recognition. A motion-based segmentation scheme for image motion estimation is proposed using variable-order parameterized models of image motion and robust regression. Based on image motion parameters, two different appearance change models of hand gestures are created. Template-Based classification technique is then employed to perform hand gesture recognition in which reference templates are created with a mini-max type of optimization. A series of experiments on 120 image sequences show that high recognition rate, low computation load, and high stability can be achieved with the proposed methods.

Abstract:The Internet marketplace is getting attention widely as a new computational paradigm which enables applications to obtain and integrate remote services for data supply and for data manipulation on Internet. In this paper, a means of representing services on an Internet marketplace using extensible markup language (XML) is proposed which well balances the interests of the marketplace infrastructure with those of the customers and providers.

Abstract:In this paper, a method is proposed to develop a concurrent program from a VDM－SL (Vienna development method-specification language) specification. On the basis of DD-VDM (data decomposition-Vienna development method), service parallelism, internal parallelism and virtual atomicity can be observed in the development process. Then a nested object-oriented structure is presented to specify these parallelisms. This nested structure can be implemented with several language structures for two different kinds of applications including share-variables parallel system and distributed parallel system.

Abstract:In order to integrate and query irregular and dynamic information on WEB in a database-like fashion, the authors use object exchange model (OEM) to construct information model of WEB in this paper. To express each component of pages as an OEM object, the authors design an algorithm which extracts semi-structured data from HTML pages, and the testing results are given. This method can extract structured and semi-structured data. It has better applicability than other existing methods.

Abstract:Based on the introduction of active network, the MANet (mobile agents based active network) is presented as a secure and efficient active network system constructed on the mobile agents system. It implements integrated active networks by capsule the program code and data into an active package which can run on active node as an agent. Also the performance and flexibility of active network are improved by the on-demand code loading and caching based on the CodeBroker.

Abstract:In order to realize fuzzy rule acquisition automatically, and to construct high performance intelligent system and solve the bottle neck problem in the intelligent system, the method of automatic rule acquisition using genetic algorithms and the combination optimization ability of genetic algorithms have been studied. The simulation results show that this is an effective fuzzy rule acquisition method.

Abstract:In this paper, the existence of the least anti-unification in multi-pattern is proved and an algorithm for the anti-unification is proposed. In addition, the application of the anti-unification in multi-pattern is also introduced.

Abstract:For periodic tasks in a distributed real-timesystem, a number of static allocation algorithms have been developed which solve the problem of assigning and scheduling tasks effectively under some determined conditions. The principal limitation of these approaches is that the attributes of the tasks have to be known. Sometimes the execution time or the number of subtasks of a periodic task might be a stochastic process obeying some rule. In such cases, the performance of the static schemes will decrease greatly. According to the analysis of the processing in specific application fields, the authors model two types of random tasks in distributed real-time systems and introduce the static allocation algorithms (SAA) which have been applied in engineering for the two task models separately. On the basis of SAA, a predicting allocation algorithm (PAA) is presented for the assignment and the scheduling of multitasks in distributed systems. The proposed algorithm, depending on the statistic features of the task execution time or of the number of subtasks included in the tasks, can predict the task parameters reasonably and implement dynamic allocation of the tasks, so that the system can meet the timing requirements more efficiently. The results of the simulation of the two task models have shown that compared with SAA scheme, the performance of PAA is significantly better in task finishing time, load balancing, system response time, ratio of discarded tasks, etc.

Abstract:The stochastic Petri net modeling technique can be used in many different ways. It allows the simple design for complex system models, that typically are very costly to solve due to their state space explosion problem. However, refinement of models can be used to develop compact models, which reveal the independence and interdependent relations of submodels in the original models and can be solved by decomposition technique. In this paper, the author uses a multiserver multiqueue system model as an example to show how the refinement of a stochastic Petri net model can be developed by applying the description of enabling predicates and random switches of transitions. In addition, the routing and selecting schemes for multiserver multiqueue systems are discussed and the stochastic Petri net models for those schemes are provided.

Abstract:An image can be considered as a combination of regions, which have some intrinsic homogeneities in color or texture, etc. The shapes in an image are described by the boundaries of these regions and their spatial relations. To retrieve image by shape, it is a key problem to measure the similarity among shapes and match their spatial relations. Adopting template-matching technique, the authors present a computation method for simple shape similarity. Based on the two-dimensional set string representation of the spatial relation of these simple shapes, a spatial relation match algorithm is also presented. The whole retrieval process is divided in three stages, i.e., the rough stage, the refining stage and the spatial relation matching stage. The experiment shows this method is rapid and accurate.

Abstract:DC/P (duration calculus prover) is a proof assistant for a family of interval logics. It adopts the Gentzen-style sequent calculus as its basic proof system. The techniques such as term rewriting and automatic decision procedure are integrated to automate many trivial proof steps. In this paper, the authors briefly describe the semantic encoding approach, and the sequent calculus, as well as the related implementation techniques of the DC/P.

Abstract:The shortcomings of the existing solutions to the performance bottleneck and reliability problem of Internet servers are analyzed, and a solution based on IP-level load balancing is given in this paper, in which a scalable and highly available virtual Internet server can be built on a cluster of servers. Scalability is achieved by transparently adding or removing a node in the cluster. High availability can be provided by detecting the node or daemon failures and reconfiguring the system appropriately. The architecture, design and implementation of the virtual Internet server are discussed in detail. Brief performance testing results are also provided.

Abstract:Data dependence is the basic guideline and constraint for parallel processing. The structural distinctiveness of VLIW (very long instruction word), i.e., the lockstep property, leads to remarkable uniqueness in its data dependence analysis, as is shown in this paper. Flow dependences with the same iteration distance comprise a linear ordered set, while characteristic flow dependences with different iteration distances may also have inclusion relationship between each other. From such discovery, a novel method is presented to eliminate redundant loop-carried flow dependences for VLIW architectures, so as to facilitate loop scheduling. The method is complete in that it gets rid of all redundancies. The sufficient and necessary preconditions to identify redundancy for single and multiple iteration distances are given, and a linear ordered algorithm is described. The method is generic, and can serve as a foundation for research on VLIW, such as software pipelining and multi-instruction stream scheduling.

Abstract:The local structure of CMAC (cerebella model articulation controller) neural networks results in faster learning of nonlinear functions. However, the learning accuracy of CMAC is too low to meet the requirements of application in many fields. Hence, an associative interpolation algorithm is proposed in this paper for improving the learning accuracy of CMAC. Meanwhile, a simulation experiment is described. Its result shows that the learning accuracy of the improved CMAC is ten times higher than that of the original CMAC, and the learning convergence is also faster.

Abstract:In this paper, the authors transform the problem of undirected graph drawing to the problem of function optimization, then use genetic algorithms to find approximate optimal solutions of the objective function, and thus obtain a general structure of undirected graph drawing algorithms. The characters of the new method are: the structures of the different graph drawing algorithms are the same, the difference exists only in the objective functions which reflect aesthetic criteria. The advantages of the method are: unified algorithms, simplicity, easy modification and parallelism, and it can be used to draw non-connected graphs directly.