2020-12-05T10:06:47Z
http://scientiairanica.sharif.edu/?_action=export&rf=summon&issue=1062
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
From Object-Z Specification to Groovy Implementation
Farzin
Zaker
Hassan
Haghighi
Eslam
Nazemi
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.
Formal program development
Object oriented programming
Animation
Object-Z
Groovy
JVM
2018
12
01
3415
3441
http://scientiairanica.sharif.edu/article_20798_085d4c579555c471e8ddeebb4ea714e5.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Practical Provably-Secure Authenticated Encryption Schemes Using Lattice-based Pseudorandom Function SPRING
Ahmad
Boorghany
Siavash
Bayat-Sarmadi
Rasool
Jalili
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.
Authenticated Encryption
Lattice-based Cryptography
Post-quantum Cryptography
Provable Security
2018
12
01
3442
3460
http://scientiairanica.sharif.edu/article_21044_0bae5fe2e12764b95354633886c6d2cd.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Massive Parallel Digital Micro fluidic Biochip Architecture for Automating Large-Scale Biochemistry Assays
Abbas
Haddad
Maryam
Taajobian
Ali
Jahanian
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 congure 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 showthat, 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.
Micro fluidic Biochip
Physical Design
Architecture
2018
12
01
3461
3474
http://scientiairanica.sharif.edu/article_20797_f021dcd3ec742f9b3a41de1b03b7f153.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Corrigendum to: “Making problem: A new approach to reachability assurance in digraphs”[Scientia Iranica 25(3) (2018) 1441-1455]
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.
Marking problem
Reachability assurance
Pathfinding
Software testing
2018
12
01
3475
3475
http://scientiairanica.sharif.edu/article_21196_77cdd0fb250541c1ed0e50a2613335e7.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Quadrature oscillator based on novel low-voltage ultra-low-power quasi-floating-gate DVCC
Fabian
KHATEB
Nabhan
KHATIB
Jaroslav
KOTON
Norbert
HERENCSAR
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.
Quadrature oscillator
Quasi-floating-gate MOST
Low-voltage ultra-low-power analog circuit design
DVCC
2018
12
01
3477
3489
http://scientiairanica.sharif.edu/article_4377_c0dc127568ca2f503274199d5047e4ee.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Symbiotic Organisms Search algorithm for economic load dispatch problem with valve-point effect
Ugur
Guvenc
Serhat
Duman
Yusuf
Sonmez
H.
Tolga Kahraman
M.
Kenan Dosoglu
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.
Symbiotic Organisms Search
Economic Load Dispatch
power systems
optimization
2018
12
01
3490
3506
http://scientiairanica.sharif.edu/article_4378_04a36b9110cf7586942e28772a78fb8e.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Design of Alternating Magnetic Field Generator for Magnetic Fluid Hyperthermia Research Application
Mahdi
Mohseni
Amirhossein
Rajaei
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.
AC magnetic field
hyperthermia
resonant converter
magnetic nanoparticles
solenoid coil
2018
12
01
3507
3516
http://scientiairanica.sharif.edu/article_4380_b08f840230e86740f06f69de07e6d2c3.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Shannon Entropy And Tracking Dynamic Systems Over Noisy Channels
Alireza
Farhadi
This paper is concerned with the estimation of state trajectory of linear discrete timedynamic systems subject to parametric uncertainty over the compound erasure channelthat 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 thereceiver 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 receiveris asymptotically zero almost surely is presented. This leads to the conclusion thatover the compound erasure channel, a condition on Shannon capacity in terms ofthe rate of expansion of the Shannon entropy is a necessary and sucient conditionfor estimation with uniform almost sure asymptotically zero estimation error. Thesatisfactory performance of the proposed technique is illustrated using simulation.
Estimation
Networked control system
Shannon entropy
2018
12
01
3517
3531
http://scientiairanica.sharif.edu/article_4375_275fd393b37d7911832fe4900437f3ff.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
DTC-SVPWM of an Energy Storage Flywheel Associated with a Wind Turbine Based on the DFIM
Abdelhafidh
Moualdia
Ahmed
Medjber
A.
Kouzou
O.
Bouchhida
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.
Asynchronous machine
energy storage
Wind Turbine
DTC-SPWM
direct torque control
wind energy conversion
2018
12
01
3532
3541
http://scientiairanica.sharif.edu/article_4379_84b52685e5fad89c255b0f3f95530161.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Design of prototype dual axis tracker solar panel controlled by geared dc servo motors
A.
Mansouri
F.
Krim
Z.
Khouni
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
Arduino uno
dual axis
light dependant resistor
low cost solar tracker PWM control
2018
12
01
3542
3558
http://scientiairanica.sharif.edu/article_20045_9cc703fa700a58988a562b278cce9555.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Power System Thévenin Equivalent Estimation Based on Phasor Measurements
Bahman
Alinejad Osbouei
Hossein
Kazemi Karegar
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.
Thévenin equivalent
Phasor Measurement Units (PMU)
Triangulation method
Phase drift
Slip frequency
2018
12
01
3559
3568
http://scientiairanica.sharif.edu/article_4373_7bebdd06b0cdd78d655a8a4100f0d652.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Portfolio Optimization in Electricity Market Using a Novel Risk Based Decision Making Approach
Somayyeh
Bazmohammadi
Asghar
Akbari Foroud
Najmeh
Bazmohammadi
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.
Decision making approach
fuzzy satisfaction theorem
portfolio optimization
Risk Management
stochastic programming
2018
12
01
3569
3583
http://scientiairanica.sharif.edu/article_4381_3f50488968772586f3a0fcbf73b76fd7.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
INVESTIGATION OF DISPERSION ORDER ON CHIRP MICROWAVE GENERATION USING MICROWAVE PHOTONIC LINK WITHOUT OPTICAL FILTER
Mandeep
Singh
Sanjeev
Kumar Raghuwanshi
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.
RF Photonics
Triple Parallel-Intensity Modulators (TP-IM)
Fiber Dispersion
RoF
Optical Sideband Suppression Ratio (OPSSR)
Radio Frequency Spurious Suppression Ratio (RFSSR)
2018
12
01
3584
3590
http://scientiairanica.sharif.edu/article_4376_75695053d7fcce53b26c2994d979a690.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
GAIT GENERATION AND TRANSITION FOR BIPEDAL LOCOMOTION SYSTEM USING MORRIS-LECAR MODEL OF CENTRAL PATTERN GENERATOR
MOHAMMAD-REZA
SAYYED NOORANI
SAHAR
FARSHBAF RASHIDI
MARYAM
SHOARAN
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.
Central Pattern Generator (CPG)
Gait Transition
Bipedal Locomotion
Morris-Lecar Non-linear Oscillator
Genetic Algorithm
2018
12
01
3591
3603
http://scientiairanica.sharif.edu/article_4404_2536bc447019a17f3ef4f57333236f33.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Optimal design of fractional-order digital integrators:An evolutionary approach
S.
Mahata
S.
Kumar Saha
R.
Kar
D.
Mandal
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.
Fractional-order integrators
Hybrid flower pollination algorithm
Metaheuristics
optimization
2018
12
01
3604
3627
http://scientiairanica.sharif.edu/article_21197_dca0b1cdfcc2b3d78cbb08caf03acfe9.pdf
Scientia Iranica
Scientia Iranica
1026-3098
1026-3098
2018
25
6
Bayesian Hypothesis Testing for One Bit Compressed Sensing with Sensing Matrix Perturbation
H.
Zayyani
M.
Korki
F.
Marvasti
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.
Compressed sensing
One bit measurements
Bayesian hypothesis test
ML estimator
2018
12
01
3628
3633
http://scientiairanica.sharif.edu/article_4374_dd5ab11abdebdf11d3ff770a00e61405.pdf