A Risk-Sensitive Intrusion Detection Model
Intrusion detection systems (IDSs) must meet the security goals while minimizing risks of wrong detections. In this paper, we study the issue of building a risk-sensitive intrusion detection model. To determinate whether a system calls sequence is normal or not, we consider not only the probability of this sequence belonging to normal sequences set or intrusion sequences set, but also the risk of a false detection. We define the risk model to formulate the expected risk of an intrusion detection decision, and present risk-sensitive machine learning techniques that can produce detection model to minimize the risks of false negatives and false positives. Meanwhile, this model is a hybrid model that combines misuse intrusion detection and anomaly intrusion detection. To achieve a satisfying performance, some techniques are applied to extend this model.

title: Fault-tolerant grid architecture and practice
abstract: Grid computing emerges as effective technologies to couple geographically distributed resources and solve large-scale computational problems in wide area networks. The fault tolerance is a significant and complex issue in grid computing systems. Various techniques have been investigated to detect and correct faults in distributed computing systems. Unreliable fault detection is one of the most effective techniques. Globus as a grid middleware manages resources in a wide area network. The Globus fault detection service uses the well-known techniques based on unreliable fault detectors to detect and report component failures. However, more powerful techniques are required to detect and correct both system-level and application-level faults in a grid system, and a convenient toolkit is also needed to maintain the consistency in the grid. A fault-tolerant grid platform (FTGP) based on an unreliable fault detector and the Globus fault detection service is presented in this paper. The platform offers effective strategies in such three aspects as grid key components, user tasks, and high-level applications.

title: SVG Web Environment for Z Specification Language
abstract: This paper presents a web environment for the Z formal specification language using the Scalable Vector Graphics (SVG) technology. The Z Specification Web Editor (ZSWE) is the first prototype of a web based graphical editor for the Z specification language. It not only supports graphical editing and global accessibility for the Z formal specifications, but also provides model comprehension facilities such as schema expansion, specification navigation and model querying. This paper outlines the requirement, design and implementation of the tool and its future improvements.

title: Hybrid Control of Automotive Powertrain Systems: A Case Study
abstract: In this paper, a hybrid control design approach is used to develop control strategies for coordination of automotive engine and transmission systems. The main goal is to improve system performance, fuel economy, robustness and other performance specifications. The method employs performance indices in guiding both analog and discrete control actions such that robust stability and performance of closed-loop hybrid systems are maintained, in the presence of modeling errors, disturbances and structural uncertainties.

title: Algorithmic Design Using Object-Z for Twig XML Queries Evaluation
abstract: Web technologies based on XML, e.g. Semantic Web and Web Services, facilitate Web automation and universally accessible content. One of the key factors for the success of XML-based technologies is of finding an efficient query evaluation algorithm for XML-based data models. An XML twig query is a complex selection predicate on both structure and content of a labelled XML document. Several novel twig query evaluation algorithms have been proposed recently. However, these algorithms are difficult to understand and hence implement due to high complexity. In this work, we present an algorithmic design for XML queries evaluation system using Object-Z. An Object-Z specification is developed to give a concise and logical description of the XML data model and the twig queries. It makes the twig query evaluation straight-forward, and allows different evaluation algorithms to be constructed easily and independently.

title: Reasoning about semantic Web in Isabelle/HOL
abstract: Semantic Web is regarded as the next generation of the World Wide Web. It provides not only the structure of the Web but also meaningful semantics for the information presented. To make semantic Web services understandable for distributed agents, formal definitions of the ontologies and their consistencies are essential. However, the existing tools for reasoning about semantic Web ontologies are still primitive. We believe that mature software engineering tools, such as theorem provers, can contribute to the reasoning phase. In this paper, we present an approach of encoding the semantic Web ontology (DAML+OIL) into the generic theorem prover Isabelle/HOL for automatic reasoning. Furthermore, a translation tool was developed to transform semantic Web ontologies into their extended Isabelle theories. With additional intermediate lemmas, Isabelle can be used to perform both subsumption (class) level and instantiation (instance) level reasoning of the semantic Web ontologies.

title: Z Approach to Semantic Web
abstract: The Semantic Web (SW) service is a web application using Semantic Web techniques which usually involve cooperation between several intelligent agents. The design of SW systems requires precise modelling techniques to capture ontology domain properties and application functionalities. We believe that Z as a specification technique can contribute to the Semantic Web-based system development in many ways. In this paper, we firstly conduct a case study of applying Z to the design of a SW service system (online talk discovery), and then present translation techniques and tools which can extract the SW ontology from the Z model automatically. Furthermore, we discuss how existing Z tools, i.e. Z/EVES, can be used to improve the quality of SW ontology design.