Mar 2010, Volume 4 Issue 1
    

  • Select all
  • Research articles
    Recent advances in program verification through computer algebra
    Lu YANG, Chaochen ZHOU, Naijun ZHAN, Bican XIA,
    2010, 4(1): 1-16. https://doi.org/10.1007/s11704-009-0074-7
    Download PDF
    In this paper, we summarize the results on program verification through semi-algebraic systemsSASs solving that we have obtained, including automatic discovery of invariants and ranking functions, symbolic decision procedure for the termination of a class of linear loops, termination analysis of nonlinear systems, and so on.
  • Research articles
    Static worst-case execution time analysis of the μ C/OS-II real-time kernel
    Mingsong LV, Nan GUAN, Qingxu DENG, Ge YU, Wang Yi,
    2010, 4(1): 17-27. https://doi.org/10.1007/s11704-009-0073-8
    Download PDF
    Worst-case execution time (WCET) analysis is one of the major tasks in timing validation of hard real-time systems. In complex systems with real-time operating systems (RTOS), the timing properties of the system are decided by both the applications and RTOS. Traditionally, WCET analysis mainly deals with application programs, while it is crucial to know whether RTOS also behaves in a timely predictable manner. In this paper, static analysis techniques are used to predict the WCET of the system calls and the Disable Interrupt regions of the μC/OS-II real-time kernel, which presents a quantitative evaluation of the real-time performance of μC/OS-II. The precision of applying existing WCET analysis techniques on RTOS is evaluated, and the practical difficulties in using static methods in timing analysis of RTOS are also discussed.
  • Research articles
    A semantic model of confinement and Locality Theorem
    Shuling WANG, Qin SHU, Yijing LIU, Zongyan QIU,
    2010, 4(1): 28-46. https://doi.org/10.1007/s11704-009-0075-6
    Download PDF
    Confinement is required in object-oriented programming in order to protect sensitive object references. Recently a range of confinement schemes have been proposed to achieve object encapsulation by defining static type systems, but unavoidably, with strong restrictions. On the other hand, no similarity in concepts makes assessing of these schemes a difficulty. We build in this paper a semantic model for confinement in μJava, a subset of sequential Java that offers most objectoriented features. This model has limited restriction for programs. From a semantic view, confinement is defined with respect to a given context that specifies partition of the object pool and confinement constraint among them. Moreover, we present the main Locality Theorem for checking well confinement of programs locally. By applying this Theorem, we have solved a security breach problem from Java JDK 1.1.1, and furthermore, proved the soundness of two widely used confinement schemes: confined types and ownership types.
  • Research articles
    TRainbow: a new trusted virtual machine based platform
    Yuzhong SUN, Ying SONG, Yunwei GAO, Haifeng FANG, Kai ZHANG, Hongyong ZANG, Yaqiong LI, Yajun YANG, Ran AO, Yongbing HUANG, Lei DU,
    2010, 4(1): 47-64. https://doi.org/10.1007/s11704-009-0076-5
    Download PDF
    Currently, with the evolution of virtualization technology, cloud computing mode has become more and more popular. However, people still concern the issues of the runtime integrity and data security of cloud computing platform, as well as the service efficiency on such computing platform. At the same time, according to our knowledge, the design theory of the trusted virtual computing environment and its core system software for such network-based computing platform is at the exploratory stage. In this paper, we believe that efficiency and isolation are the two key proprieties of the trusted virtual computing environment. To guarantee these two proprieties, based on the design principle of splitting, customizing, reconstructing, and isolation-based enhancing to the platform, we introduce TRainbow, a novel trusted virtual computing platform developing by our research group. With the two creative mechanisms, that is, capacity flowing amongst VMs and VM-based kernel reconstructing, TRainbow provides great improvements (up to 42%) in service performance and isolated reliable computing environment for Internet-oriented, large-scale, concurrent services.
  • Research articles
    Formal verification of concurrent programs with read-write locks
    Ming FU, Yu ZHANG, Yong LI,
    2010, 4(1): 65-77. https://doi.org/10.1007/s11704-009-0067-6
    Download PDF
    Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms.
    This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.
  • Research articles
    A new model for model checking: cycle-weighted Kripke structure
    Jiaqi ZHU, Hanpin WANG, Zhongyuan XU, Chunxiang XU,
    2010, 4(1): 78-88. https://doi.org/10.1007/s11704-009-0066-7
    Download PDF
    This paper proposes a new model, named cycle-weighted Kripke structure (CWKS), based on the traditional Kripke structure. It adds two integer weights to some transitions of the Kripke structure, restricting when these transitions can occur. These weights mainly specify the occurrences of some cycles in a Kripke structure, giving a range of how many times these cycles may be executed repeatedly. This new model can efficiently describe some quantitative discrete-time characters of reactive and concurrent systems, so it is significant for some model checking problems. We also define a subset of CWKS, named conditional CWKS, which satisfies a constraint referring to the weighted transitions in the structure. The paper modifies the explicit computation tree logic (CTL) model checking algorithm to accommodate the conditional CWKS. It can also be regarded as the foundation of some more complex models obtained by extending from the Kripke structure, which will be studied in the future.
  • Research articles
    Mining non-redundant diverse patterns: an information theoretic perspective
    Chaofeng SHA, Jian GONG, Aoying ZHOU,
    2010, 4(1): 89-99. https://doi.org/10.1007/s11704-009-0072-9
    Download PDF
    The discovery of diversity patterns from binary data is an important data mining task. In this paper, we propose the problem of mining highly diverse patterns called non-redundant diversity patterns (NDPs). In this framework, entropy is adopted to measure the diversity of itemsets. In addition, an algorithm called NDP miner is proposed to exploit both monotone properties of entropy diversity measure and pruning power for the efficient discovery of non-redundant diversity patterns. Finally, our experimental results are given to show that the NDP miner can efficiently identify non-redundant diversity patterns.
  • Research articles
    A constraint-based topic modeling approach for name disambiguation
    Feng WANG, Jie TANG, Juanzi LI, Kehong WANG,
    2010, 4(1): 100-111. https://doi.org/10.1007/s11704-009-0064-9
    Download PDF
    Name ambiguity refers to a problem that different people might be referenced with an identical name. This problem has become critical in many applications, particularly in online bibliography systems, such as DBLP and CiterSeer. Although much work has been conducted to address this problem, there still exist many challenges. In this paper, a general framework of constraint-based topic modeling is proposed, which can make use of user-defined constraints to enhance the performance of name disambiguation. A Gibbs sampling algorithm that integrates the constraints has been proposed to do the inference of the topic model. Experimental results on a real-world dataset show that significant improvements can be obtained by taking the proposed approach.
  • Research articles
    Improved feedback modeling of transport in enlarging urban areas of developing countries
    Xuesong FENG, Yoshitsugu HAYASHI, Hirokazu KATO, Junyi ZHANG, Akimasa FUJIWARA,
    2010, 4(1): 112-122. https://doi.org/10.1007/s11704-009-0069-4
    Download PDF
    Toward the common issue of quick urban sprawls of many cities in developing countries today, this research incorporates the expectation-maximization (EM) algorithm into the feedback application process of a newly developed feedback model to improve the modeling studies of the urban transport prediction and planning for the developments of the cities with their urban areas enlarged in the future. By utilizing the survey data obtained in Jabodetabek metropolitan region of Indonesia in 2002, the study results numerically confirm that the iteratively computational calibrations to the K-factors for the newly urbanized areas of a developing city by employing the EM algorithm in the feedback process can truly improve the validity of the proposed feedback model’s application to effectively predict the urban transport developments of developing cities in the future.
  • Research articles
    Efficient distributed location verification in wireless sensor networks
    Qiyuan ZHANG, Xuehai ZHOU,
    2010, 4(1): 123-134. https://doi.org/10.1007/s11704-009-0071-x
    Download PDF
    In wireless sensor networks, reliable location information is not only necessary to event reports but also crucial to network functionalities such as geographic routing, distributed information storage/retrieval. However, sensors could be compromised by adversaries to claim arbitrary locations to disrupt the normal network operation. Thus, location verification should be carried out for security considerations. Due to the importance of the problem, we propose a highly efficient algorithm that effectively detects false location claims from compromised sensors. Extensive analysis and simulation results demonstrate that our algorithm is energy-efficient and resilient against adversaries.
  • Research articles
    An effective scheduling scheme for multi-hop multicast in wireless mesh networks
    Zheng LIU, Heng DAI, Farouk ALKADHI, Jufeng DAI,
    2010, 4(1): 135-142. https://doi.org/10.1007/s11704-009-0068-5
    Download PDF
    With the utilization of concurrent transmission strategy, a throughput-enhanced scheduling scheme is devised for multicast service in wireless multi-hop mesh networks. Since the performance of a multicast mechanism is constrained in a wireless setting due to the interference among local wireless transmissions, the interference relationships are first characterized by introducing a graph transformation method. Based on the graph transformation, the multicast scheduling problem is converted to the graph coloring problem, and then a capacity greedy algorithm is designed to provide concurrent transmission scheduling so that the demanded multicast transmission rate can be achieved. Moreover, the necessary and sufficient conditions of multicast schedulable feasibility are derived. Through corresponding simulations, it is shown that the proposed strategy can enhance the throughput of wireless multi-hop multicast systems significantly.
  • Research articles
    A MANET accessing Internet routing algorithm based on dynamic gateway adaptive selection
    Xin LI, Zhe LI,
    2010, 4(1): 143-150. https://doi.org/10.1007/s11704-009-0065-8
    Download PDF
    Based on the study on communication situation of mobile ad hoc network (MANET) accessing Internet and taking the gateway important function of accessing network into account, a MANET accessing Internet routing algorithm based on dynamic gateway adaptive selection (MRBDAS) is presented. It considers candidate gateways’ connecting degree, load degree, residual energy, and movement rate synthetically and uses the idea of group decision-making method for reference. The algorithm employs the methods of multipaths and query localization technique based on old path information to maintain routing adaptively. Compared with the existing accessing routing algorithm based on dynamic gateway, the algorithm demonstrates in its simulations that by bringing dynamic gateways colony function, the MRBDAS can improve network throughput, reduce average transmission delay of data packets and routing overhead, and prolong accessing network life. The validity of MRBDAS has been proven.