| | SLO | ENG | Cookies and privacy

Bigger font | Smaller font

Search the digital library catalog Help

Query: search in
search in
search in
search in
* old and bologna study programme

Options:
  Reset


61 - 70 / 745
First pagePrevious page3456789101112Next pageLast page
61.
Akcijska logika dreves izvajanj z operatorjem unless
Robert Meolic, doctoral dissertation

Abstract: Doktorska disertacija definira in raziskuje akcijsko logiko dreves izvajanj z operatorjem unless (ACTLW). ACTLW je izjavna temporalna logika razvejanega časa. Izhaja iz logike ACTL, ki je bila vpeljana leta 1990 in je ena od uveljavljenih temporalnih logik za izražanje lastnosti modelov, ki temeljijo na dogodkih. ACTLW je fleksibilnejša od ACTL, saj ne vsiljuje uporabe notranjega dogodka T pri izražanju lastnosti. ACTLW je tudi nekoliko izraznejša od ACTL, saj vsebuje temporalni operator unless (W), katerega pomena v ACTL ni možno v celoti izraziti. Nasprotno pa lahko vse formule ACTL izrazimo z uporabo operatorjev ACTLW. ACTLW omogoča učinkovito izvedbo preverjanja modelov s podobnimi algoritmi kot pri preverjanju modela s CTL, kar je pomembna izboljšava glede na logiko ACTL. Doktorska disertacija podaja definicijo logike ACTLW, izpeljave vseh standardnih temporalnih operatorjev in algoritme za globalno preverjanje modela z ACTLW s simboličnim računanjem. Predstavljeni so tudi algoritmi za tvorjenje diagnostike pri ACTLW, za tvorjenje lineamih prič in protiprimerov pri ACTLW ter za tvorjenje avtomatov prič in proti primerov pri ACTLW. Doktorska disertacija je v celoto zaokrožena z vzorci formul ACTLW in dvema večjima praktičnima primeroma: verifikacijo več različnih algoritmov za medsebojno izključevanje in verifikacijo dveh asinhronih vezij za porazdeljeno medsebojno izključevanje.
Keywords: formalne metode verifikacije sistemov, preverjanje modela, temporalna logika, doktorske disertacije, CTL, ACTL, ACTLW, diagnostika, problem medsebojnega izključevanja
Published: 04.08.2017; Views: 273; Downloads: 40
.pdf Full text (1,04 MB)

62.
Preverjanje pravilnosti obnašanja sistemov s sočasnostjo
Robert Meolic, master's thesis

Abstract: Magistrsko delo obravnava metode preverjanja pravilnosti obnašanja sistemov, ki temeljijo na opisu sistema s procesno algebro. Podana je definicija procesne algebre in primeri opisov sistemov s procesi. Predstavljeno je ugotavljanje ekvivalence sledi, stroge, vejitvene in šibke opazovalne ekvivalence, ugotavljanje testne ekvivalence ter simbolično preverjanje modelov z izjavno vejitveno temporalno logiko ACTL. Vse obravnavane metode se med seboj odlično dopolnjujejo in skupaj tvorijo močno orodje za formalno verifikacijo sistemov. V magistrskem delu je opisana izvedba takšnega orodja z BDD-ji. Uporaba orodja je ponazorjena na primeru verifikacije komunikacijskega protokola BRP.
Keywords: formalne metode verifikacije, sistemi s sočasnostjo, procesne algebre, opazovalne ekvivalence, testne ekvivalence, simbolično preverjanje modelov, ACTL, BDD
Published: 04.08.2017; Views: 292; Downloads: 34
.pdf Full text (1,10 MB)

63.
Social presence and interaction in learning environments
Ines Kožuh, Zoran Jeremić, Andrej Sarjaš, Julija Lapuh Bele, Vladan Devedžić, Matjaž Debevc, 2014, original scientific article

Abstract: With the increased use of social media there is a growing interest in using social interaction and social presence in education. Despite this phenomenon, no appropriate methodology was found on effective integrating of both concepts into online learning. In this study, we propose integrating two different kinds of learning tools to provide social interaction and social presence in Personal Learning Environments. We have evaluated the proposed concept in a classroom setting, using a specific social interaction tool and a specific social presence tool. The findings revealed that although the use of the social interaction tool was positively associated with students% academic success, the perceived ease of using the social presence tool was negatively related to students' success.
Keywords: personal learning environment, social interaction, social presence, online social presence, academic success
Published: 03.08.2017; Views: 386; Downloads: 39
.pdf Full text (810,12 KB)
This document has many files! More...

64.
Applying automated model extraction for simulation and verification of real-life SDL specification with spin
Boštjan Vlaovič, Aleksander Vreže, Zmago Brezočnik, 2017, original scientific article

Abstract: Formally defined Specification and Description Language (SDL) is used for the design and specification of complex safety-critical systems. Each change in the specification of the product should be immediately checked formally against the requirements’ specification. This paper presents semi-automated system abstraction, automated model extraction, simulation, and formal verification of real-life complex SDL specification. Sound algorithms implemented in our sdl2pml automated model extraction tool preserve all properties of the SDL system. Sdl2pml includes our model of discrete time, abstraction, and support for all relevant SDL functionality and constructs such as dynamic process creation, rational data types, and communication with more than one process instance. To the best of our knowledge, most of them are not supported by any other known approach. We use our SpinRCP tool for simulation and formal verification of the extracted model with the Spin model checker. We demonstrate the applicability of our approach on ISDN User adaptation protocol from SI3000 Softswitch. The extracted Promela model is the largest one ever processed by Spin. We have shown that Spin simulation and model checking can be applied successfully to such huge models.
Keywords: formal specifications, automated extraction, formal languages, simulation, formal verification, model cheking, SDL, Promela, SpinRCP, Sdl2pml
Published: 03.08.2017; Views: 347; Downloads: 168
.pdf Full text (13,46 MB)
This document has many files! More...

65.
A wearable device and system for movement and biometric data acquisition for sports applications
Marko Kos, Iztok Kramberger, 2017, original scientific article

Abstract: This paper presents a miniature wearable device and a system for detecting and recording the movement and biometric information of a user during sport activities. The wearable device is designed to be worn on a wrist and can monitor skin temperature and pulse rate. Furthermore, it can monitor arm movement and detect gestures using inertial measurement unit. The device can be used for various professional and amateur sport applications and for health monitoring. Because of its small size and minimum weight, it is especially appropriate for swing-based sports like tennis or golf, where any additional weight on the arms would most likely disturb the player and have some influence on the player’s performance. Basic signal processing is performed directly on the wearable device but for more complex signal analysis, the data can be uploaded via the Internet to a cloud service, where it can be processed by a dedicated application. The device is powered by a lightweight miniature LiPo battery and has about 6 h of autonomy at maximum performance.
Keywords: biometric data acquisition, inertial sensing, movement detection, pulse rate, sensor fusion, wearable
Published: 03.08.2017; Views: 338; Downloads: 174
.pdf Full text (8,88 MB)
This document has many files! More...

66.
Suitability of the double Langevin function for description of anhysteretic magnetization curves in NO and GO electrical steel grades
Simon Steentjes, Martin Petrun, G. Glehn, Drago Dolinar, Kay Hameyer, 2017, original scientific article

Abstract: This paper compares the match obtained using the classical Langevin function, the tanh function as well as a recently by the authors proposed double Langevin function with the measured anhysteretic magnetization curve of three different non-oriented electrical steel grades and one grain-oriented grade. Two standard non-oriented grades and a high-silicon grade (Si content of 6.5%) made by CVD are analyzed. An excellent match is obtained using the double Langevin function, whereas the classical solutions are less appropriate. Thereby, problems such as those due to propagation of approximation errors observed in hysteresis modeling can be bypassed.
Keywords: polarization, magnetization measurement, magnetic materials, hysteresis models, Langevin function, electrical steel, saturation
Published: 03.08.2017; Views: 278; Downloads: 196
.pdf Full text (652,05 KB)
This document has many files! More...

67.
Rate-dependent extensions of the parametric magneto-dynamic model with magnetic hysteresis
Simon Steentjes, Martin Petrun, G. Glehn, Drago Dolinar, Kay Hameyer, 2017, original scientific article

Abstract: This paper extends the parametric magneto-dynamic model of soft magnetic steel sheets to account for the phase shift between local magnetic flux density and magnetic field strength. This phase shift originates from the damped motion of domain walls and is strongly dependent on the microstructure of the material. In this regard, two different approaches to include the rate-dependent effects are investigated: a purely phenomenological, mathematical approach and a physical-based one.
Keywords: magnetic hysteresis, eddies, magnetic flux, viscosity, magnetic fields, magneto-dynamic models, parametric
Published: 03.08.2017; Views: 278; Downloads: 176
.pdf Full text (567,72 KB)
This document has many files! More...

68.
Jezikovnoteoretska načela v korpusnem jezikoslovju
Darinka Verdonik, 2015, original scientific article

Abstract: Predmet razprave so teoretsko-metodološka načela, ki so se razvijala v krogih t. i. novofirthijancev, kjer se od vsega začetka opredeljujejo za korpusno analizo, čim manj obremenjeno s predhodnimi jezikoslovnimi teorijami. V prispevku najprej pregledamo dela teh avtorjev, iz katerih izhajajo med drugim slovnica vzorcev (angl. pattern grammar), teorija leksikalnega proženja (angl. lexical priming), teorija konvencij in invencij (angl. theory of norms and exploitations) ter teorija kontekstne prozodije (angl. contextual prosodic theory). Nato povzamemo njihove zaledne predpostavke in stališča o jeziku kot rezultatih raziskovanja. Tako definiramo šest skupnih načel: predmet raziskovanja je jezikovna raba, tj. jezik v »kontekstu situacije«, raziskovalni fokus se obrne k temu, kar je običajno, raziskovalčeva intuicija je v vlogi evalvacije avtentičnih jezikovnih rab, jezikovne ravni (slovnica in slovar) so razumljene kot prepletene, na jezikovni sistem se gleda kot visoko dinamičen, v teoretskih temeljih pa zavzame eno osrednjih mest jezikovni vzorec. Nazadnje opozorimo tudi na nekatere omejitve, s katerimi se soočamo pri korpusnem pristopu.
Keywords: korpusi (jezikoslovje), korpus kot teorija, popolni korpusni pristop, korpusno jezikoslovje, teorija jezika
Published: 03.08.2017; Views: 205; Downloads: 151
.pdf Full text (234,37 KB)
This document has many files! More...

69.
Security analysis and improvements to the psychopass method
Boštjan Brumen, Marjan Heričko, Ivan Rozman, Marko Hölbl, 2013, original scientific article

Abstract: Background: In a recent paper, Pietro Cipresso et al proposed the PsychoPass method, a simple way to create strong passwords that are easy to remember. However, the method has some security issues that need to be addressed. Objective: To perform a security analysis on the PsychoPass method and outline the limitations of and possible improvements to the method. Methods: We used the brute force analysis and dictionary attack analysis of the PsychoPass method to outline its weaknesses. Results: The first issue with the Psychopass method is that it requires the password reproduction on the same keyboard layout as was used to generate the password. The second issue is a security weakness: although the produced password is 24 characters long, the password is still weak. We elaborate on the weakness and propose a solution that produces strong passwords. The proposed version first requires the use of the SHIFT and ALT-GR keys in combination with other keys, and second, the keys need to be 1-2 distances apart. Conclusions: The proposed improved PsychoPass method yields passwords that can be broken only in hundreds of years based on current computing powers. The proposed PsychoPass method requires 10 keys, as opposed to 20 keys in the original method, for comparable password strength.
Keywords: passwords, cryptanalysis, data security
Published: 02.08.2017; Views: 269; Downloads: 150
.pdf Full text (542,01 KB)
This document has many files! More...

70.
Outsourcing medical data analyses
Boštjan Brumen, Marjan Heričko, Andrej Sevčnikar, Jernej Završnik, Marko Hölbl, 2013, original scientific article

Abstract: Background: Medical data are gold mines for deriving the knowledge that could change the course of a single patient’s life or even the health of the entire population. A data analyst needs to have full access to relevant data, but full access may be denied by privacy and confidentiality of medical data legal regulations, especially when the data analyst is not affiliated with the data owner. Objective: Our first objective was to analyze the privacy and confidentiality issues and the associated regulations pertaining to medical data, and to identify technologies to properly address these issues. Our second objective was to develop a procedure to protect medical data in such a way that the outsourced analyst would be capable of doing analyses on protected data and the results would be comparable, if not the same, as if they had been done on the original data. Specifically, our hypothesis was there would not be a difference between the outsourced decision trees built on encrypted data and the ones built on original data. Methods: Using formal definitions, we developed an algorithm to protect medical data for outsourced analyses. The algorithm was applied to publicly available datasets (N=30) from the medical and life sciences fields. The analyses were performed on the original and the protected datasets and the results of the analyses were compared. Bootstrapped paired t tests for 2 dependent samples were used to test whether the mean differences in size, number of leaves, and the accuracy of the original and the encrypted decision trees were significantly different. Results: The decision trees built on encrypted data were virtually the same as those built on original data. Out of 30 datasets, 100% of the trees had identical accuracy. The size of a tree and the number of leaves was different only once (1/30, 3%, P=.19). Conclusions: The proposed algorithm encrypts a file with plain text medical data into an encrypted file with the data protected in such a way that external data analyses are still possible. The results show that the results of analyses on original and on protected data are identical or comparably similar. The approach addresses the privacy and confidentiality issues that arise with medical data and is adherent to strict legal rules in the United States and Europe regarding the processing of the medical data.
Keywords: medical data, disclosure control, medical confidentiality, data analysis, data security
Published: 02.08.2017; Views: 334; Downloads: 37
.pdf Full text (3,34 MB)
This document has many files! More...

Search done in 0.44 sec.
Back to top
Logos of partners University of Maribor University of Ljubljana University of Primorska University of Nova Gorica