Verification of Computation Orchestration Via Timed Automata
Recently, a promising programming model called Orc has been proposed to support a structured way of orchestrating distributed web services. Orc is intuitive because it offers concise constructors to manage concurrent communication, time-outs, priorities, failure of sites or communication and so forth. The semantics of Orc is also precisely defined. However, there is no verification tool available to verify critical properties against Orc models. Instead of building one from scratch, we believe the existing mature model-checkers can be reused. In this work, we first define a Timed Automata semantics for the Orc language, which we prove is semantically equivalent to the original operational semantics of Orc. Consequently, Timed Automata models are systematically constructed from Orc models. The practical implication of the construction is that tool supports for Timed Automata, e.g., UPPAAL, can be used to model check Orc models. An experimental tool is implemented to automate our approach.

title: XML-Based Static Type Checking and Dynamic Visualization for TCOZ
abstract: Timed Communicating Object Z(TCOZ) combines Object-Z's strengths in modelling complex data and state with TCSP's strengths in modeling real-time concurrency. Based on our previous work on the XML environment for TCOZ, this paper firstly demonstrates the development of a type checker for detecting static semantic errors of the TCOZ specification, then illustrates a transformation tool to automatically project TCOZ models into UML statechart diagrams for visualising the dynamic system behaviour.

title: A tools environment for developing and reasoning about ontologies
abstract: Started in the beginning of 2001, the semantic Web is regarded by many as the next generation of the Web. Ontology languages are the building blocks of semantic Web as they provide basic vocabularies for data markups: the ontologies. The correctness of shared ontologies is crucial to the proper functioning of agents. Hence ensuring the consistency of ontologies is a central issue in both the design and deployment phases of any semantic Web-aware application. Our experiences show that semantic Web is a novel and fruitful application domain for formal languages and their mature reasoning tool support. In order to ease the application of formal methods and tools to the semantic Web, we developed an integrated tools environment to support systematic development of OWL ontologies and then transformation, reasoning assistance and querying of them.

title: Object-Z web environment and projections to UML
abstract: This paper presents the XML/XSL approach to the development of a web environment for the formal speci cation language Object-Z. The projection techniques and tools from Object-Z (in XML) to UML (in XMI) are developed using XSL Transformations (XSLT). Furthermore, Object-Z (itself) is used to specify and design the essential functionalities of the web environment and the projection tools to UML. In a sense, the paper also demonstrates a formal approach to modeling web applications.

title: Validating Semistructured Data Using OWL
abstract: Semistructured data has become prevalent in both web applications and database systems. This rapid growth in use makes the design of good semistructured data essential. Formal semantics and automated reasoning tools enable us to reveal the inconsistencies in a semistructured data model and its instances. The Object Relationship Attribute model for Semistructured data (ORA-SS) is a graphical notation for designing and representing semistructured data. This paper presents a methodology of encoding the semantics of ORA-SS in the Web Ontology Language (OWL) and automatically validating the semistructured data design using the OWL reasoning tool – RACER. Our methodology provides automated consistency checking of an ORA-SS data model at both the schema and instance levels.

title: A Z Approach in Validating ORA-SS Data Models
abstract: The rapid growth of the World Wide Web has resulted in more data being accessed over the Internet. In turn there is an increase in the use of semistructured data, which plays a crucial role in many web applications particularly with the introduction of XML and its related technologies. This increase in use makes the design of good semistructured data structures essential. The Object Relationship Attribute model for Semistructured data (ORA-SS) is a graphical notation for designing and representing semistructured data. In this paper, we demonstrate an approach to formally validate the ORA-SS data models in order to enhance the correctness of semistructured data design. A mathematical semantics for the ORA-SS notation is defined using the Z formal language, and further validation processes are carried out to check the correctness of the semistructured data models at both the schema and instance levels.

title: GE-CKO: A Method to Optimize Composite Kernels for Web Page Classification
abstract: Most of current researches on Web page classification focus on leveraging heterogeneous features such as plain text, hyperlinks and anchor texts in an effective and efficient way. Composite kernel method is one topic of interest among them. It first selects a bunch of initial kernels, each of which is determined separately by a certain type of features. Then a classifier is trained based on a linear combination of these kernels. In this paper, we propose an effective way to optimize the linear combination of kernels. We proved that this problem is equivalent to solving a generalized eigenvalue problem. And the weight vector of the kernels is the eigenvector associated with the largest eigen-value. A support vector machine (SVM) classifier is then trained based on this optimized combination of kernels. Our experiment on the WebKB dataset has shown the effectiveness of our proposed method.

title: Distributed Pattern Discovery in Multiple Streams
abstract: Given m groups of streams which consist of n1,...,nm co-evolving streams in each group, we want to: (i) incrementally find local patterns within a single group, (ii) efficiently obtain global patterns across groups, and more importantly, (iii) efficiently do that in real time while limiting shared information across groups. In this paper, we present a distributed, hierarchical algorithm addressing these problems. Our experimental case study confirms that the proposed method can perform hierarchical correlation detection efficiently and effectively.

title: Efficient Immunization Algorithm for Peer-to-Peer Networks
abstract: In this paper, we present a detail study about the immunization of viruses in Peer-to-Peer networks with power-law degree distributions. By comparing two different immunization strategies, we conclude that it is efficient to immunize the highly connected nodes in order to eradicate viruses from the network. Furthermore, we propose an efficient updating algorithm of global virus database according to the degree-based immunization strategy.

title: Text Classification Improved through Automatically Extracted Sequences
abstract: We propose to use the n-multigram model to help the automatic text classification task. This model could automatically discover the latent semantic sequences contained in the document set of each category. Based on the n-multigram model and the n-gram language model, we put forward two text classification algorithms. The experiments on RCV1 show that our proposed algorithm based on n-multigram model can achieve the similar classification performance compared with the one based on n-gram model. However, the model size of our algorithm is only 4.21% of the latter one. Another proposed algorithm based on the combination of nmultigram model and n-gram model improves the micro- F1 and macro-F1 values by 3.5% and 4.5% respectively which support the validity of our approach.

title: Subjectivity Categorization of Weblog with Part-of-Speech Based Smoothing
abstract: Experts from different domains try to mine users' comments on Weblogs for different reasons such as politics or commerce. All these needs necessitate automatically distinguishing subjective Weblog contents from objective ones, namely subjectivity categorization. Since Weblogs contain various topics from different domains, limited training data can hardly cover all the topics and "unseen words" becomes a serious problem for categorization tasks. In this paper, part-of-speech (POS) based smoothing is proposed to alleviate the "unseen words" problem. In conjunction with a naive Bayes model constructed from limited training data, the probability of an unseen word in a new domain can be well smoothed by the probability of its POS result. Empirical studies on five datasets show that our approach consistently outperforms the basic naive Bayes with Laplace smoothing. In a cross-domain experiment, our approach achieves 22.0% improvement in Macro Fl and 24.4% in Micro Fl over basic naive Bayes. These verify that POS based smoothing can indeed benefit subjectivity categorization, especially in the cases with a large number of unseen words.