Dec 2008, Volume 2 Issue 4
    

  • Select all
  • SUN Jun, LIU Yang, Dong Jin Song, Sun Jing
    Verification techniques like SAT-based bounded model checking have been successfully applied to a variety of system models. Applying bounded model checking to compositional process algebras is, however, a highly non-trivial task. One challenge is that the number of system states for process algebra models is not statically known, whereas exploring the full state space is computationally expensive. This paper presents a compositional encoding of hierarchical processes as SAT problems and then applies state-of-the-art SAT solvers for bounded model checking. The encoding avoids exploring the full state space for complex systems so as to deal with state space explosion. We developed an automated analyzer which combines complementing model checking techniques (i.e., bounded model checking and explicit on-the-fly model checking) to validate system models against event-based temporal properties. The experiment results show the analyzer handles large systems.
  • WANG Zhifang, CHEN Yiyun, WANG Zhenming, HUA Baojian
    Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic – Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool – plcc was implemented to automatically verify a number of non-trivial pointer programs.
  • BROGI Antonio, POPESCU Razvan
    In this paper we introduce SMoL, a simplified BPEL-like language for specifying peer and service behaviour in P2P systems. We then define a transformational semantics of SMoL in terms of Yet Another Workflow Language (YAWL) workflow
  • GUAN Lianwei, LI Xingyu, HU Hao, LU Jian
    The concept of aspect-orientation allows for modularizing crosscutting concerns as aspect modules. Aspect-orientation originally emerged at the programming level, and has stretched over other development phases now. Among them aspect-oriented modeling (AOM) is a hot topic, and there are many approaches supporting it. Petri net is a good formalism which can provide the foundations for modeling software and simulating its execution, but fails to resolve the problem of crosscutting concerns to support AOM. So, this paper presents an approach which extends the Petri net so as to support the AOM. In this paper, the basic functions of the system are modeled as base net by Petri net, and the crosscutting concerns are modeled as aspect nets. In order to analyze the whole system, woven mechanism is proposed to compose the aspect nets and base net together. The problems about aspect-aspect conflict and conflict relations may exist among the aspect nets matching the shared join point, thus this paper propose solutions to resolve them. The Object Petri net which is an extension of traditional Petri net is also extended so as to support aspect-oriented modeling here.
  • HU Yue, GAO Xiaoyu, LI Li, GAO Qingshi
    To express semantic knowledge of natural languages accurately and unify the processing of languages, the style transformation of natural languages is discussed in an all-round way. The discussion covers purpose, voice, modal, tense, narrow sense of style, number and case. All style transformations may be described accurately by a four-element Descriptive Language of Style Transformation (STDL). The transformation between representation of semantic units without style and with style can be converted through style transformation function. Each style transformation function is a difference function in multiple natural languages. Such difference functions can be used to simplify language processing procedure and improve processing quality.
  • ZHENG Yunping, CHEN Chuanbo, SAREM Mudar
    Although the triangle non-symmetry and anti-packing model (TNAM) representation for gray images is an effective image representation method, there is still much space left for optimization. In this paper, inspired by the optimization idea of the packing problem, we proposed an improved algorithm for gray image representation using the non-symmetry and anti-packing model with triangles and rectangles (NAMTR). By comparing the representation algorithm of the NAMTR with those of the TNAM and the popular linear quadtree, theoretical and experimental results presented in this paper show that the former can greatly reduce the number of sub-patterns or nodes and simultaneously save the data storage much more effectively than the latter, and therefore it is a better method to represent gray images. Representation method of the NAMTR, as envisaged in this paper, shows a very strong promise, and it is valuable for further theoretical research and potential business foreground, such as reducing storage space, increasing transmission speed and improving pattern match efficiency.
  • LI Xin, HUA Bei, XIONG Yan, SHANG Yi
    Most of the state-of-the-art localization algorithms in wireless sensor networks (WSNs) are vulnerable to various kinds of location attacks, whereas secure localization schemes proposed so far are too complex to apply to power constrained WSNs. This paper provides a distributed robust localization algorithm called Bilateration that employs a unified way to deal with all kinds of location attacks as well as other kinds of information distortion caused by node malfunction or abnormal environmental noise. Bilateration directly calculates two candidate positions for every two heard anchors, and then uses the average of a maximum set of close-by candidate positions as the location estimation. The basic idea behind Bilateration is that candidate positions calculated from reasonable (i.e., error bounded) anchor positions and distance measurements tend to be close to each other, whereas candidate positions calculated from false anchor positions or distance measurements are highly unlikely to be close to each other if false information are not collaborated. By using ilateration instead of classical multilateration to compute location estimation, Bilateration requires much lower computational complexity, yet still retains the same localization accuracy. This paper also evaluates and compares Bilateration with three multilateration-based localization algorithms, and the simulation results show that Bilateration achieves the best comprehensive performance and is more suitable to real wireless sensor networks.