Scientia Iranica
Volume:22 Issue: 3, 2015

Due to the popularity of object-oriented programming approaches, there is a growing interest in utilizing object-oriented concepts, such as encapsulation and reuse, when applying formal methods. The main contribution of this paper is to review and compare existing formal methods to develop object-oriented programs from formal speci cations. The secondary contribution is providing a comparison between widely used object-oriented formal speci cation languages. The results of this paper can be utilized by researchers wishing to know what open problems are outstanding in the areas of formal, objectoriented speci cation and program development. Our ndings are also useful for those who are looking for proper speci cation languages and program development methods to specify and develop object-oriented programs formally. In addition, the provided criteria are suitable for evaluating numerous object-oriented formal speci cation languages that are under development, either by extending existing formal approaches or formalizing informal OO-methods. As one consequence of this work, it can be mentioned that among formal speci cation languages, OZ and VDM++ support OO concepts more strongly in comparison to VDM++ and UML-B. Program development methods based on OZ have less tool support. Finally, most proposed methods for formal, object-oriented program development have been evaluated using only case studies, rather than employing formal approaches.

Software Performance Engineering (SPE) evaluates the key performance factors such as response time and utilization in the entire life cycle of software development. One of the important issue of software performance is bottlenecks that is not investigated more till now in the process of SPE. Meanwhile, Bottleneck detection and mitigation in software modeling stage is quality-centered and cost effective. Layered bottleneck is a type of bottleneck that occurs in systems with layered services and affects its utilization more than flat bottlenecks. Presented approach in this paper has selected Layered Queening Network (LQN) as an appropriate performance model to present and analyze the layered bottlenecks. The process of SPE from software model to performance model has been automatically implemented. Also, an optimization stage is added to find the best specification of software model in a way that strength of the bottleneck, response time and cost will be minimized. To assess the proposed solution two recently proposed multi-objective gravitational search algorithms are employed. To evaluate the effectiveness of the applied algorithms, two well-known multi-objective algorithms: NSGA-II and MOPSO are also applied for a case study and a comprehensive comparison is presented.

Tremendous broadcast soccer videos demand automatic semantic representation for event and tactic analysis. Player tracking is an important step which can be further processed and analyzed by sport experts to evaluate player or team performance. A novel scheme for player tracking in soccer broadcast videos is proposed in this research. Following player detection using Adaboost, player labeling, occlusion handling and mosaic construction, player tracking is formulated as an optimization problem allowing us to extract player trajectories using Particle Swarm Optimization (PSO). PSO is an optimization method inspired by the flocking behavior of birds which was originally customized for continuous function value optimization. In this paper, a new application of discrete particle swarm optimization for player tracking in soccer videos is proposed. Updating equations for particle swarm optimization algorithm are modified based on problem characteristics and discrete variables to extract player trajectory. Experimental results show that the modified PSO is promising in solving soccer player tracking problem.

Increasing the Constant Power Speed Range (CPSR) and economical design are the main concern for designers. In this paper a new optimal design of the interior permanent magnetic motor for traction application is proposed. The magnet volume has been minimized and CPSR has been wide enough for traction applications. The new idea of this paper is combination of the PM segmented and using nonconventional air bridges in one design. The optimization process has been done using Genetic algorithm (GA). Verification of simulation results has been done using Finite Element Method (FEM)

In this paper, solution of systems of delay di erential equations, with initial conditions, using numerical methods, including the Taylor collocation method, the Lambert W function and the variational iteration method, is considered. We have endeavored to show the most appropriate method by comparing the solutions of this system of equations with di erent types of methods. All numerical computations have been performed on the computer algebraic system, Matlab.

The acoustic signal is an important medium in communication, damage and leakage detecting, etc. They are also used in the wireless sensor network positioning in recent years. With the development of mobile communication technology, smartphone-based indoor positioning by acoustic signals becomes possible. In the indoor environment, however, acoustic signals will be interfered with by environmental noise and multipath effect. Moreover, when multiple users are positioning simultaneously, acoustic signals will interfere with each other. In order to eliminate various forms of interference, we design a robust acoustic signal for smartphone-based indoor positioning in this paper. The signal is generated by using the pseudo-random codes, Gold sequences to modulate 6 kHz cosine wave. It is detected through its auto-correlation properties in the receiver. The designed acoustic signal can resist various noises with its excellent cross-correlation characteristic. We conduct experiments on real smartphones and the results show the signals can work well in the presence of forms of interference.

In this paper, a new voltage-mode (VM) first-order all-pass filter (APF) topology composed of only a grounded capacitor is proposed. The proposed APF uses a single minus-type second-generation current conveyor (CCII-) which can be constructed by only five MOS transistors. It has low power consumption. Resonance frequency of the proposed APF can be adjusted by changing only a resistor value. However, it needs a single matching condition. As an application, a quadrature oscillator example is given. A non-ideality analysis for the proposed APF is also given. A number of time domain and frequency domain simulation results and an experimental test result are included to confirm the theory.

This paper proposes an analysis on the calculation of voltage and current ripples, voltage stresses, switching device power, and switching loss in Z-source inverter.In this paper, the formulas of the inductor current ripple, capacitor voltage ripple, voltage stress on the devices and capacitors, switching device power, and switching loss are presented. Actually, computing these formulas will help us a lot in the performance improvement of Z-source inverter. A detailed analysis on the main formulas of Z-source inverter is presented in this paper. Simulation results are also given to confirm the analysis

Automatic road extraction from satellite images is one of the most important areas of research in the eld of remote sensing. The method proposed in this study is based on a fuzzy method for the detection of road areas from high resolution SAR images. In this method, the multiple features are extracted rst, using the backscatter coecients of each pixel and its neighboring pixels. The extracted features are combined with each other in the next step using a fuzzy algorithm, and, nally, the desired road areas are selected separately considering spatial and spectral criteria. The proposed algorithm is tested on di erent scenes of TerraSAR-X images. Experimental results reveal that the proposed method is e ective.

This paper is devoted to solve transmission expansion planning (TEP) problems, via a constructive heuristic algorithm (CHA) that can be employed as a sub-routine in a meta-heuristic procedure. In such a strategic methodology, CHA may improve the quality of trial solutions that speed up the convergence of the main algorithm. By introducing a “territory concept” for each derived local optimum, this paper proposes an approach, forcing CHA sub-procedures to explore new areas in the problem sub-space. Such modification is enforced to Villasana-Garver-Salon (VGS) algorithm, as a well-known kind of CHA, to improve its performance. The improved VGS is called territory-based VGS (TBVGS). In order to evaluate the performance of TBVGS, it is implemented on a meta-heuristic algorithm in which the performance of the obtained meta-heuristic algorithm is examined with different standard test systems as well as practical cases. Simulation studies and results analysis show a promising improvement caused in computational efficiency of the algorithm and even more important, finding a higher quality set of TEP local optimums.