Scientia Iranica
Volume:25 Issue: 6, Nov - Dec 2018

So far, valuable researches have been conducted on mapping object-oriented specification notations, such as Object-Z, to different object-oriented programming languages, such as C++. However, the results of selecting JVM-based programming languages for mapping have not covered most of basic Object-Z structures. In this paper, the Groovy language, as a dynamic JVM-based language, is selected to overcome some of the existing limitations. As the main contribution, the rules required for mapping Object-Z specifications to executable Groovy code are introduced. The proposed rules cover notions such as multiple inheritance, inverse specification of functions, functions defined on generic definitions, and free type constructors. These notions have not been covered in previous methods for formal program development from object-oriented specifications, regardless of the selected formal specification language and target programming language. In addition, in this paper, the parallel composition construct is mapped to a parallel, executable code to improve the faithfulness of the final code to the initial specification. We also introduce a mapping rule for the class union construct, which has not yet been provided for any JVM-based language. Unlike previous works, instead of presenting the mapping rules in terms of natural languages, we present them in terms of some formal mapping rules.

Lattice-based cryptography has received significant attention from security practitioners in the past decade. It exhibits attractive properties, including being a major post-quantum cryptography candidate, enjoying worst-case to average-case security reductions, and being supported by efficient implementations. In this paper, we propose three practical lattice-based authenticated encryption (AE) schemes. These schemes are provably secure assuming hardness of basic lattice problems. The proposed schemes have remarkable motivationsand advantages over widely-used AEs as follows. These schemes are alternatives to current conventional and post-quantum AE schemes in the post-quantum era. Moreover, composing the proposed AEs with a lattice-based asymmetric key distribution scheme results to a hybrid encryption which depends only on one (type of) security assumption. The implementation of such hybrid encryption can make use of specific optimizations regarding, e.g., code size in software, and gate equivalent or FPGA area usage in hardware. That is because the symmetric and asymmetric algorithms have some common primitive computations. To evaluate the performance of the proposed AEs, we implement them on current Intel CPUs and benchmark them to encrypt messages of various sizes. The most efficient proposed scheme is only 12% slower than AES-256-GCM for 40-byte messages on Sandy Bridge, and 34% faster for 1500-byte messages.

Micro/Nano fluidic biochips are used to automate the clinical diagnosis, DNA sequencing, automated drug discovery and real time bio-molecular recognition. One of attractive usages of biochips is Lab-on-chip (LOC). Lab-on-Chip technology is a promising replacement for biomedical and chemical apparatus. Two main types of micro fluidic based biochips are used: continuous-flow based and digital micro fluidic biochips (DMFB). In DMFBs, liquids, in the form of droplets, are controlled independently and concurrently over a two dimensional array of cells (or electrodes).Digital micro fluidic biochips provide high ability to congure and fault tolerance.
In this paper, a new architecture for DMFB with purpose of balancing among the parameters of flexibility, efficiency, cost, and completion time of biological experiments, is presented. In the new architecture, a FPGA-based structure is used, which increase flexibility and paralellizing assay operations. Experiments show that, the execution time of scheduling, routing, and simulation are improved in comparison with FPPC architecture about 2.54%, 18.76% and 12.52%, respectively in cost of 21% overhead in the number of controlling pins.

Let G be a weighted digraph and s and t be two vertices of G. The reachability assurance (RA) problem is how to label the edges of G such that every path starting at s finally reaches t and the sum of the weights of the labeled edges, called the RA cost, is minimal. The common approach to the RA problem is pathfinding, in which a path is sought from s to t and then the edges of the path are labeled. This paper introduces a new approach, the marking problem (MP), to the RA problem. Compared to the common pathfinding approach, the proposed MP approach has a lower RA cost. It is shown that the MP is NP-complete, even when the underlying digraph is an unweighted directed acyclic graph (DAG) or a weighted DAG with an out-degree of two. An appropriate heuristic algorithm to solve the MP in polynomial time is provided. To mitigate the RA problem as a serious challenge in this area, application of the MP in software testing is also presented. By evaluating the datasets from various program flow graphs, it is shown that the MP is superior to the pathfinding in the context of test case generation.

In this work, a new realization topology of the low-voltage ultra-low-power quadrature oscillator is presented. This quadrature oscillator utilizes only two active elements, namely differential voltage current conveyor (DVCC), and five passive ones, all of them are grounded, which is recommended for the integrated circuit implementation. The DVCC is based on quasi-floating-gate MOS transistor, which is a distinct technique from the conventional one, featuring with operation at low-voltage and ultra-low-power conditions; hence the proposed DVCC works with low supply voltage of ± 400 mV and consumes power of merely 6.6 µW. Thanks to these features the total power dissipation of the oscillator is only 0.28 mW. The simulation results using 0.18 µm TSMC CMOS technology are included in order to prove the design correctness.

Symbiotic Organisms Search (SOS) is a brand new and effective metaheuristic optimization algorithm. This paper proposes the SOS algorithm to solve the Economic Load Dispatch (ELD) problem with valve-point effect, which is one of the essential optimization problems in modern power systems. The proposed algorithm is tested on five different test cases consisting 3-machines 6-bus, IEEE 5-machines 14-bus, IEEE 6-machines 30-bus, 13 and 40 unit test systems including both transmission loss and without transmission loss. These test cases show that SOS is able to converge to the global optima successfully. Moreover results obtained from proposed algorithm are compared through different methods used in solving the ELD problem existing in the literature. According to these results, SOS produces better values than all.

Hyperthermia utilizing nanoparticles is a novel cancer therapy which relies on the heat released when nanoparticles inside a tumor are exposed to an alternating magnetic field. The field strength and frequency are the main variants affect performance of nanoparticles for heat generation. Besides the characteristics of nanoparticle, which is the main criteria for tuning amplitude and frequency of magnetic field generated by an alternating magnetic field generator (AMFG), several parameters should be considered for an optimum design, which is related to AMFG design. These parameters are input voltage range, copper tube resistance used for solenoid coil, coil number of turns, and etc. According to these criteria, design procedure of AMFG for research applications is performed to maximize the heat released by nanoparticles. In order to validate the design, an experimental set up of AMFG is prepared which is used for in vivo hyperthermia tests. The experimental results are shown and compared to the simulations.

This paper is concerned with the estimation of state trajectory of linear discrete time dynamic systems subject to parametric uncertainty over the compound erasure channel that uses feedback channel intermittently. For this combined system and channel, using the data processing inequality and a robust version of the Shannon lower bound, a necessary condition on channel capacity for estimation of state trajectory at the receiver giving almost sure asymptotically zero estimation error is presented. Then, an estimation technique over the compound erasure channel that includes an encoder, decoder and a sucient condition under which the estimation error at the receiver is asymptotically zero almost surely is presented. This leads to the conclusion that over the compound erasure channel, a condition on Shannon capacity in terms of the rate of expansion of the Shannon entropy is a necessary and sucient condition for estimation with uniform almost sure asymptotically zero estimation error. The satisfactory performance of the proposed technique is illustrated using simulation.

In this article we will control the energy storage inertial noted inertial energy storage system to partner with a wind energy conversion system that aims to improve the power quality transit network. Inertial storage is considered a flywheel coupled to an induction motor and controlled by a voltage inverter type power converter. First step, a model of inertial energy storage system (flywheel + asynchronous machine) is presented, then two control methods are proposed: the direct torque control (DTC and DTC-conventional SVPWM) (space vector pulse with modulation). The two control methods give similar performance, but the DTC-SVPWM requires less computation time. The two regulators and the proportional integrator SVPWM technique were used to determine the switching frequency. Using direct control with vector modulation strategy has enabled the inertial energy storage system of demonstrating good continuation even under rather severe operating conditions, and the torque ripples are significantly reduced compared to the case of conventional DTC. Then we come to the presentation of simulation results obtained.

Sunlight sensing for maximum illumination, providing initial position and delays of PV panel, design of an adequate control unit for minimal consuming servo motors are the main challenges of solar tracking systems. That is the objective of this paper to design and implement an automatic control for directing maximum solar illumination to a photovoltaic (PV) panel. The proposed prototype dual axis solar tracker panel is used to optimize the conversion of solar energy into electricity by orienting the panel toward the real position of the sun, at a cost of mechanical complexity and maintenance need, for the best efficiency. In hardware development, two geared DC servo motors are pulse width modulation (PWM) controlled by a drive unit moving the panel using four light dependant resistors (LDR) to provide analog signals processed by a simple and low energy ATMEGA328P microcontroller with Arduino. For the software part, after data processing, a C++ programming controls two DC servo motors to position light sensors in the most favorable direction, where solar panel and sensors will be perpendicular to the sunlight

This paper presents a novel algorithm based on phasor measurements to online estimation of power system Thévenin Equivalent (TE) from a generator terminal. Three consecutive phasor measurements of generator terminal voltage and current are used to estimate the system TE. In a real network, system frequency deviation from its nominal value will produce some phase drift in consecutive phasors reported by Phasor Measurements Units (PMUs). To correct the phase drift and synchronizing the reported phasors to the same reference, an improved triangulation method is developed. The improved method uses a virtual vector in its structure. Using this vector alleviates the negative impacts of improper data resulting from noise or disturbances which make the simple triangulation method to be useless. The algorithm is tested on standard NE-39 network and is implemented in Shahid Beheshti University (SBU) protection laboratory to verify the results in a practical area. The obtained results show that the new method can efficiently estimate the in online mode in steady-state and transient conditions.

This paper provides generation companies (GENCOs) with a novel decision-making tool that accounts for both long term and short term risk aversion preferences and devises optimal strategies to participate in energy, ancillary services markets and forward contracts where possibility of involvement in arbitrage opportunities is also considered. Because of the imprecise nature of the decision maker’s judgment, appropriate modelling of risk aversion attitude of the GENCO is another challenge. This paper uses fuzzy satisfaction theory to express decision maker’s attitude toward risk. Conditional value at risk methodology (CVaR) is utilized as the measure of risk and uncertainty sources include prices for the day-ahead energy market, automatic generation control (AGC) and reserve markets. By applying the proposed method, not only trading loss over the whole scheduling horizon can be controlled, but also the amount of imposed loss during every time period can be reduced. An illustrative case study is provided for further analysis.

In this work, we investigate the influence of the second order-(2OD) and third order-(3OD) dispersion terms on chirp signal generation and transmission through RF photonic link without optical filter. Dispersion equations are formalised using Taylor series and Bessel function to study the link performance. Our result (Eye diagrams) shows that the 2OD+3OD have significant impact on chirp mm-wave propagating through fiber of different lengths. In this paper chirp mm signal is controlled at photo detector by individual phase term of external modulators. Moreover, we also demonstrated experimentally that the chirp rate can be significantly controlled by properly choosing the type of fiber in the experiments. We discussed the RF photonic link performance in terms of Optical Sideband Suppression Ratio (OPSSR), Radio Frequency Spurious Suppression Ratio (RFSSR), Bit Error Rate (BER). Theoretical results are verified using MATLAB Software.

In this paper, we intend to improve the CPG network presented by Pinto et al. based on 4-cell model for bipedal locomotion systems. This model is composed of four coupled identical cells which internal dynamics of each one is described by the Morris-Lecar nonlinear differential equation and the couplings between the cells follow the synaptic type. We exploit an elitist non-dominated sorting genetic algorithm (NSGA II) to find the best set of coupling weights by which the phase differences become optimally close to the ones required for a primary bipedal gait. Thus, we achieve the rhythmic signals associated with four primary bipedal gaits of walk, run, two-legged jump, and two-legged hop. Also, we successfully obtain all secondary gaits corresponding to the bipedal locomotion identified by Pinto et al. from the 4-cell model, by symmetry breaking bifurcations of primary gaits. Particularly, we are able to produce the secondary gait called “hesitation walk” through transition from primary gaits of run and two-legged jump.

This paper presents an optimal approach to design Fractional-Order Digital Integrators (FODIs) using a metaheuristic technique, called Hybrid Flower Pollination Algorithm (HFPA). HFPA is a hybrid approach which combines the exploitation and exploration capabilities of two dierent evolutionary optimization algorithms, namely, Particle Swarm Optimization (PSO) and Flower Pollination Algorithm (FPA). The proposed HFPA based designs are compared with the designs based on Real Coded Genetic Algorithm (RGA), PSO, Dierential Evolution (DE), and FPA. Simulation results demonstrate that HFPA based FODIs of all the dierent orders consistently achieve the best magnitude responses. The proposed technique yields FODIs which surpass all the designs based on both classical and evolutionary optimization approaches reported in recent literature.

This paper proposes a low-computational Bayesian algorithm for noisy sparse recovery in the context of one bit compressed sensing with sensing matrix perturbation. The proposed algorithm which is called BHT-MLE comprises a sparse support detector and an amplitude estimator. The support detector utilizes Bayesian hypothesis test, while the amplitude estimator uses an ML estimator which is obtained by solving a convex optimization problem. Simulation results show that Bayesian hypothesis testing in combination with the ML estimator has more reconstruction accuracy than that of only an ML estimator and also has less computational complexity.