Distributed Virtual Reality (DVR) is a combination of network and virtual reality technology, it could facilitate to construct a uniformly shared Distributed Virtual Environment (DVE) by using network to connect geographically distributed multiplayers. This paper concentrates on the theoretical research and practical development about Multiplayer Virtual Intelligent System (MVIS), and the main contribution could be summarized as two points. (1) Based on the DVR technology, this paper presented some theoretical research on MVIS, including the classification of virtual entities, communication pattern of entities, and the behavioral consistency research. Furthermore, a Multiplayer Earliest Deadline First (MEDF) program was proposed in order to guarantee the consistency of entities. (2) A prototype algorithm experiment system, called Multiplayer Graph-algorithm Intelligent System (MGIS), was designed. MGIS not onlyefficiently solves many problems in traditional computer algorithm teaching, such as high-abstraction, difficulty to understand, and lack of interaction mechanism; but also extends the application of DVR to cultural tourism, because MGIS is developed on the 3D scene of Lushan Mountain, which is one of the notable tourist attractions in China, and was included in the UNESCO World Heritage list in 1996. What i’s more, MGIS illustrates the ability of expression, applicability and generality of the theoretical research about MVIS.

Summary Service‐oriented paradigm presents numerous new software development patterns and idioms. Software systems are implemented by composing existing third‐party services deployed in the open environment, which is significantly different from traditional software development methodologies in which systems are built through developing modules after system design in a closed environment. Therefore, it is urgent to raise a new design method to adapt to this new circumstance. We concentrate on reusing as many deployed services as possible then introduce a new life cycle model named Taiji model to illustrate this development process. The iteration‐based interactive analysis method following the model is proposed to design service‐oriented systems based on the view of extracting non‐creative activities from a creative activity through defining new notations or applying new rules. The method includes the interactive analysis process that analyzes requirements with deployed services in a local point of view and the iterative analysis process that redesigns system with new knowledge in a global perspective. Meanwhile, the reusable service threshold value is defined to build the uncertain candidate service set (UCSS) of each module in analysis process. The reliability and flexibility of systems can be improved through the quantitative static structure analysis on the basis of the UCSS of systems. Meanwhile, a practical dynamic service binding method that selects services according to actual states of invoking them is presented on the basis of the UCSS containing them. Finally, we also give a case study to illustrate the feasibility of this method. Copyright © 2017 John Wiley & Sons, Ltd.

Summary OSEK/VDX, a development standard for automobiles, has now been widely adopted by automotive manufacturers for developing a vehicle‐mounted system. The ever increasing complexity of the system has created a challenge for ensuring the reliability of the developed OSEK/VDX applications in exhaustive way. Model checking as an exhaustive verification technique has attracted much attention in the automotive industry. To check OSEK/VDX applications by using model checking verification techniques, we have proposed a method based on SMT‐based bounded model checking. However, the method performs a poor efficiency in checking the OSEK/VDX applications that hold many loops, especially it is unable to deal with interruptions. In this paper, to apply model checking verification techniques to check a practical OSEK/VDX application, we develop and investigate an alterative approach based on the well‐known model checker Spin. In our Spin‐based approach, interruptions are taken into account, and moreover, 2 optimization strategies are used to boost the scalability and efficiency of the approach by reducing state space and accelerating bug detection. We have investigated the Spin‐based approach based on a series of experiments. The experimental results show that the approach is an impactful technique to verify the developed OSEK/VDX applications that hold a number of loops and interruptions.

Hanoi Tower problem is an ancient and interesting puzzle and Isabelle is one of famous proof assistants. We have put forward a method to verify the correctness of algorithmic programs based on Isabelle, and have presented formal derivation and proof about the non-recursive algorithm of Hanoi Tower problem in our previous work. The focus of this paper is to turn the former manual verification to automatic verification by using Isabelle Theorem Prover. On the other hand, we originally find a boundary function, which used to proof termination of our non-recursive algorithm of Hanoi Tower problem. This work realizes mechanically automatic-verifying the complete correctness of our non-recursive algorithm of Hanoi Tower Problem, and overcomes the intricacies of manual verification, improves the verification efficiency, and ensures the trustworthiness and reliability of the algorithm program.

The motivation of Web service comes from its interoperational ability so a large number of Web services can interact with others and constitute an open network, Web service network. The success of Web services selection rely on, not only its Qos capability advertised, but the trustworthy of QoS to large degree. How to evaluate the trustworthy of services QoS information, however, is a challenge in Web service network. Reputation system, a mechanism which assesses the future QoS performance by the past behavior of service, is one of promising approaches to facilitate users make optimal decision. In this paper, we present a hybrid framework of reputation model for Web service. Based on this hybrid architecture, clients build their specific social communities, by which they obtain service's prior reputation. At the same time, the central reputation system fuses the rating data from clients by bayesian estimation. The result of experiments illustrated our approach is more efficiency and accuracy in several aspects, especially when dealing with strategics services.

Using highly configurable semi-automatic approach to algorithmic programs development can improve correctness and productivity. This paper explores a way to use generative techniques to produce the algorithmic programs for searching problem. Based on PAR method and PAR platform, it is to formally develop generic type component and algorithm components, and to design a formal algorithm generative model that models an invariant behavior in terms of variant behaviors, and then to automatically generate a variety of specialized searching algorithmic programs through replacing the generic identifiers with a few concrete operations. Through the super framework and underlying components, the reliability and productivity of domain specific algorithms are dramatically improved.

The article presents a sample derivation and proof for Knuth's program (D. Knuth, 1990) that translates a binary fraction to a decimal fraction. The main technique used is the partition-and-recur approach, that is, partitioning the problem, deriving an algorithm represented by recurrences, and finally transforming the algorithm to a program in a straightforward manner. Practice with this example has given us more confidence that partition-and-recur is a practicable approach for derivation and proof of general algorithms and programs.