Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Existing model checkers are deficient in verifying the systems as only limited kinds of fairness are supported with limited verification efficiency. In this work, we support model checking of distributed systems in the toolkit PAT (process analysis toolkit), with a variety of fairness constraints (e.g., process-level weak/strong fairness, event-level weak/strong fairness, strong global fairness). It performs on-the-fly verification against linear temporal properties. We show through empirical evaluation (on recent population protocols as well as benchmark systems) that PAT has advantage in model checking with fairness. Previously unknown bugs have been revealed against systems which are designed to function only with strong global fairness.
Context-awareness is becoming critical for mobile and ubiquitous computing, where the application needs dynamically adapt its behavior to its execution environment. Context-oriented programming (COP) languages support dynamic behavior adaptation, however, they do not support dynamic layer addition. As a result, they provide little support for the runtime adaptation of application behavior in case that unpredictable execution environments are encountered. Furthermore, block-structured constructs for layer activation hardly support fine-grain adaptation and separate changes of contexts and execution of context-specific methods with difficulty. In this paper, we propose a virtual machine (VM)- centric approach to address these issues. It incorporates object composition and delegation into the VM to implement layer activation, and extends existing VM services to support dynamic layer addition. To ensure that our approach preserves the type safety properties of the program, we develop a calculus built on featherweight Java (FJ) to describe the approach, focus on type-checking issues, and prove type soundness of the calculus. We also present the implementation and evaluation of our approach. The evaluation demonstrates that our approach has advantages over the compilerbased approach proposed by JCOP.
An increasing number of social computational systems consist of a great amount of autonomous entities and operate in highly dynamic and unpredictable environments. To construct such systems needs to seek high-level abstraction to manage the complexity of the systems and novel mechanism to support their characteristics, i.e., dynamism and flexibility. Agent-oriented programming (AOP) is considered as a potential paradigm for developing such systems by exhibiting a number of characteristics, such as autonomy, flexibility, social ability, etc. However, current researches on AOP mainly focus on the construction of multi-agent system (MAS) with theory and language facilities inspired from artificial intelligence (AI) and distributed AI, seldom considering and integrating the proven principles and practices of programming and software engineering. Moreover, abstractions and mechanism based on AI are inadequate for developing dynamic and flexible MAS in open environment. This paper proposes a novel AOP approach, namely Oragent, for constructing and implementing dynamic and flexible systems. From a software engineering perspective, Oragent integrates organizational concepts and mechanism into AOP language, and support the dynamism and flexibility with explicit primitives. The proposed approach consists of a programming model and a corresponding programming language. This paper presents the syntax and formal operational semantics of Oragent language, and studies a case to demonstrate our approach.
Points-to analysis is a static code analysis technique that establishes the relationships between variables of references and allocated objects. A number of points-to analysis algorithms have been proposed for procedural and object-oriented languages like C and Java, while few of them can be used for AspectJ as we know so far. One main reason is that AspectJ is an aspect-oriented language which implements the separation of crosscutting concerns by advices, pointcuts, and inter-type declarations, while a points-to analysis of AspectJ programs may be imprecise because any aspect woven into the base code may change the points-to relations in the program and thus a conservative analysis has to be taken in order to handle the aspects. In this paper, we propose a context-sensitive points-to analysis technique called AJPoints for AspectJ. Similar to the weaving mechanism for AspectJ, AJPoints obtains the constraints and templates on the points-to relations for the base code and the aspects, espectively, but weaves and solves them in an iterative manner in order to cross the boundary between the base code and the aspects. We have implemented AJPoints on abc AspectJ compiler and evaluated it by using twelve AspectJ benchmark programs. The experimental results show that our technique can achieve a high precision about points-to relations in AspectJ programs.
DBSCAN (density-based spatial clustering of applications with noise) is an important spatial clustering technique that is widely adopted in numerous applications. As the size of datasets is extremely large nowadays, parallel processing of complex data analysis such as DBSCAN becomes indispensable. However, there are three major drawbacks in the existing parallel DBSCAN algorithms. First, they fail to properly balance the load among parallel tasks, especially when data are heavily skewed. Second, the scalability of these algorithms is limited because not all the critical sub-procedures are parallelized. Third, most of them are not primarily designed for shared-nothing environments, which makes them less portable to emerging parallel processing paradigms. In this paper, we present MR-DBSCAN, a scalable DBSCAN algorithm using MapReduce. In our algorithm, all the critical sub-procedures are fully parallelized. As such, there is no performance bottleneck caused by sequential processing. Most importantly, we propose a novel data partitioning method based on computation cost estimation. The objective is to achieve desirable load balancing even in the context of heavily skewed data. Besides, We conduct our evaluation using real large datasets with up to 1.2 billion points. The experiment results well confirm the efficiency and scalability of MR-DBSCAN.
Graph model has been widely applied in document summarization by using sentence as the graph node, and the similarity between sentences as the edge. In this paper, a novel graph model for document summarization is presented, that not only sentences relevance but also phrases relevance information included in sentences are utilized. In a word, we construct a phrase-sentence two-layer graph structure model (PSG) to summarize document(s) . We use this model for generic document summarization and query-focused summarization. The experimental results show that our model greatly outperforms existing work.
Flash memory is widely used in embedded devices and enterprise storage systems. Currently, flash-based storage devices usually use a flash translation layer (FTL) to cope with the special features of flash memory. Many methods for the design and implementation of the FTL have been proposed, such as BAST (block-associative sector translation), FAST (fully associative sector translation), and IPL (in-page logging), of which IPL has been demonstrated to have the best performance. However, IPL offers little consideration to reducing merge operations that consequently result in the degradation of the overall performance of flash-memory storage systems. We propose an improvement to IPL, called adaptive IPL (AIPL). The idea of adaptive IPL is to make the log region in a block resizable, therefore a hot block (i.e., a write-intensive block) will use a large log region so as to absorb more page updates and in turn reduce the merge operations, while a cold block, i.e., a block rarely written to, will use a small log region. This is realized by first detecting the update pattern of a block and then presenting an update-pattern-based algorithm to dynamically adjust the log region size of a newly allocated block. We conduct experiments on TPC-C traces and synthetic traces and compare the performance of AIPL with other competitors in terms of merge count, write count and elapsed time. The results demonstrate that compared with IPL, AIPL can reduce merge operations by 65% and write operations by 54% on average.
In this paper, a saliency weighted visual feature similarity (SWVFS) metric is proposed for full reference image quality assessment (IQA). Instead of traditional spatial pooling strategies, a visual saliency-based approach is employed for better compliance with properties of the human visual system, where the saliency allocation is closely related to the activity of posterior parietal cortex and the pluvial nuclei of the thalamus. Assuming that the saliency map actually represents the contribution of locally computed visual distortions to the overall image quality, the gradient similarity and the textural congruency are merged into the final image quality indicator. The gradient and texture comparison play complementary roles in characterizing the local image distortion. Extensive experiments conducted on seven publicly available image databases show that the performance of SWVFS is competitive with the state-of-the-art IQA algorithms.
Splitting touching cells is important for medical image processing and analysis system. In this paper, a novel strategy is proposed to separate ellipse-like or circle-like touching cells in which different algorithms are used according to the concave-point cases of touching domains. In the strategy, a concave-point extraction and contour segmentation methods for cells in series and in parallel are used for the images with distinct concave points, and an improved watershed algorithm with multi-scale gradient and distance transformation is adopted for the images with un-distinct or complex concave points. In order to visualize each whole cell, ellipse fitting is used to process the segments. Experimental results show that, for the cell images with distinct concave points, both of the two algorithms can achieve good separating results, but the concave-point based algorithm is more efficient. However, for the cell images with unobvious or complex concave points, the improved watershed based algorithm can give satisfying segmenting results.
Certificateless public key cryptography eliminates inherent key escrow problem in identity-based cryptography, and does not yet requires certificates as in the traditional public key infrastructure. In this paper, we give crypt-analysis to Hwang et al.’s certificateless encryption scheme which is the first concrete certificateless encryption scheme that can be proved to be secure against “malicious-but-passive” key generation center (KGC) attack in the standard model. Their scheme is proved to be insecure even in a weaker security model called “honest-but-curious” KGC attack model. We then propose an improved scheme which is really secure against “malicious-but-passive” KGC attack in the standard model.