|
Recent advances in program verification through
computer algebra
Lu YANG, Chaochen ZHOU, Naijun ZHAN, Bican XIA,
Front. Comput. Sci.. 2010, 4 (1): 1-16.
https://doi.org/10.1007/s11704-009-0074-7
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.
References |
Related Articles |
Metrics
|
|
Static worst-case execution time analysis of
the μ C/OS-II real-time kernel
Mingsong LV, Nan GUAN, Qingxu DENG, Ge YU, Wang Yi,
Front. Comput. Sci.. 2010, 4 (1): 17-27.
https://doi.org/10.1007/s11704-009-0073-8
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.
References |
Related Articles |
Metrics
|
|
A semantic model of confinement and Locality
Theorem
Shuling WANG, Qin SHU, Yijing LIU, Zongyan QIU,
Front. Comput. Sci.. 2010, 4 (1): 28-46.
https://doi.org/10.1007/s11704-009-0075-6
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.
References |
Related Articles |
Metrics
|
|
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,
Front. Comput. Sci.. 2010, 4 (1): 47-64.
https://doi.org/10.1007/s11704-009-0076-5
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.
References |
Related Articles |
Metrics
|
|
A new model for model checking: cycle-weighted
Kripke structure
Jiaqi ZHU, Hanpin WANG, Zhongyuan XU, Chunxiang XU,
Front. Comput. Sci.. 2010, 4 (1): 78-88.
https://doi.org/10.1007/s11704-009-0066-7
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.
References |
Related Articles |
Metrics
|
|
A constraint-based topic modeling approach for
name disambiguation
Feng WANG, Jie TANG, Juanzi LI, Kehong WANG,
Front. Comput. Sci.. 2010, 4 (1): 100-111.
https://doi.org/10.1007/s11704-009-0064-9
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.
References |
Related Articles |
Metrics
|
|
An effective scheduling scheme for multi-hop
multicast in wireless mesh networks
Zheng LIU, Heng DAI, Farouk ALKADHI, Jufeng DAI,
Front. Comput. Sci.. 2010, 4 (1): 135-142.
https://doi.org/10.1007/s11704-009-0068-5
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.
References |
Related Articles |
Metrics
|
|
A MANET accessing Internet routing algorithm
based on dynamic gateway adaptive selection
Xin LI, Zhe LI,
Front. Comput. Sci.. 2010, 4 (1): 143-150.
https://doi.org/10.1007/s11704-009-0065-8
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.
References |
Related Articles |
Metrics
|
12 articles
|