Symbolic Model Checking of Interactions in Sequence Diagrams with Combined Fragments by SMV

In this paper, we proposed a method for detecting consistency violation between state machine diagrams and a sequence diagram defined in UML 2.0 using SMV. We extended a method expressing these diagrams defined in UML 1.0 with boolean formulas so that it can express a sequence diagram with combined fragments introduced in UML 2.0. This extension made it possible to represent three types of combined fragment: alternative, option and parallel. As a result of experiment, we confirmed that the proposed method could detect consistency violation correctly with SMV.

Performance Analysis of Software Reliability Models using Matrix Method

This paper presents a computational methodology based on matrix operations for a computer based solution to the problem of performance analysis of software reliability models (SRMs). A set of seven comparison criteria have been formulated to rank various non-homogenous Poisson process software reliability models proposed during the past 30 years to estimate software reliability measures such as the number of remaining faults, software failure rate, and software reliability. Selection of optimal SRM for use in a particular case has been an area of interest for researchers in the field of software reliability. Tools and techniques for software reliability model selection found in the literature cannot be used with high level of confidence as they use a limited number of model selection criteria. A real data set of middle size software project from published papers has been used for demonstration of matrix method. The result of this study will be a ranking of SRMs based on the Permanent value of the criteria matrix formed for each model based on the comparison criteria. The software reliability model with highest value of the Permanent is ranked at number – 1 and so on.

Specifying a Timestamp-based Protocol For Multi-step Transactions Using LTL

Most of the concurrent transactional protocols consider serializability as a correctness criterion of the transactions execution. Usually, the proof of the serializability relies on mathematical proofs for a fixed finite number of transactions. In this paper, we introduce a protocol to deal with an infinite number of transactions which are iterated infinitely often. We specify serializability of the transactions and the protocol using a specification language based on temporal logics. It is worthwhile using temporal logics such as LTL (Lineartime Temporal Logic) to specify transactions, to gain full automatic verification by using model checkers.

Neural Network Based Predictive DTC Algorithm for Induction Motors

In this paper, a Neural Network based predictive DTC algorithm is proposed .This approach is used as an alternative to classical approaches .An appropriate riate Feed - forward network is chosen and based on its value of derivative electromagnetic torque ; optimal stator voltage vector is determined to be applied to the induction motor (by inverter). Moreover, an appropriate torque and flux observer is proposed.

Usage-based Traffic Control for P2P Content Delivery

Recently, content delivery services have grown rapidly over the Internet. For ASPs (Application Service Provider) providing content delivery services, P2P architecture is beneficial to reduce outgoing traffic from content servers. On the other hand, ISPs are suffering from the increase in P2P traffic. The P2P traffic is unnecessarily redundant because the same content or the same fractions of content are transferred through an inter-ISP link several times. Subscriber ISPs have to pay a transit fee to upstream ISPs based on the volume of inter-ISP traffic. In order to solve such problems, several works have been done for the purpose of P2P traffic reduction. However, these existing works cannot control the traffic volume of a certain link. In order to solve such an ISP-s operational requirement, we propose a method to control traffic volume for a link within a preconfigured upper bound value. We evaluated that the proposed method works well by conducting a simulation on a 1,000-user scale. We confirm that the traffic volume could be controlled at a lower level than the upper bound for all evaluated conditions. Moreover, our method could control the traffic volume at 98.95% link usage against the target value.

Average Current Estimation Technique for Reliability Analysis of Multiple Semiconductor Interconnects

Average current analysis checking the impact of current flow is very important to guarantee the reliability of semiconductor systems. As semiconductor process technologies improve, the coupling capacitance often become bigger than self capacitances. In this paper, we propose an analytic technique for analyzing average current on interconnects in multi-conductor structures. The proposed technique has shown to yield the acceptable errors compared to HSPICE results while providing computational efficiency.

Evaluation of Service Continuity in a Self-organizing IMS

The NGN (Next Generation Network), which can provide advanced multimedia services over an all-IP based network, has been the subject of much attention for years. While there have been tremendous efforts to develop its architecture and protocols, especially for IMS, which is a key technology of the NGN, it is far from being widely deployed. However, efforts to create an advanced signaling infrastructure realizing many requirements have resulted in a large number of functional components and interactions between those components. Thus, the carriers are trying to explore effective ways to deploy IMS while offering value-added services. As one such approach, we have proposed a self-organizing IMS. A self-organizing IMS enables IMS functional components and corresponding physical nodes to adapt dynamically and automatically based on situation such as network load and available system resources while continuing IMS operation. To realize this, service continuity for users is an important requirement when a reconfiguration occurs during operation. In this paper, we propose a mechanism that will provide service continuity to users and focus on the implementation and describe performance evaluation in terms of number of control signaling and processing time during reconfiguration