A New Formal Method for Communication Protocol Specification

A new formal method for communication protocol specification is presented.FSM,CSP and ADT are mixed and the best features of these approaches can be offered in the fomal method.First,we briefly describe the formal techniques of communication protocol.We then put forward the hybrid method of protocol specification.Finally,an example,i.e.,IEEE 802.3 MAC protocol for LAN described by the proposed formal method,is given.The results of studies show that this hybrid formal method for protocol specification is a correct,unambiguous and complete approach.     

Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL

Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.     

A semantically complete extension sequence of the system (?)

In this paper, the method of well-combined semantics and syntax proposed by Pavelka is applied to the research of the prepositional calculus formal system (?)*. The partial constant values are taken as formulas, formulas are fuzzified in two manners of semantics and syntax, and inferring processes are fuzzified. A sequence of new extensions {(?)_n~*} of the system ? is proposed, and the completeness of (?)_n~* is proved.     

Attribute reduction theory of concept lattice based on decision formal contexts

The theory of concept lattices is an efficient tool for knowledge representation and knowledge discovery, and is applied to many fields successfully. One focus of knowledge discovery is knowledge reduction. Based on the reduction theory of classical formal context, this paper proposes the definition of decision formal context and its reduction theory, which extends the reduction theory of concept lattices. In this paper, strong consistence and weak consistence of decision formal context are defined respectively. For strongly consistent decision formal context, the judgment theorems of consistent sets are examined, and approaches to reduction are given. For weakly consistent decision formal context, implication mapping is defined, and its reduction is studied. Finally, the relation between reducts of weakly consistent decision formal context and reducts of implication mapping is discussed.     

Object-oriented analysis of ELIMINO

ELIMINO is a mathematical research system developed for the implementation of Wu‘s method,a powerful method for polynomial equation system solving and geometric theorem proving.The aim of ELIMINO is to provide user a programmable interpreting environment to use Wu‘s method in scientific research and engineering computation.In this paper,the development of ELIMINO system is outlined and the techniques adopted are discussed,then some details about the aobject-oriented analysis of ELIMINO are presented.     

Gallbladder Removal Simulation for Laparoscopic Surgery Training: A Hybrid Modeling Method

Laparoscopic surgery has many advantages, but it is difficult for a surgeon to achieve the necessary surgical skills. Recently, virtual training simulations have been gaining interest because they can provide a safe and efficient learning environment for medical students and novice surgeons. In this paper, we present a hybrid modeling method for simulating gallbladder removal that uses both the boundary element method (BEM) and the finite element method (FEM). Each modeling method is applied according to the deformable properties of human organs: BEM for the liver and FEM for the gallbladder. Connective tissues between the liver and the gallbladder are also included in the surgical simulation. Deformations in the liver and the gallbladder models are transferred via connective tissue springs using a mass-spring method. Special effects and techniques are developed to achieve realistic simulations, and the software is integrated into a custom-designed haptic interface device. Various computer graphical techniques are also applied in the virtual gallbladder removal laparoscopic surgery training. The detailed techniques and the results of the simulations are described in this paper.     

0ntology建模方法研究

The ontology model of a certain domatin is an effective approach for the intercommunion between people form the different domains,the communication and interoperation among agents,and the share and reuse of the software.But the lack of formal analysis tools for domain modeling results in taking liberties with conceptualization.This paper discusses how to introduce the ontological notions from philosophy into Knowledge Engineering in order to supply a set of formal analysis tools for conceptualization analysis.This method can definitely record the hypothesis and analysis criterions through ontology huilding,and clarify the hiberarchy of concepts.     

Identification Schemes for Unmanned Excavator Arm Parameters

Parameter identification is a key requirement in the field of automated control of unmanned excavators(UEs).Further- more,the UE operates in unstructured,often hazardous environments,and requires a robust parameter identification scheme for field applications.This paper presents the results of a research study on parameter identification for UE.Three identification methods, the Newton-Raphson method,the generalized Newton method,and the least squares method are used and compared for prediction accuracy,robustness to noise and computational speed.The techniques are used to identify the link parameters(mass,inertia,and length)and friction coefficients of the full-scale UE.Using experimental data from a full-scale field UE,the values of link parameters and the friction coefficient are identified.Some of the identified parameters are compared with measured physical values.Furthermore, the joint torques and positions computed by the proposed model using the identified parameters are validated against measured data. The comparison shows that both the Newton-Raphson method and the generalized Newton method are better in terms of prediction accuracy.The Newton-Raphson method is computationally efficient and has potential for real time application,but the generalized Newton method is slightly more robust to measurement noise.The experimental data were obtained in collaboration with QinetiQ Ltd.     

The Application of VDM to the Industrial Development of Firmware for a Smart Card IC Chip

We have applied the formal speci.cation language in the development of the .rmware of the smart card IC chip for embedding in mobile phone. We report on an in-dustrial application of formal methods to the development of a complex system, namely the .rmware for the “Mobile FeliCa” smart card IC chip. The use of formal techniques, specif-ically the Vienna Development Method (VDM), was aimed at raising the quality of system speci.cations by reducing ambiguity and improving communications between engineers. De-velopment data gathered during the life cycle con.rm the e.ectiveness of a lightweight formal method in contributing to the quality of the deliverables in early development stages. No software speci.cation problems have, to date, been reported since .rst release (over 100 million mobile phones have the chip embedded).     

Identification schemes for unmanned excavator arm parameters

Parameter identification is a key requirement in the field of automated control of unmanned excavators （UEs）. Furthermore, the UE operates in unstructured, often hazardous environments, and requires a robust parameter identification scheme for field applications. This paper presents the results of a research study on parameter identification for UE. Three identification methods, the Newton-Raphson method, the generalized Newton method, and the least squares method are used and compared for prediction accuracy, robustness to noise and computational speed. The techniques are used to identify the link parameters （mass, inertia, and length） and friction coefficients of the full-scale UE. Using experimental data from a full-scale field UE, the values of link parameters and the friction coefficient are identified. Some of the identified parameters are compared with measured physical values. Furthermore, the joint torques and positions computed by the proposed model using the identified parameters are validated against measured data. The comparison shows that both the Newton-Raphson method and the generalized Newton method are better in terms of prediction accuracy. The Newton-Raphson method is computationally efficient and has potential for real time application, but the generalized Newton method is slightly more robust to measurement noise. The experimental data were obtained in collaboration with QinetiQ Ltd.     

Simulation of Current Measurement Using Magnetic Sensor Arrays and Its Error Model

Magnetic sensor arrays are proposed to measure electric current in a non-contact way. In order to achieve higher accuracy, signal processing techniques for magnetic sensor arrays are utilized. Simulation techniques are necessary to study the factors influencing the accuracy of current measurement. This paper presents a simulation method to estimate the impact of sensing area and position of sensors on the accuracy of current measurement. Several error models are built up to support computer-aided design of magnetic sensor arrays.     

Logical Object as a Basis of Knowledge Based Systems

This paper presents a framework called logical knowledge object (LKO),which is taken as a basis of the dependable development of knowledge based systems(KBSs).LKO combines logic programming and object-oriented programming paradigms,where objects are viewed as abstractions with states,constraints,behaviors and inheritance.The operational semantics defined in the style of natural semantics is simple and clear.A hybrid knowledge representation amalgamating rule,frame,semantic network and blackboard is available for both most structured and flat knowledge.The management of knowledge bases has been formally specified.Accordingly,LKO is well suited for the formal representation of knowledge and requirements of KBSs.Based on the framework,verification techniques are also explored to enhance the analysis of requirement specifications and the validation of KBSs.In addition,LKO provides a methodology for the development of KBSs,applying the concepts of rapid prototyping and top-down design to deal with changing and incomplete requirements,and to provide multiple abstract models of the domain,where formal methods might be used at each abstract level.     

Parametric estimation of interconnected nonlinear systems described by input-output mathematical models

In this paper, two types of mathematical models are developed to describe the dynamics of large-scale nonlinear systems,which are composed of several interconnected nonlinear subsystems. Each subsystem can be described by an input-output nonlinear discrete-time mathematical model, with unknown, but constant or slowly time-varying parameters. Then, two recursive estimation methods are used to solve the parametric estimation problem for the considered class of the interconnected nonlinear systems. These methods are based on the recursive least squares techniques and the prediction error method. Convergence analysis is provided using the hyper-stability and positivity method and the differential equation approach. A numerical simulation example of the parametric estimation of a stochastic interconnected nonlinear hydraulic system is treated.     

Dominant Skyline Query Processing over Multiple Time Series

Multiple time series (MTS), which describes an object in multi-dimensions, is based on single time series and has been proved to be useful. In this paper, a new analytical method called α/β-Dominant-Skyline on MTS and a formal definition of the α/β-dominant skyline MTS are given. Also, three algorithms, called NL, BC and MFB, are proposed to address the α/β-dominant skyline queries over MTS. Finally experimental results on both synthetic and real data verify the correctness and e?ectiveness of the proposed method and algorithms.     

一种新颖的图像水印嵌入方法

An novel embedding method for image watermark based on wavelet transform is proposed. With this method ,the value of each pels is modified directly,so that a bit of watermark information is embedded in every pel-s. Before emeded,the original image is decomposed by wavelet transform,and then,a correlation mask for every imagepels is confirmed by the characteristic and tree structure ralation of the wavelet coefficients. At last, the modified val-ue of every pels is controlled by its corresponding mask for watermark information embedded. The experimental re-sults show that the embedded digital watermarks with this proposed method are invisible and robust enough againstthe commonly used image processing techniques.     

COMPUTER PATTERN DESIGN AND PAINTING TECHNIQUE BASED ON AESTHETICS KNOWLEDGE

Computer Art (CA) is a very important field in computer applications. Based on the analysisand summarization of the painting process, a new method of CA creation using the techniques of com-puter graphics and the expert system is presented in this paper. The reduction of pattern model, simu-lation of special effect, representation of aesthetics knowledge and fuzzy judgement of beauty are includ-ed by this new method.