In this paper, a new local matching algorithm, to estimate dense disparity map in stereo vision, consisting of two stages is presented. At the first stage, the reduction of search space is carried out with a high efficiency, i.e. remarkable decrease in the average number of candidates per pixel, with low computational cost and high assurance of retaining the correct answer. This outcome being due to the effective use of multiple radial windows, intensity information, and some usual and new constraints, in a reasonable manner, retains those candidates which satisfy more constraints and especially being more promising to satisfy the implied assumption in using support windows; i.e., the disparity consistency of the window pixels. Such an output from the first stage, while speeding up the final selection of disparity in the second stage due to search space reduction, is also promising a more accurate result due to having more reliable candidates. In the second stage, the weighted window, although not necessarily being the exclusive choice, is employed and examined. The experimental results on the standard stereo benchmarks for the developed algorithm are presented, confirming that the massive computations to obtain more precise matching costs in weighted window is reduced to about 1/11 and the final disparity map is also improved.

With the growth of wireless computing and the popularity of eXtensible Markup Language (XML), wireless XML data management is emerging as an important research area. In this paper, cache invalidation methodology with XML update is addressed in wireless computing environments. A family of XML cache invalidation strategies, called S-XIR, D-XIR and E-XIR, is suggested. Using S-XIR and D-XIR, the unchanged part of XML data, only its structure changes, can be effectively reused in client caching. E-XIR, which uses prefetching, can further improve access time. Simulations are carried out to evaluate the proposed methodology; they show that the proposed strategies improve both tuning time and access time significantly. In particular, the proposed strategies are on average about 4 to 12 times better than the previous approach in terms of tuning time.

In this paper, we propose a midpoint-validation method which improves the generalization of Support Vector Machine. The proposed method creates midpoint data, as well as a turning adjustment parameter of Support Vector Machine using midpoint data and previous training data. We compare its performance with the original Support Vector Machine, Multilayer Perceptron, Radial Basis Function Neural Network and also tested our proposed method on several benchmark problems. The results obtained from the simulation shows the effectiveness of the proposed method.

Today, TLS is widely used for achieving a secure communication system. And TLS is used PKI for server authentication and/or client authentication. However, its PKI environment, which is called as "multiple trust anchors environment," causes the problem that the verifier has to maintain huge number of CA certificates in the ubiquitous network because the increase of terminals connected to the network brings the increase of CAs. However, most of terminals in the ubiquitous network will not have enough memory to hold such huge number of CA certificates. Therefore, another PKI environment, "cross certification environment", is useful for the ubiquitous network. But, because current TLS is designed for the multiple trust anchors model, TLS cannot work efficiently on the cross-certification model. This paper proposes a TLS implementation method to support the cross certification model efficiently. Our proposal reduces the size of exchanged messages between the TLS client and the TLS server during the handshake process. Therefore, our proposal is suitable for implementing TLS in the terminals that do not have enough computing power and memory in ubiquitous network.

In mobile computing environments, cache invalidation techiniques are widely used. However, theses techniques require a large-sized invalidation report and show low cache utilization under high server update rate. In this paper, we propose a new cache-level cache invalidation technique called TTCI (Timestamp Tree-based Cache Invalidation technique) to overcome the above two problems. TTCI also supports selective tuning for a cache-level cache invalidation. We show in our experiment that our technique requires much smaller size of cache invalidation report and improves cache utilization.

Visual criteria for diagnosing liver diseases, such as cirrhosis, from ultrasound images can be assisted by computerized texture classification. This paper proposes a system applying a PNN (Pyramid Neural Network) for classifying the hepatic parenchymal diseases in ultrasonic B-scan texture. In this study, we propose a multifractal-dimensions method to select the patterns for the training set and the validation sets. A modified box-counting algorithm is used to calculate the dimensions of the B-scan images. FDWT (Fast Discrete Wavelet Transform) is applied for feature extraction during the preprocessing. The structure of the proposed neural network is testified by training and validation sets by cross-validation method. The performance of the proposed system and a system based on the conventional multilayer network architecture is compared. The results show that, compared with the conventional 3-layer neural network, the performance of the proposed pyramid neural network is improved by efficiently utilizing the lower layer of the neural network.

It has been a very important issue to evaluate the performance of transmission control protocol (TCP), and the importance is still growing up because TCP will be deployed more widely in future wireless as well as wireline networks. It is also the reason why there have been a lot of efforts to analyze TCP performance more accurately. Most of these works are focusing on overall TCP end-to-end throughput that is defined as the number of bytes transmitted for a given time period. Even though each TCP's fast recovery strategy should be considered in computation of the exact time period, it has not been considered sufficiently in the existing models. That is, for more detailed performance analysis of a TCP implementation, the fast recovery latency during which lost packets are retransmitted should be considered with its relevant strategy. In this paper, we extend the existing models in order to capture TCP's loss recovery behaviors in detail. On the basis of the model, the loss recovery latency of three TCP implementations can be derived with considering the number of retransmitted packets. In particular, the proposed model differentiates the loss recovery performance of TCP using selective acknowledgement (SACK) option from TCP NewReno. We also verify that the proposed model reflects the precise latency of each TCP's loss recovery by simulations.

This paper proposes an algorithm for detecting 3-way interactions. As far as the authors know, this is the first proposal ever made for a detection algorithm of 3-way interactions. In this paper, by analyzing examples, the mechanism of 3-way interactions is clarified and a detection algorithm of 3-way interactions is proposed. Namely the proposed detection algorithm is heuristic. To evaluate the algorithm, we implemented a detection system based on the proposed algorithm and applied it to 12 services, and 82 3-way interactions were detected. This shows the proposed algorithm is effective.

The traditional approach for establishing the correctness of group communication protocols is through rigorous arguments. While this is a valid approach, the likelihood of subtle errors in the design and implementation of such complex distributed protocols is not negligible. The use of formal verification methods has been widely advocated to instill confidence in the correctness of protocols. In this paper, we describe how we used the SPIN model checker to formally verify a group membership protocol that is part of an intrusion-tolerant group communication system. We describe how we successfully tackled the state-space explosion problem by determining the right abstraction level for formally specifying the protocol. The verification exercise not only formally showed that the protocol satisfies its correctness claims, but also provided information that will help us make the protocol more efficient without violating correctness.

Software certification is a notoriously difficult problem. From software reliability engineering perspective, certification process must provide evidence that the program meets or exceeds the required level of reliability. When certifying the reliability of a high assurance system very few, if any, failures are observed by testing. In statistical estimation theory the probability of an event is estimated by determining the proportion of the times it occurs in a fixed number of trials. In absence of failures, the number of required certification tests becomes impractically large. We suggest that subjective reliability estimation from the development lifecycle, based on observed behavior or the reflection of one's belief in the system quality, be included in certification. In statistical terms, we hypothesize that a system failure occurs with the hypothesized probability. Presumed reliability needs to be corroborated by statistical testing during the reliability certification phase. As evidence relevant to the hypothesis increases, we change the degree of belief in the hypothesis. Depending on the corroboration evidence, the system is either certified or rejected. The advantage of the proposed theory is an economically acceptable number of required system certification tests, even for high assurance systems so far considered impossible to certify.

In this paper, we describe the development and the analysis of the Label Distribution Protocol (LDP) for Multiprotocol Label Switching System. We review the implementation issues that are required to construct the LDP for a gigabit switched router and propose a detailed design of the LDP. We present the detailed design using the Deviation Tree of the protocol state machine and a formal specification of the state machine using the process algebra. These specifications are based on the IETF standard. By analyzing the protocol behaviors of the Deviation Trees and the formal specification, we prove the interoperability, completeness, liveness, reachability, and the safety of the implemented LDP. We expect that the reliability would be improved using these analyses. With these proofs we expect the implemented LDP will be interoperable with other commercialized products. As a result we validate the protocol behaviors of the implemented LDP.

Caching of frequently accessed data has been shown to be a useful technique for reducing congestion on the narrow bandwidth of wireless channels. However, traditional client/server strategies for supporting transactional cache consistency, which require extensive communications between a client and a server, are not appropriate in a wireless mobile database. This paper proposes two, simple but effective, transactional cache consistency protocols for mobile read-only transactions by utilizing the broadcast-based solutions for the problem of invalidating caches. The novelty of our approach is that the consistency check on accessed data and the commitment protocol are implemented in a truly distributed fashion as an integral part of cache invalidation process. The applicability of proposed techniques is also examined by an analytical study.

The stateless-based cache invalidation schemes for wireless environments can be categorized into either asynchronous or synchronous cache invalidation according to the broadcasting way of invalidation report. However, if the asynchronous cache invalidation scheme attempts to support local processing of read-only transaction, a critical problem may occur; the asynchronous invalidation reports provide no guarantee of waiting time for mobile transactions requesting commit. To solve this problem, the server in our approaches broadcasts two kind of messages, asynchronous invalidation report to reduce transaction latency and periodic guide message to avoid the uncertainty of waiting time for the next invalidation report. This paper presents a simulation-based analysis on the performance of the suggesting algorithms. The simulation experiments show that the local processing algorithms of read-only transaction based on asynchronous cache invalidation scheme get better response time than the algorithm based on synchronous cache invalidation scheme.

This paper presents a fast inversion method for electromagnetic imaging of cylindrical dielectric objects with the optimal regularization parameter used in the Levenberg-Marquardt method. A novel procedure for choosing the optimal regularization parameter is proposed. The method of moments with pulse-basis functions and point matching is applied to discretize the equations for the scattered electric field and the total electric field inside the object. Then the inverse scattering problem is reduced to solving the matrix equation for the unknown expansion coefficients of a contrast function, which is represented as a function of the relative permittivity of the object. The matrix equation may be solved in the least-squares sense with the Levenberg-Marquardt method. Thus the contrast function can be reconstructed by the minimization of a functional, which is expressed as the sum of a standard error term on the scattered electric field and an additional regularization term. While a regularization parameter is usually chosen according to the generalized cross-validation (GCV) method, the optimal one is now determined by minimizing the absolute value of the radius of curvature of the GCV function. This scheme is quite different from the GCV method. Numerical results are presented for a circular cylinder and a stratified circular cylinder consisting of two concentric homogeneous layers. The convergence behaviors of the proposed method and the GCV method are compared with each other. It is confirmed from the numerical results that the proposed method provides successful reconstructions with the property of much faster convergence than the conventional GCV method.

This paper presents a system-level bus architecture validation technique and shows its application to a consumer product design. This technique enables the entire system to be validated with bus cycle accuracy using bus architecture level models derived from their corresponding behavioral level models. Experimental results from a digital still camera (DSC) system design show that our approach offers much faster simulation speed than register transfer level (RTL) simulators. Using this fast and accurate validation technique, bus architecture designs, validations and optimizations can be effectively carried out at system-level and total turn around time of system designs can be reduced dramatically.

This paper presents a method of calculating an interval including a bifurcation point. Turning points, simple bifurcation points, symmetry breaking bifurcation points and hysteresis points are calculated with guaranteed accuracy by the extended systems for them and by the Krawczyk-based interval validation method. Taking several examples, the results of validation are also presented.

A new concept of "an imperfect singular solution" is defined as an approximate solution which becomes a singular solution by adding a suitable small perturbation to the original equations. A numerical method is presented for proving the existence of imperfect singular solutions of nonlinear equations with guaranteed accuracy. A few numerical examples are also presented for illustration.

Page-based DSM systems suffer from false sharing since they use a large page as a coherence unit. The optimal page size is dynamically affected by application characteristics. Therefore, a fixed-size page cannot satisfy various applications even if it is small as a cache line size. In this paper we present a software-only coherence protocol called BCP (Buddy Coherence Protocol) to support multiple page sizes that vary adaptively according to the behavior of each application during run time. In BCP, the address of a remote access and the address of the most recent local access is compared. If they are to the different halves of a page, BCP considers it as false sharing and demotes the page to two subpages of equal size. If two contiguous pages belong to the same node, BCP promotes two pages to a superpage to reduce the number of the following coherence activities. We also suggest a mechanism to detect data sharing patterns to optimize the protocol. It detects and keeps the sharing pattern for each page by a state transition mechanism. By referring to those patterns, BCP selectively demotes the page and increases the effectiveness of a demotion. Self-invalidation of the migratorily shared page is also employed to reduce the number of invalidations. Our simulations show that the optimized BCP outperforms almost all the best cases of the write-invalidate protocols using fixed-size pages. BCP improves performance by 42.2% for some applications when compared against the case of the fixed-size page.

In a distributed concurrent system such as a computer communication network, the system components communicate with each other via communication links in order to accomplish a desired distributed application. If the links are dynamically established among the components, the system configuration as well as its behavior becomes complex. In this paper, we give formal specification of such a dynamically reconfigurable system in which the components are modeled by communicating finite state machines executed concurrently with the communication links which are dynamically established and disconnected. We also present an algorithm to validate the safety and link-related properties in the specified behavior. Finally, we design and implement a simulator and a validator that enables execution and validation of the given specification, respectively.

Requirements engineering refers to activities of gathering and organizing customer requirements and system specifications, making explicit representations of them, and making sure that they are valid and accounted for during the course of the design lifecycle of software. One very popular software development practice is the incremental development practice. The incremental development refers to practices that allow a program, or similarly specifications, to be developed, validated, and delivered in stages. The incremental practice is characterized by its depth-first process where focuses are given to small parts of the system in sequence to fair amounts of detail. In this paper, we present a development and validation of specifications in such an incremental style using a tool called ASADAL, a comprehensive CASE tool for real-time systems. ASADAL supports incremental and hierarchical refinements of specifications using multiple representational constructs and the evolving incomplete specifications can be formally tested with respect to critical real time properties or be simulated to determine whether the specifications capture the intended system behavior. In particular, we highlight features of ASADAL's specification simulator, called ASADAL/SIM, that plays a critical role in the incremental validation and helps users gain insights into the validity of evolving specifications. Such features include the multiple and mixed level simulation, real-value simulation, presentation and analysis of simulation data, and variety of flexible simulation control schemes. We illustrate the overall process using an example of an incremental specification development of an elevator control system.