Search results for: Formal power series

Authors: Josip Vasilj, Petar Sarajcev, Damir Jakus

Abstract:

One of the major difficulties introduced with wind power penetration is the inherent uncertainty in production originating from uncertain wind conditions. This uncertainty impacts many different aspects of power system operation, especially the balancing power requirements. For this reason, in power system development planing, it is necessary to evaluate the potential uncertainty in future wind power generation. For this purpose, simulation models are required, reproducing the performance of wind power forecasts. This paper presents a wind power forecast error simulation models which are based on the stochastic process simulation. Proposed models capture the most important statistical parameters recognized in wind power forecast error time series. Furthermore, two distinct models are presented based on data availability. First model uses wind speed measurements on potential or existing wind power plant locations, while the seconds model uses statistical distribution of wind speeds.

Keywords: Wind power, Uncertainty, Stochastic process, Monte Carlo simulation.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3885

Authors: Anamika Gupta, Naveen Kumar, Vasudha Bhatnagar

Abstract:

This paper focuses on analyzing medical diagnostic data using classification rules in data mining and context reduction in formal concept analysis. It helps in finding redundancies among the various medical examination tests used in diagnosis of a disease. Classification rules have been derived from positive and negative association rules using the Concept lattice structure of the Formal Concept Analysis. Context reduction technique given in Formal Concept Analysis along with classification rules has been used to find redundancies among the various medical examination tests. Also it finds out whether expensive medical tests can be replaced by some cheaper tests.

Keywords: Data Mining, Formal Concept Analysis, Medical Data, Negative Classification Rules.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1686

Authors: Sebastian Kusch, Markus Kaiser

Abstract:

In this paper we analyze the application of a formal proof system to the discrete logarithm problem used in publickey cryptography. That means, we explore a computer verification of the ElGamal encryption scheme with the formal proof system Isabelle/HOL. More precisely, the functional correctness of this algorithm is formally verified with computer support. Besides, we present a formalization of the DSA signature scheme in the Isabelle/HOL system. We show that this scheme is correct what is a necessary condition for the usefulness of any cryptographic signature scheme.

Keywords: Formal proof system, higher-order logic, formal verification, cryptographic signature scheme.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1517

Authors: Khalid M. Aamir, Mohammad A. Maud

Abstract:

Power Spectral Density (PSD) of quasi-stationary processes can be efficiently estimated using the short time Fourier series (STFT). In this paper, an algorithm has been proposed that computes the PSD of quasi-stationary process efficiently using offline autoregressive model order estimation algorithm, recursive parameter estimation technique and modified sliding window discrete Fourier Transform algorithm. The main difference in this algorithm and STFT is that the sliding window (SW) and window for spectral estimation (WSA) are separately defined. WSA is updated and its PSD is computed only when change in statistics is detected in the SW. The computational complexity of the proposed algorithm is found to be lesser than that for standard STFT technique.

Keywords: Power Spectral Density (PSD), quasi-stationarytime series, short time Fourier Transform, Sliding window DFT.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1924

Authors: Yash Pal, A.Swarup, Bhim Singh

Abstract:

This paper presents a novel control strategy of a threephase four-wire Unified Power Quality (UPQC) for an improvement in power quality. The UPQC is realized by integration of series and shunt active power filters (APFs) sharing a common dc bus capacitor. The shunt APF is realized using a thee-phase, four leg voltage source inverter (VSI) and the series APF is realized using a three-phase, three leg VSI. A control technique based on unit vector template technique (UTT) is used to get the reference signals for series APF, while instantaneous sequence component theory (ISCT) is used for the control of Shunt APF. The performance of the implemented control algorithm is evaluated in terms of power-factor correction, load balancing, neutral source current mitigation and mitigation of voltage and current harmonics, voltage sag and swell in a three-phase four-wire distribution system for different combination of linear and non-linear loads. In this proposed control scheme of UPQC, the current/voltage control is applied over the fundamental supply currents/voltages instead of fast changing APFs currents/voltages, there by reducing the computational delay and the required sensors. MATLAB/Simulink based simulations are obtained, which support the functionality of the UPQC. MATLAB/Simulink based simulations are obtained, which support the functionality of the UPQC.

Keywords: Power Quality, UPQC, Harmonics, Load Balancing, Power Factor Correction, voltage harmonic mitigation, currentharmonic mitigation, voltage sag, swell

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2226

Authors: Kei Kawamorita, Ryouta Kasahara, Yuuki Mochizuki, Kenichiro Noguchi

Abstract:

A separation-kernel-based operating system (OS) has been designed for use in secure embedded systems by applying formal methods to the design of the separation-kernel part. The separation kernel is a small OS kernel that provides an abstract distributed environment on a single CPU. The design of the separation kernel was verified using two formal methods, the B method and the Spin model checker. A newly designed semi-formal method, the extended state transition method, was also applied. An OS comprising the separation-kernel part and additional OS services on top of the separation kernel was prototyped on the Intel IA-32 architecture. Developing and testing of a prototype embedded application, a point-of-sale application, on the prototype OS demonstrated that the proposed architecture and the use of formal methods to design its kernel part are effective for achieving a secure embedded system having a high-assurance separation kernel.

Keywords: B method, embedded systems, extended state transition, formal methods, separation kernel, Spin.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1886

Authors: Buket Turan Azizoğlu

Abstract:

In switch mode power inverters, small sized inverters can be obtained by increasing the switching frequency. Switching frequency increment causes high driver losses. Also, high dt di and dt dv produced by the switching action creates high Electromagnetic Interference (EMI) and Radio Frequency Interference (RFI). In this paper, a series half bridge series resonant inverter circuit is simulated and evaluated practically to demonstrate the turn-on and turn-off conditions during zero or close to zero voltage switching. Also, the reverse recovery current effects of the body diode of the MOSFETs were investigated by operating above and below resonant frequency.

Keywords: Driver losses, Half Bridge series resonant inverter, Zero Voltage Switching

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3721

Authors: Zeeshan Furqan, Shahabuddin Muhammad, Ratan Guha

Abstract:

IEEE has designed 802.11i protocol to address the security issues in wireless local area networks. Formal analysis is important to ensure that the protocols work properly without having to resort to tedious testing and debugging which can only show the presence of errors, never their absence. In this paper, we present the formal verification of an abstract protocol model of 802.11i. We translate the 802.11i protocol into the Strand Space Model and then prove the authentication property of the resulting model using the Strand Space formalism. The intruder in our model is imbued with powerful capabilities and repercussions to possible attacks are evaluated. Our analysis proves that the authentication of 802.11i is not compromised in the presented model. We further demonstrate how changes in our model will yield a successful man-in-the-middle attack.

Keywords: authentication, formal analysis, formal verification, security.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1481

Authors: Zainab M. Musa, Nordin M. A. Rahman, Julaily A. Jusoh

Abstract:

The web services applications for digital reference service (WSDRS) of LIS model is an informal model that claims to reduce the problems of digital reference services in libraries. It uses web services technology to provide efficient way of satisfying users’ needs in the reference section of libraries. The formal WSDRS model consists of the Z specifications of all the informal specifications of the model. This paper discusses the formal validation of the Z specifications of WSDRS model. The authors formally verify and thus validate the properties of the model using Z/EVES theorem prover.

Keywords: Validation, verification, formal, theorem proving.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1280

Authors: Siriporn Meenanan

Abstract:

The objective of this study is to investigate the attitude of Thai students towards the Thai series "Hormones the Series Season 2". This study was conducted in the quantitative research, and the questionnaires were used to collect data from 400 people of the sample group. Descriptive statistics were used in data analysis. The findings reveal that most participants have positive comments regarding the series. They strongly agreed that the series reflects on the way of life and problems of teenagers in Thailand. Hence, the participants believe that if adults have a chance to watch the series, they will have the better understanding of the teenagers. In addition, the participants also agreed that the contents of the play are appropriate and satisfiable as the contents of “Hormones the Series Season 2” will raise awareness among the teens and use it as a guide to prevent problems that might happen during their teenage life.

Keywords: Content analysis, attitude, Thai series, Hormones the series.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 913

Authors: Mohamed A. Sullabi

Abstract:

The importance of the formal specification in the software life cycle is barely concealing to anyone. Formal specifications use mathematical notation to describe the properties of information system precisely, without unduly constraining the way in how these properties are achieved. Having a correct and quality software specification is not easy task. This study concerns with how a group of rectifiers can communicate with each other and work to prepare and produce a correct formal software specification. WBCS has been implemented based mainly in the proposed supported cooperative work model and a survey conducted on the existing Webbased collaborative writing tools. This paper aims to assess the feasibility of executing the web-based collaboration process using WBCS. The purpose of conducting this test is to test the system as a whole for functionality and fitness for use based on the evaluation test plan.

Keywords: Formal methods, Formal specifications, collaborative writing, Usability testing.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1673

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this article we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (σ-algebras, probability spaces and conditional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes- Formula. Besides, we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this article shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in cryptographic research, if the corresponding basic mathematical knowledge is available in a database.

Keywords: prime numbers, primality tests, (conditional) probabilitydistributions, formal proof system, higher-order logic, formalverification, Bayes' Formula, Miller-Rabin primality test.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1425

Authors: Hadj Bourdoucen, Adel Gastli

Abstract:

In this paper, an approach for finding optimized layouts for connecting PV units delivering maximum array output power is suggested. The approach is based on considering the different varying parameters of PV units that might be extracted from a general two-diode model. These are mainly, solar irradiation, reverse saturation currents, ideality factors, series and shunt resistances in addition to operating temperature. The approach has been tested on 19 possible 2×3 configurations and allowed to determine the optimized configurations as well as examine the effects of the different units- parameters on the maximum output power. Thus, using this approach, standard arrays with n×m units can be configured for maximum generated power and allows designing PV based systems having reduced surfaces to fit specific required power, as it is the case for solar cars and other mobile systems.

Keywords: Photovoltaic, PV unit, optimum configuration, maximum power, Orcad.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1708

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this paper we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (o--algebras, probability spaces and condi¬tional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes' Formula. Besides we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this paper shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in crypto-graphic research, if the corresponding basic mathematical knowledge is available in a database.

Keywords: prime numbers, primality tests, (conditional) proba¬bility distributions, formal proof system, higher-order logic, formal verification, Bayes' Formula, Miller-Rabin primality test.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2143

Authors: Zainab M. Musa, Nordin M. A. Rahman, Julaily A. Jusoh

Abstract:

Digital reference service is when a traditional library reference service is provided electronically. In most cases users do not get full satisfaction from using digital reference service due to variety of reasons. This paper discusses the formal specification of web services applications for digital reference services (WSDRS). WSDRS is an informal model that claims to reduce the problems of digital reference services in libraries. It uses web services technology to provide efficient digital way of satisfying users’ need in the reference section of libraries. Informal model is in natural language which is inconsistent and ambiguous that may cause difficulties to the developers of the system. In order to solve this problem we decided to convert the informal specifications into formal specifications. This is supposed to reduce the overall development time and cost. We use Z language to develop the formal model and verify it with Z/EVES theorem prover tool.

Keywords: Formal, specifications, web services, digital reference services.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1577

Authors: Kazuo Komatsu, Hitoshi Takata

Abstract:

This paper discusses a design of nonlinear observer by a formal linearization method using an application of Chebyshev Interpolation in order to facilitate processes for synthesizing a nonlinear observer and to improve the precision of linearization. A dynamic nonlinear system is linearized with respect to a linearization function, and a measurement equation is transformed into an augmented linear one by the formal linearization method which is based on Chebyshev interpolation. To the linearized system, a linear estimation theory is applied and a nonlinear observer is derived. To show effectiveness of the observer design, numerical experiments are illustrated and they indicate that the design shows remarkable performances for nonlinear systems.

Keywords: nonlinear system, nonlinear observer, formal linearization, Chebyshev interpolation.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1548

Authors: Chih-Ling Huang, Wen-Yi Lin, Kuo-Mo Hsiao

Abstract:

A method based on the power series solution is proposed to solve the natural frequency of flapping vibration for the rotating inclined Euler beam with constant angular velocity. The vibration of the rotating beam is measured from the position of the corresponding steady state axial deformation. In this paper the governing equations for linear vibration of a rotating Euler beam are derived by the d'Alembert principle, the virtual work principle and the consistent linearization of the fully geometrically nonlinear beam theory in a rotating coordinate system. The governing equation for flapping vibration of the rotating inclined Euler beam is linear ordinary differential equation with variable coefficients and is solved by a power series with four independent coefficients. Substituting the power series solution into the corresponding boundary conditions at two end nodes of the rotating beam, a set of homogeneous equations can be obtained. The natural frequencies may be determined by solving the homogeneous equations using the bisection method. Numerical examples are studied to investigate the effect of inclination angle on the natural frequency of flapping vibration for rotating inclined Euler beams with different angular velocity and slenderness ratio.

Keywords: Flapping vibration, Inclination angle, Natural frequency, Rotating beam.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2145

Authors: K. Himaja, T. S. Surendra, S. Tara Kalyani

Abstract:

In this article, Optimal Control for Coordinated Control (COC) of Series Vectorial Compensator (SVeC) and Power System Stabilizer (PSS) in order to damp Low Frequency Oscillations (LFO) is proposed. SVeC is a series Flexible Alternating Current Transmission System (FACTS) device. The Optimal Control strategy based on state feedback control for coordination of PSS and SVeC controllers under different loading conditions has not been developed. So, the Optimal State Feedback Controller (OSFC) for incorporating of PSS and SVeC controllers in COC manner has been developed in this paper. The performance of the proposed controller is checked through eigenvalue analysis and nonlinear time domain simulation results. The proposed Optimal Controller design for the COC of SVeC and PSS results will be analyzed without controller. The comparative results show that Optimal Controller for COC of SVeC and PSSs improve greatly the system damping LFO than without controller.

Keywords: Coordinated control, damping controller, optimal state feedback controller, power system stabilizer, series vectorial compensator.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 725

Authors: Charline David, Alexandre Blondin Massé, Arnaud Zinflou

Abstract:

We present a multiple equation time series approach for the short-term load forecasting applied to the electrical power load consumption for the whole Quebec province, in Canada. More precisely, we take into account three meteorological variables — temperature, cloudiness and wind speed —, and we use meteorological measurements taken at different locations on the territory. Our final model shows an average MAPE score of 1.79% over an 8-years dataset.

Keywords: Short-term load forecasting, special days, time series, multiple equations, parallelization, clustering.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 210

Authors: Rafael Dias Silva

Abstract:

The school is a social institution that should promote learning situations that remain throughout life. Based on this, the teaching activities promoted in museum spaces can represent an educational strategy that contributes to the learning process in a more meaningful way. This article systematizes a series of elements that guide the use of these spaces for the scientific literacy of deaf students and as experiences of this nature are favorable for the school development through the concept of the circularity. The methodology for the didactic use of these spaces of non-formal education is one of the reflections developed in this study and how such environments can contribute to the learning in the classroom. To develop in the student the idea of ​​association making him create connections with the curricular proposal and notice how the proposed activity is articulated. It is in our interest that the experience lived in the museum be shared collaborating for the construction of a scientific literacy and cultural identity through the research.

Keywords: Accessibility in museums, Brazilian sign language, deaf students, teacher training.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 755

Authors: S.C.Swain, A.K.Balirsingh, S. Mahapatra, S. Panda

Abstract:

This paper presents a systematic approach for designing Static Synchronous Series Compensator (SSSC) based supplementary damping controllers for damping low frequency oscillations in a single-machine infinite-bus power system. The design problem of the proposed controller is formulated as an optimization problem and RCGA is employed to search for optimal controller parameters. By minimizing the time-domain based objective function, in which the deviation in the oscillatory rotor speed of the generator is involved; stability performance of the system is improved. Simulation results are presented and compared with a conventional method of tuning the damping controller parameters to show the effectiveness and robustness of the proposed design approach.

Keywords: Low frequency Oscillations, Phase CompensationTechnique, Real Coded Genetic Algorithm, Single-machine InfiniteBus Power System, Static Synchronous Series Compensator.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2445

Authors: Gayadhar Panda, P. K. Rautraya

Abstract:

Damping of inter-area electromechanical oscillations is one of the major challenges to the electric power system operators. This paper presents Gravitational Search Algorithm (GSA) for tuning Static Synchronous Series Compensator (SSSC) based damping controller to improve power system oscillation stability. In the proposed algorithm, the searcher agents are a collection of masses which interact with each other based on the Newtonian gravity and the laws of motion. The effectiveness of the scheme in damping power system oscillations during system faults at different loading conditions is demonstrated through time-domain simulation.

Keywords: FACTS, Damping controller design, Gravitational search algorithm (GSA), Power system oscillations, Single-machine infinite Bus power system, SSSC.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2301

Authors: S. Panda, S. C. Swain, A. K. Baliarsingh, C. Ardil

Abstract:

Optimal supplementary damping controller design for Thyristor Controlled Series Compensator (TCSC) is presented in this paper. For the proposed controller design, a multi-objective fitness function consisting of both damping factors and real part of system electromachanical eigenvalue is used and Real- Coded Genetic Algorithm (RCGA) is employed for the optimal supplementary controller parameters. The performance of the designed supplementary TCSC-based damping controller is tested on a weakly connected power system with different disturbances and loading conditions with parameter variations. Simulation results are presented and compared with a conventional power system stabilizer and also with the TCSC-based supplementary controller when the controller parameters are not optimized to show the effectiveness and robustness of the proposed approach over a wide range of loading conditions and disturbances.

Keywords: Power System Oscillations, Real-Coded Genetic Algorithm (RCGA), Thyristor Controlled Series Compensator (TCSC), Damping Controller, Power System Stabilizer.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2178

Authors: Kazuo Komatsu, Hitoshi Takata

Abstract:

In this paper we consider a nonlinear control design for nonlinear systems by using two-stage formal linearization and twotype LQ controls. The ordinary LQ control is designed on almost linear region around the steady state point. On the other region, another control is derived as follows. This derivation is based on coordinate transformation twice with respect to linearization functions which are defined by polynomials. The linearized systems can be made up by using Taylor expansion considered up to the higher order. To the resulting formal linear system, the LQ control theory is applied to obtain another LQ control. Finally these two-type LQ controls are smoothly united to form a single nonlinear control. Numerical experiments indicate that this control show remarkable performances for a nonlinear system.

Keywords: Formal Linearization, LQ Control, Nonlinear Control, Taylor Expansion, Zero Function.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1582

Authors: A.K. Baliarsingh, S. Panda, A.K. Mohanty, C. Ardil

Abstract:

This paper presents a systematic approach for designing Unified Power Flow Controller (UPFC) based supplementary damping controllers for damping low frequency oscillations in a single-machine infinite-bus power system. Detailed investigations have been carried out considering the four alternatives UPFC based damping controller namely modulating index of series inverter (mB), modulating index of shunt inverter (mE), phase angle of series inverter (δB ) and phase angle of the shunt inverter (δE ). The design problem of the proposed controllers is formulated as an optimization problem and Real- Coded Genetic Algorithm (RCGA) is employed to optimize damping controller parameters. Simulation results are presented and compared with a conventional method of tuning the damping controller parameters to show the effectiveness and robustness of the proposed design approach.

Keywords: Power System Oscillations, Real-Coded Genetic Algorithm (RCGA), Flexible AC Transmission Systems (FACTS), Unified Power Flow Controller (UPFC), Damping Controller.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2049

Authors: Sidhartha Panda, N. P. Padhy

Abstract:

Recently, genetic algorithms (GA) and particle swarm optimization (PSO) technique have attracted considerable attention among various modern heuristic optimization techniques. Since the two approaches are supposed to find a solution to a given objective function but employ different strategies and computational effort, it is appropriate to compare their performance. This paper presents the application and performance comparison of PSO and GA optimization techniques, for Thyristor Controlled Series Compensator (TCSC)-based controller design. The design objective is to enhance the power system stability. The design problem of the FACTS-based controller is formulated as an optimization problem and both the PSO and GA optimization techniques are employed to search for optimal controller parameters. The performance of both optimization techniques in terms of computational time and convergence rate is compared. Further, the optimized controllers are tested on a weakly connected power system subjected to different disturbances, and their performance is compared with the conventional power system stabilizer (CPSS). The eigenvalue analysis and non-linear simulation results are presented and compared to show the effectiveness of both the techniques in designing a TCSC-based controller, to enhance power system stability.

Keywords: Thyristor Controlled Series Compensator, geneticalgorithm; particle swarm optimization; Phillips-Heffron model;power system stability.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3118

Authors: Guowei Hou, Lixin Yu, Wei Zhuang, Hui Qin, Xue Yang

Abstract:

Formal verification is proposed to ensure the correctness of the design and make functional verification more efficient. As cache plays a vital role in the design of System on Chip (SoC), and cache with Memory Management Unit (MMU) and cache memory unit makes the state space too large for simulation to verify, then a formal verification is presented for such system design. In the paper, a formal model checking verification flow is suggested and a new cache memory model which is called “exhaustive search model” is proposed. Instead of using large size ram to denote the whole cache memory, exhaustive search model employs just two cache blocks. For cache system contains data cache (Dcache) and instruction cache (Icache), Dcache memory model and Icache memory model are established separately using the same mechanism. At last, the novel model is employed to the verification of a cache which is module of a custom-built SoC system that has been applied in practical, and the result shows that the cache system is verified correctly using the exhaustive search model, and it makes the verification much more manageable and flexible.

Keywords: Cache system, formal verification, novel model, System on Chip (SoC).

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2243

Authors: Snezhana G. Gocheva-Ilieva, Ivan H. Feschiev

Abstract:

In this study integral form and new recursive formulas for Favard constants and some connected with them numeric and Fourier series are obtained. The method is based on preliminary integration of Fourier series which allows for establishing finite recursive representations for the summation. It is shown that the derived recursive representations are numerically more effective than known representations of the considered objects.

Keywords: Effective summation of series, Favard constants, finite recursive representations, Fourier series

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1306

Authors: D. Mondal, A. Chakrabarti, A. Sengupta

Abstract:

This paper aims to select the optimal location and setting parameters of TCSC (Thyristor Controlled Series Compensator) controller using Particle Swarm Optimization (PSO) and Genetic Algorithm (GA) to mitigate small signal oscillations in a multimachine power system. Though Power System Stabilizers (PSSs) are prime choice in this issue, installation of FACTS device has been suggested here in order to achieve appreciable damping of system oscillations. However, performance of any FACTS devices highly depends upon its parameters and suitable location in the power network. In this paper PSO as well as GA based techniques are used separately and compared their performances to investigate this problem. The results of small signal stability analysis have been represented employing eigenvalue as well as time domain response in face of two common power system disturbances e.g., varying load and transmission line outage. It has been revealed that the PSO based TCSC controller is more effective than GA based controller even during critical loading condition.

Keywords: Genetic Algorithm, Particle Swarm Optimization, Small Signal Stability, Thyristor Controlled Series Compensator.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1911

Authors: Prima Gusti Yanti, Fairul Zabadi

Abstract:

The purpose of the study is to find out relation of moral massage between the authority and globalization in proverb. Proverb is one of the many forms of cultural identity of the Indonesian/Malay people filled with moral values. The values contained within those proverbs are beneficial not only to the society, but also to those who held power amidst on this era of globalization. The method being used is qualitative research through content analysis which is done by describing and uncovering the forms and meanings of proverbs used within Indonesia Minangkabau society. Sources for this study’s data were extracted from a Minangkabau native speaker in the sub district of Tanah Abang, Jakarta. Said sources were retrieved through a series of interviews with the Minangkabau native speaker, whose speech is still adorned with idiomatic expressions. The research findings show that there are 30 existed proverbs or idiomatic expressions in the Minangkabau language often used by its indigenous people. The thirty data contain moral values which are closely interwoven with the matter of power and globalization. Analytical results show that the fourteen moral values contained within proverbs reflect a firm connection between rule and power in globalization; such as: responsible, brave, togetherness and consensus, tolerance, politeness, thorough and meticulous, honest and keeping promise, ingenious and learning, care, self-correction, be fair, alert, arbitrary, self-awareness. Structurally, proverbs possess an unchangeably formal construction; symbolically, proverbs possess meanings that are clearly decided through ethnographic communicative factors along with situational and cultural contexts. Values contained within proverbs may be used as a guide in social management, be it between fellow men, between men and nature, or even between men and their Creator. Therefore, the meanings and values contained within the morals of proverbs could also be utilized as a counsel for those who rule and in charge of power in order to stem the tides of globalization that had already spread into sectoral, territorial and educational continuums.

Keywords: Continuum, globalization, identity, proverb, rule-power.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1870