The article presented here deals with the verification of a digital design using temporal logic and model checking. Temporal logic has been used as a specification language to catch the behaviour of the system design and model checking has been chosen as a verification method to evaluate the design accuracy. As a digital system to be modelled and verified we have chosen the sequence detector; the detected string is 010. To compare the way how to establish temporal model and its properties and to see better coincidences and differences in describing their behaviour we made up the model of the sequence detector in two variants: without and with overlapping. We took, as finite state machine (FSM), the both automata, the Moore as well as the Mealy, each considered without and with overlapping. After the temporal properties of the four drawn models had been defined we wrote respective programs corresponding to each of models, in SMV language, to pass them as input files into the SMV model checker. Finally, we tested the correctness of the models without and with overlapping also by submitting temporal properties of the weaker sequence detector to the stronger – the result was satisfying because all the fundamental properties of the Moore FSM without overlapping were verified also by the weaker Moore FSM with overlapping. Given the limited space available we made only this experiment, the other - with the Mealy FSM, could not be performed.

The authors compare two control strategies for direct AC-AC matrix converters; namely the Venturini method and the scalar strategy control method. The performance comparison of the two strategies is made under unbalanced distorted torque, rotor speed and stator current operation. The simulation of the three-phase matrix converter feeding an induction motor was accomplished by means of the "Matlab®/Simulink®" software. This package makes it possible to simulate the dynamic systems in a simple way and in graphic environment.

In the upcoming article eight new members of the dynamical systems of class C and F are investigated via numerical integration. Although four configurations of the state matrices are familiar with the chaos generation the others are hypothetic and complete the study. The aim of this paper is to discover and describe different canonical representations for a given set of the differential equations, i.e. existing mathematical model. Individual dynamical systems are distinct from the viewpoint of the geometry of the associated vector field. The motivation for discovering the new mathematical models capable to produce a complex dynamics including chaos is both pedagogical and practical. The latter case is obvious since the new system can be easier to be implemented as an electronic circuit or has other advantage like simpler location of strategic orbits.

The aim of the present paper is the study of the behavior of passivity based control and difficulties due to synthesis for various operating conditions of a synchronous motor with a permanent magnets. The study takes into account the guarantee of satisfactory static and dynamic performance. It also allows the system to be insensitive to disturbances and uncertainties on the parameters. A number of estimation techniques have been developed to achieve speed and position permanent magnet synchronous motor (PMSM) drives without mechanical sensor. Most of them suffer from variation of motor parameters such as the stator resistance, stator inductance and torque constant. Also, it is known that conventional linear estimators are not adaptive variations of the operating point in a nonlinear system. The sliding mode technique has shown promising results when estimating or controlling nonlinear systems. This paper presents a sliding mode observer (SMO) estimating the position and speed of a permanent magnet synchronous motor (PMSM) to achieve sensorless drive system. The effect of variations of motor parameters such as torque constant, stator resistance and stator inductance on the position and/ speed estimations, over a wide speed range, have been studied. Compared to other methods, the observer is more robust to operating conditions and parameter uncertainties. Simulations show that the observer is robust.

The estimation accuracy is mostly affected by the time-dependent growth of inertial sensor errors, especially the stochastic errors. In order to eliminate negative effect of these random errors, they must be accurately modelled. Usually the stochastic models are based by the 1st or 2nd Gauss-Markov models, where the key is the successful implementation that depends on how well the noise statistics of the inertial sensors is selected [9]. In order to improve the performance of the inertial sensors, the users are keen to know more details about the noise components for a better modelling of the stochastic part to improve the navigation solution [6], [7]. The main objective of this paper is to test the Allan variance as a unified method in identifying and modelling noise terms of inertial measurement unit sensors.

The synthesis algorithms of modern control theory and fuzzy logic have been studied to upgrade the performances of SMC. In this paper, Fuzzy sliding mode control, which takes the features of both SMC and FLC to overcome the disadvantage of chattering and enhancing the robustness of the controller, is presented. The fuzzy sliding mode controller is designed for a class of non linear dynamic systems to tackle the problems with model uncertainties, parameter fluctuations and external disturbances. By this design, the bounds of the uncertainties are not required to be known in advance, and the robust stability of closed loop system is analysed in the Lyapunov sense. A numerical example is simulated with the proposed algorithm, witch consists to control the synchronous motor speed. The simulation results show the effectiveness of the proposed control strategy with desired tracking accuracy and robustness.