Situ L.,Nanjing University |
Zhao L.,Guangxi Key Laboratory of Trusted Software |
Zhao L.,Guilin University of Electronic Technology
Proceedings - Asia-Pacific Software Engineering Conference, APSEC | Year: 2016
Model checking is a mainstream method for formal verification of communicating sequential processes (CSP). Existing CSP Model Checkers are incapable of verifying multiple properties concurrently in one run of a model checker. In addition, the properties to be verified are described with CSP in most model checkers, which is good for refinement checking, but leads to limited description power and weak generality. In order to tackle the two problems, answer set programming(ASP), which is completely free of sequential dependencies, is used to construct a CSP bounded model checking framework, where the CSP model checking problem is turned into a computation problem of answer sets. CTL is extended with events to describe the properties to be verified. In addition, preprocessing technique of properties is proposed for the sake of reducing the expense spending on replicated verification of the same sub formulas. An ASP based description system is constructed for complete description of various CSP processes and automatic generation of parallel processes. We integrated all the methods into a CSP model checker - ACSPChecker. The feasibility and efficiency of our methods are illustrated by the experiments with a classic concurrency problem - dining philosophers problem. © 2015 IEEE.
Li W.-J.,China University of Mining and Technology |
Jiang S.-J.,China University of Mining and Technology |
Qian J.-Y.,Guilin University of Electronic Technology |
Qian J.-Y.,Guangxi Key Laboratory of Trusted Software |
And 3 more authors.
Tien Tzu Hsueh Pao/Acta Electronica Sinica | Year: 2015
An approach was proposed to analyze the memory behavior of Java programs based on object reference relations. Unlike traditional methods that just consider the factor of memory consumption to find out program's important data structures and analyze their memory behavior, our approach considers both memory consumption and memory domination to decide whether a data structure is important, and get the important memory behaviors via analyzes the memory dominance relationship between data structures and references analysis. Experimental results show that the proposed approach is effective, and can get more precise analysis results than other methods. ©, 2015, Chinese Institute of Electronics. All right reserved.
Li X.,Guilin University of Electronic Technology |
Li X.,Guangxi Key Laboratory of Trusted Software |
Dong S.,Guilin University of Electronic Technology |
Si L.,Guilin University of Electronic Technology |
Liang H.,Guilin University of Electronic Technology
Gaojishu Tongxin/Chinese High Technology Letters | Year: 2014
To realize the secure coverage in wireless sensor networks, a Highly Reliable distributed Coverage Mechanism based on Trust Management (HRCMTM) was proposed by integrating a coverage algorithm into a trust management system. Through the analysis of the underlying requirements of trust management systems, the proper grid size was derived theoretically. The new concept of dynamic trust threshold was introduced to quantitatively analyze the relationship between the size of coverage node set, the joint trust level and the dynamic trust threshold. Futher more, a node scheduling coverage algorithm was designed to guarantee that the target area is covered reliably. The experimental results demonstrated the effectiveness of this mechanism in terms of coverage ratio and joint trust level.
Li X.-L.,Guilin University of Electronic Technology |
Li X.-L.,Guangxi Key Laboratory of Trusted Software |
Feng D.-L.,Guilin University of Electronic Technology |
Peng P.-C.,Guilin University of Electronic Technology
Wuli Xuebao/Acta Physica Sinica | Year: 2016
In real-world applications, wireless sensor networks often consist of a large number of sensor nodes with constraint battery resources. How to reduce the power consumption of sensor nodes and maximize the network life, becomes the most important goal of topology control schemes in wireless sensor networks. During the operation of networks, sensor nodes may spend different levels of energy, and result in the uneven distribution of residual energy of sensor nodes. In order to extend the network life, it is essential to adjust the network burden of sensor nodes dynamically, so as to achieve energy balance among nodes under the consideration of different energy levels at nodes. In this paper, we introduce the game theory and the concept of game potential. By synthetically considering the factors of the residual energy and transmission power of nodes, a potential game based mathematical model of topology control is constructed. We prove the existence of Nash equilibrium. Through designing a payoff function, which takes into account both network connectivity and energy balance of nodes, the connectivity of sensor networks can be maintained while the power of sensor nodes is reduced. By increasing the average value of residual energy of neighbors, it enables to select nodes with more energy that reserves in neighborhood as neighbors, to improve the energy balance among nodes. Based on that, a distributed energy-balanced topology control algorithm (DEBA) is proposed. Theoretical analysis proves that the algorithm can maintain network connectivity. Compared with other existing game theory based algorithms DIA and MLPT, the topologies formed by the proposed algorithm have fewer bottleneck nodes which feature heavy traffic load and low residual energy, and smaller variance of node residual energy, thus achieving a longer life. © 2016 Chinese Physical Society.
Zhao L.,Guilin University of Electronic Technology |
Zhao L.,Guangxi Key Laboratory of Trusted Software |
Zhang L.,Guilin University of Electronic Technology |
Qian J.,Guilin University of Electronic Technology |
And 2 more authors.
Journal of Computational Information Systems | Year: 2014
Existing CSP model checkers are based on operational semantics, which need to translate processes into a label transition system. The conversion process is complex. Moreover, in most CSP model checkers, the properties to be verified are described by CSP, which is helpful for refinement checking, but leads to limited description power and weak generality. Therefore, ASP techniques have been proposed to verify CSP concurrent systems in our previous work. However, the methods are inadequate for verifying communication protocols, which may include assignment operator and an event contains channel and message. In this paper, a significant extension to the previous verification framework is proposed, which includes the ASP representation of prefix and assignment operator and concurrency rules. Practice with AB protocol shows the correctness and feasibility of the method for verifying communication protocols. © 2014 Binary Information Press.