| Summary: |
HUDÁK, Š., ZAITSEV, D. A., KOREČKO, Š., ŠIMOŇÁK, S.:
MFDTE/PNtool - a Tool for the Rigorous Design, Analysis and Development of Concurrent and Time-Critical Systems [full paper]
This paper describes the PNtool - a tool for a design, analysis and development of concurrent and time-critical systems based on the Petri nets (PN) formalism. The PNtool supports four Petri nets dialects, which are also described in the paper: Generalized Petri nets, Time-basic nets, Evaluative and Coloured Petri nets. The Generalized PN are the basic type of Petri nets supported in the PNtool. Time-basic nets allow to model time-critical systems and Evaluative PN have the computational power equal to the Turing machines. In Coloured Petri nets it is possible to distinguish between tokens, because each of them has a value, called colour. The PNtool allows to design and simulate a system using any of supported PN dialects. In addition, an invariants-based analysis and reachability analysis is available for Generalized PN. Each Generalized and Evaluative PN can be loaded from and saved in a standard interchange format called PNML. All of these features are described in the paper, too.
The PNtool is implemented in Java as a part of the mFDT Environment (mFDTE). The mFDTE is a toolset for the formal design and analysis of concurrent discrete and time-critical systems, developed at the home institution of the authors. It integrates three formal methods with complementary features: Petri nets, process algebra and B-Method. This paper also describes interfaces, which connect the PNtool with other parts of mFDTE.
The work presented is supported by the grants No. 1/3140/06 and No. 1/4073/07 of the VEGA- The Scientific Grant Agency of Slovakia and NATO CLG 96128 grant.
|
VOKOROKOS, L., BALÁŽ, A., ÁDÁM, N.:
Events Planning in Intrusion Detection Systems [full paper]
The goal of this paper is to present designed architecture of intrusion detection system based on events planning and intrusion signature. The article describes problematic of the variation of intrusions and intrusion detection systems. The core of the proposed architecture is intrusion signature matching through petri nets that clasify system behaviour and determine potential intrusion of monitored computer system. The result is a new method of intrusions signature detection.
|
URBANČÍK, J., PIETRIKOVÁ, A., BANSKÝ, J:
Exploitation of LTCC Qualities in Gas Sensors Application [full paper]
In this contribution we deal with technology potential of the low temperature co-fired ceramic (LTCC) in association with design, development and production of organometallic thick film gas sensors. Customer demands to the gas sensors array and to the joint construction of the sensing part with evaluating ASIC led to the exploitation of LTCC potential in the production technology. The presented outcomes are based on the lot of investigations and simulations on the several models of organometallic gas sensors made with one common factor - low temperature co-fired ceramic utilisation.
The most important characteristic of LTCC and main reason for its utilisation in technology of sensor production is behind its temperature charactersistics also the possibility to fabricate various shapes in several separate layers which finally create monolithic ceramic module based on its attractive features. In this review, we want to emphasise tailored utilisation of LTCC in thick film based gas sensors, which were successively realised in the following parts: LTCC based multilayer heating systems for achievement of sensor operating temperature with exceedingly flat temperature distribution in the active sensor area, creation of the special LTCC sensor/ASIC carrier for relative high temperature and safety operation and finally LTCC based design for the gas sensor array.
|
PAVELKA, P., KRAJŇÁK, J., GALAJDA, P., KOCUR, D.:
Analysis of Non-Linear Distortions in MC-CDMA Systems [full paper]
Multi-carrier code division multiple access (MC-CDMA) is a powerful modulation technique that is being considered in many emerging broadband communication systems. It exploits the advantages of spread spectrum and the advantages of multi-carrier systems, particularly orthogonal frequency division multiplexing (OFDM) technique. However, since it uses OFDM, the MC-CDMA signals are a superposition of many narrow-band signals and, as a result suffer from strong envelope fluctuations which make them very prone to nonlinear effects introduced by high power amplifier (HPA). HPA introduces conversion in both amplitude and phase, that is responsible for increasing bit error rate, which is caused by the loss of orthogonality of both, the spreading sequences and subcarriers used in the downlink scenario. In order to be able design a robust method for the nonlinearity effects cancellation, it is necessary to analyze the effects of nonlinear amplification on the MC-CDMA signals. In this paper we have focused on the signals at the output of the nonlinear distorting device, where we observed two major phenomena, rotation and clouding, and spectral outgrowth. Additionally, we used a Bussgang theorem to represent output signal from the nonlinear distorting device as the sum of the scaled version of the input signal and the distortion term. The frequency domain representation of this distortion term let us express the distortion term as two disjoint sets, that correspond to in-band and out-of-band distortion term, respectively.
|
KOLLA, I., KOVÁČ, D.:
Communication Interfaces for Measuring Systems [full paper]
The presented paper deals with the proposal of the measuring chain assigned for remote measuring of parameters of distributed industrial systems. The designed solution should be able to do automatic measurement of all required parameters and to send obtained data to the remote centre, where they could be analyzed by telemeter based on the expert system.
|
VARGONČÍK, M., KOLCUN, M.:
Special Protection Schemes in Electric Power Systems [full paper]
The report represents the initial study that aims at designing SPS
(System Protection Scheme) having following characteristics: 1.) wide
area approach; 2.) capability of mitigation one or more dangerous
phenomena having a system wide nature (e.g. voltage instability,
frequency instability etc.); 3.) emergency protection function
(preventive protection can be sufficiently provided by SCADA/EMS
systems); 4.) execution of control, not only monitoring which does not
include the effect of change of power system behaviour when subjected to
control inputs (load shedding etc.); 5.) acceptance by utilities
This report briefly summarises available information in the area of SPS.
It is based on the survey of scientific literature (Conference
Proceedings, Journals) and partly on the author’s personal experience
(meetings with representatives of utilities and work in R&D in this
area) with focus on above listed features.
The structure of the report is as follows. In the first part
introduction. In the second chapter definition of the problem and some
fundamental questions are shortly outlined. The third chapter is divided
into sections. Each section concentrates on one major instability
phenomenon, starts with the description of instability principle, the
countermeasures that might be taken followed by an overview of what has
been done in that area – research activities both by the utilities and
in academic environment emphasizing the ones which have been brought to
final realization. The fourth chapter is conclusion.
|
BANDÁKOVÁ, J., KOLLÁR, J.:
On Adaptive Principles in Software Systems Evolution [full paper]
This paper deals with a problem of software system evolution. When the software system is developed the programmer tries to transform his ideas about final properties of the system in running application using some programming paradigm. Properties of the software system have an important role not only in development process but also in later phases of lifecycle, especially when the modification of an existing system is needed. Therefore it is necessary to express them formally as clearly as possible. When properties are expressed unambiguous then the behavior of the system can be controlled and modified effectively. In our research project we concentrate on formalizing the development process in form of aspect weaving and try to make the process automated. In addition, when the system is complex and complicated then it is appropriate to express it using multiple paradigms so we try to analyze the relations between functional, imperative, object-oriented and aspect-oriented paradigms that have crucial role for our goals. As can be seen, the principles of adaptive programming can be used in solution of software system evolution.
|
NOVITZKÁ, V., VERBOVÁ, A.:
On Optimizing Proof Search in Linear Logic by Value Iteration Method [full paper]
In this article we are interested in proving of linear logic sequents. In linear sequent calculus one sequent can have more than one proof tree. We choose the best among them satisfying some criterion. There can occur some non-deterministic choices in the process of building the proof of a sequent. We introduce probabilities to these proof constructions. Therefore we can apply one method of stochastic programming (value iteration method) to determine the optimal way in the proof search.
|
MOLNÁR, J., KOVÁČOVÁ, I.:
Distance Remote Measurement of Magnetic Field [full paper]
In the paper, sensing of magnetic field, communication between TEKTRONIX oscilloscope and computer via RS-232 and consequently measurement via Internet are described. The evaluation version of Control Web program has been utilized to allow a remote measurement. Designed program receives the data from Hall sensor by the digital oscilloscope. In addition the received data saves to the file on local computer and in following step distributes it to remote computer via Internet. Remote computer shows the shape of signals saved by oscilloscope using an external program. The created program also allows archiving the shapes to the file or opening the files with the shapes.
|
KOVAĽ, F., CIMBALA, R.:
IRC Analysis of Insulation Systems [full paper]
This article describes insulation systems of electrical equipments, degradation of this system and temperature stress of Remikaflex insulation. Also describes polarization processes in insulation and how does change this processes due to degradation. In addition deals with monitoring of dielectric properties by Isothermal Relaxation Current-analysis (IRC–analysis) and finally were displayed diagrams of times and currents depend on degradation time and we made conversion of dissipation factor to frequency domain through parameters we got by IRC-analysis.
|
VARCHOLA, M., DRUTAROVSKÝ, M.:
ZigBee Based Home Automation Wireless Sensor Network [full paper]
Increased demands on implementation of wireless sensor networks in automation praxis result in relatively new wireless standard – ZigBee. The new workplace was established on the Department of Electronics and Multimedia Communications (DEMC) in order to keep up with ZigBee modern trend. This paper presents the first results and experiences associated with ZigBee based wireless sensor networking. The accent was put on suitable chipset platform selection for Home Automation wireless network purposes. Four popular microcontrollers was selected to investigate memory requirements and power consumption such as ARM, x51, HCS08, and Coldfire. Next objective was to test interoperability between various manufacturers’ platforms, what is important feature of ZigBee standard. A simple network based on ZigBee physical layer as well as ZigBee compliant network were made to confirm the basic ZigBee interoperability.
|
TOMÁŠEK, M.:
Types for Calculus of Mobile Code Applications [full paper]
In this paper we present new type system for calculus of mobile ambients. Our approach is suitable for expressing dynamic properties of mobile code applications, where the main goal is to avoid ambiguities and possible maliciousness of some constructions in calculus of mobile ambients. We define behavioral scheme assigned to process types that statically specifies and checks access rights for authorization of ambients and threads to communicate and move. We proved the soundness theorem for the new type system and we demonstrated the system by showing how to model typical mobile code paradigms that are used to design mobile code applications.
|
DAŇO, I.:
On the Neurodynamic Model of Recurrent Networks [full paper]
Neurodynamical models of recurrent networks are characterized by their topology, by interactions between the elements sitting at the nodes of a network and by intrinsic dynamics of these local subsystems. In the present paper we give some relationship between Lyapunov’s exponents and the recurrent neural network model described by the system of delay-differential equations. We investigate the dynamic properties of the specific class of nonlinear delay-differential equations by studying the asymptotic behaviour of their solutions by means of Lyapunov’s exponents.
|
|
