Emerging research indicates that sentiment analyses of Dubrovnik focus mainly on hotel accommodations and restaurants. However, little attention has been paid to attractions, even though they are an important aspect of destinations and require more care and investment than amenities. This study examines how visitors experience Dubrovnik based on the reviews published on the Tripadvisor platform. Data were collected by implementing a web-scraping script to retrieve reviews of the tourist attraction “Old Town” from Tripadvisor, while data augmentation and random oversampling techniques were applied to address class imbalances. A sentiment analysis model, based on the pre-trained RoBERTa, was also developed and evaluated. In particular, a sentiment analysis was performed to compare reviews from 2022 and 2023. Overall, the results of this study are promising and demonstrate the effectiveness of this model and its potential applicability to other attractions. These findings provide valuable insights for decision makers to improve services and to increase visitor engagement.

In this paper we examine the effects of the COVID-19 pandemic on the usage of e-learning systems. We applied Formal Concept Analysis method to compare the students’ success on our freshmen year course Fundamentals of electrical engineering with the level of their activity on our e-learning system. This allowed us to visualize how did the COVID-19 pandemic impact the relationship between academic success and e-learning system engagement. Analysis showed that the students’ activity on our e-learning system increased during the pandemic and that this higher activity level is sustained even in the post-pandemic environment. In future work we will also utilize process mining techniques to analyze detailed log data from our in-house e-learning system.

This paper presents a unique and extensive dataset containing over 33 million entries with pairs in the form “spelling error → correction” from ispravi.me, the most popular Croatian online spellchecking service, collected since 2008. The dataset, compiled from the contribution of nearly 900,000 users, is a valuable resource for researchers and developers in the field of natural language processing (NLP), improving spellcheck accuracy, and language learning applications. The dataset may be used to accomplish several goals: (1) improving spellchecking accuracy by incorporating common user corrections and reducing false positives and negatives; (2) helping language learners identify common errors and learn correct spelling through targeted feedback; (3) analyzing data trends and patterns to uncover the most common spelling errors and their underlying causes; (4) identifying and evaluating factors that influence typing input; (5) improving NLP applications such as text recognition and machine translation. Tasks specific to the Croatian language include the creation of a letter-level confusion matrix and the refinement of word suggestions based on historical usage of the service. This comprehensive dataset provides researchers and practitioners with a wealth of information, opening the path for advancements in spellchecking, language learning, and NLP applications in the Croatian language.

In this paper we deal with the problem of creating an online environment for taking written exams during the lockdown caused by the COVID-19 pandemic. We have taken an approach that combines Microsoft Teams and an e-learning system. Before the exam begins all students join a Microsoft Teams meeting together with the teachers. This provides a simple way for teachers to check and monitor students' activity during the exam. Also, any student can immediately contact the teachers if they encounter technical problems. Online exam is accessed through an e-learning system. In our e-learning system exam questions can be parameterized, so that each student gets different variants of questions of the same difficulty. Furthermore, the order of the questions is randomized, so that students get different permutations of the questions. In smaller courses this can ensure that each student takes a unique variant of the exam which can discourage and minimize cheating. To answer questions students must upload scans or photos of their handwritten solutions. After the written online exam is manually evaluated, students must also take an oral exam through a Microsoft Teams meeting with the teachers. The described online exam procedure was used on the course Fundamentals of electrical engineering in the Fall semester of 2020/2021.

In this paper, we research the use of software combinatorial testing techniques and the Formal Concept Analysis method for preparing sets of questions for student assessment in e-learning systems. Utilizing these techniques and methods, we ensure that the selected questions optimally cover the course material and that each question combines multiple topics. Therefore, in this paper we introduce our method for preparing student assessments that performs automated combinatorial testing and selection of questions, as well as automated generation of appropriate sequences of questions. The input for our method is a set of questions labelled with attributes or features. This set of questions is pre-processed using the Formal Concept Analysis method, and then the combinatorial testing of question features is performed, which generates a concise list of test-cases covering all pairs or triples of question features. Correspondingly, our method helps in identifying and selecting a subset of questions that covers all generated test-cases. Afterwards, the Formal Concept Analysis method automatically generates suitable sequences of selected questions for formative student assessments in e-learning systems. In this paper we implemented the proposed combinatorial testing method, and also demonstrated the feasibility of the proposed method on a use-case from an actual e-learning system.

This paper presents a novel approach for automated analysis of process models discovered using process mining techniques. Process mining explores underlying processes hidden in the event data generated by various devices. Our proposed Inductive machine learning method was used to build business process models based on actual event log data obtained from a hotel's Property Management System (PMS). The PMS can be considered as a Multi Agent System (MAS) because it is integrated with a variety of external systems and IoT devices. Collected event log combines data on guests stay recorded by hotel staff, as well as data streams captured from telephone exchange and other external IoT devices. Next, we performed automated analysis of the discovered process models using formal methods. Spin model checker was used to simulate process model executions and automatically verify the process model. We proposed an algorithm for the automatic transformation of the discovered process model into a verification model. Additionally, we developed a generator of positive and negative examples. In the verification stage, we have also used Linear temporal logic (LTL) to define requested system specifications. We find that the analysis results will be well suited for process model repair.

In our paper we are exploring the use of formal methods for testing and verification of interactive e-learning web applications. These programs can be highly interactive and are often used for knowledge assessment and on-line tutoring purposes. They are written in web standard languages and executed in client browsers. Even simpler web applications can have various different interaction scenarios which makes them hard to test reliably. Therefore, we are using formal methods tools such as SPIN model checker and its Promela language to improve web application testing process. We create semi-automatically Promela process models from web application source code, and run their simulations, as well as verification using SPIN. Using these techniques, we want to identify flaws in web application design, and find and visualize all interaction scenarios using finite state automata. We will present use case example based on tutoring web application from our e-learning system used on our course Fundamentals of Electrical Engineering.

In our paper we are examining the application of process mining techniques in the development of adaptive e-learning systems such as Intelligent Tutoring Systems. Process mining techniques can discover business process models from event log data. Here, we will use process mining to discover and add new useful tutoring sessions (learnLg paths) to our adaptive e-learning system. E-learning knowledge base is an ontology (union of taxonomies) of a chosen domain. Using data in the ontology we build a directed acyclic graph with nodes (states) and labeled transitions (questions), or more formally, as a deterministic finite automaton (DFA). Each tutoring session is a run of the DFA, or in process mining terminology: one learning process model. We will apply well-known Angluin's L* algorithm on the data from e-learning system log flies to discover new useful tutoring sessions which can be added to the e-learning system DFA. We will present use case examples based on our e-learning system used on our course Fundamentals of Electrical Engineering..

In this paper we interpret constraint satisfaction problem (CSP) with model checker Spin and bounded model checkers from satisfiability modulo theories (SMT) solvers.Our previous experience shows that single example modelled in different ways and interpreted with the same solver can have different space and time consumption.The goal is to find a feasible translation from of CSP problem to model checker and SMT solver.For that purpose we build Promela models for Spin model checker and Z3 models for SMT solver.Domain problem used in examples is graph colouring applied to Sudoku puzzle.In the beginning we briefly introduce CSP, model checking, graph colouring and Sudoku puzzle.The central part of this paper deals with various modelling efforts of Sudoku puzzle.After that results are analysed and compared.The main benefits of this paper are twofold, as we use them for educational purposes within Formal Methods in System Design course and as a solution to industrial scale problems like wavelength assignment in photonic networks respectively.At the end we give a conclusion and propose future research directions.

In future generation networks and systems, innovation is enabled by introducing new open platforms where various developers may contribute with new and innovative services that will be provided to the end users as a service and at runtime. These open platforms have to secure high level of automation so that developers and users may contribute to or use the open platform via standard interfaces. Moreover, these new open platforms have to secure high quality standards that would be assured through autonomous mechanisms that are implemented within these open platforms. As one of the very important aspects for the majority of services and its users is the reliability that open platforms offer for its users. Here in this paper, we present a case study how to secure an open platform for reliable service delivery. The case study is based on the use of Scribble tool that implements session types as formalism for describing protocol interactions that secure reliable operation among Erlang applications.

This paper deals with the problem of automated generation of questions for basic electrical engineering education in elearning systems.One of the main challenges in developing e-learning systems is to create an effective knowledge testing module.In most of e-learning systems teachers need to manually compose test questions, prepare the correct and wrong answers, and added feedback information.The process is time-consuming and prone to errors.We have focused on problems in basic electrical engineering education, specifically seriesparallel DC circuits, and we propose a solution for automated generation of template based questions of various degrees of similarity and complexity.Our prototype Web application dynamically generates text of the question and its circuit diagram image, solves the problem, and as a feedback provides correct results and a step-by-step solution.The interface is bilingual, available in Croatian and English.We have used standard Web technologies, such as JavaScript, jQuery and SVG, together with MathJax for mathematical notation.We will recommend our students on the course Fundamentals of Electrical Engineering to use this Web Application for self-assessment and practice.In future work we plan to advance our Web application and to fully integrate it into our developing e-learning system.

E-health aims to improve health of citizens, productivity and efficiency in healthcare delivery, and the social and economic value of health by using information and communication technologies. It encompasses various interoperability approaches and mechanisms among health services, products and processes combined with organizational change in healthcare systems, covering interaction between patients and health-service providers, institution-to-institution transmission of data, or peer-to-peer communication between patients and/or health professionals. Since inappropriate use or misuse of medical information can lead to undesirable outcomes, medicine and health are considered as very sensitive areas in terms of human life and work. Therefore, security polices, practices and procedures must be in place as well as utilization of cyber security and defense technologies, which help to protect e-health systems against attacks, detect abnormal activities and to have proven contingency plans in place. This work presents a framework for security assessment of national e-health systems, allowing country-level practices and perspectives on cyber defense, information security and data protection in e-health to be considered in a holistic manner. The framework covers assessment criteria on different levels: from national security and critical infrastructures to personal data protection and user and information privacy, as well as dealing with various cyber security aspects in government-to-government, government-to-citizen and government-to-business categories of e-government ecosystem. Security assessment criteria are grouped into and analyzed through four interoperability aspects: legal, technical, semantic and organizational. The evidence for security assessment process conducted by using the framework was provided on Croatian e-Health showcase, with advantages given and limitations commented.

This paper gives an overview of relevant research in the area of process mining. Process mining techniques are able to extract knowledge from event logs. The major objective of process mining is to discover, monitor and improve real processes. Process mining aims to exploit event data in a meaningful way to identify and anticipate problems, and recommend countermeasures. Additionally, process mining places the existing massive volumes of data in the context of processes. Since extracting data is an integral part of any process mining procedure, data preparation or data pre-processing requires certain efforts. Examples have been given to indicate how the chosen process mining technique deals with incompleteness in the event log data. Experiments have been made on the real data collected from information system for accommodation services.

This paper deals with the problem of checking consistency of automatically generated exam questions in e-learning systems. We focus on the exam questions with the numeric solutions and the automatic evaluation of their answers. Each answer is evaluated as correct if it is within a specified range from the actual correct value. In our paper we check the consistency of exam questions evaluated with this simple method, i. e. are the answers calculated using wrong methods and based on false assumptions always evaluated as incorrect. We made a mutant testing algorithm for identifying inconsistent questions using model checking. At the end we present use cases based on the evaluation of students' answers on our courses Fundamentals of Electrical Engineering and Formal Methods in System Design.

We describe our web-based system for the analysis of students' results on the course Fundamentals of Electrical Engineering by applying the method of Formal Concept Analysis. We have focused on the students' answers and constructed their concept lattices or taxonomies of the subject matter. Finally, we have shown that this approach corresponds well with the actual students' overall results and final grades.

In this article we give a brief overview of the theory behind the formal concept analysis, a novel method for data representation and analysis. From given tabular input data this method finds all formal concepts and computes a concept lattice, a directed, acyclic graph, in which all formal concepts are hierarchically ordered. We describe the link between this method and formal logic, as well as graph theory. Finally we present one example of an application of this method in the field of computer aided learning. (C) 2014 The Authors. Published by Elsevier Ltd.

Modern Web or database servers are usually designed with a thread pool as a major component for servicing. Controlling of such servers, as well as defining adequate resource management policies, with the aim of minimizing requests' sojourn times presuppose the existence of performance models of thread-pooled systems. In this paper a queuing model of a thread pool is formulated along with a set of underlying assumptions and definitions used. Requests are abstracted in such a way that they are characterized by service time distribution and CPU consumption parameter. The model is defined as a Quasi-Birth-and-Death (QBD) process. Stability conditions for the model are derived and an analytic method based on generating functions for calculation of expected sojourn times is presented. The analytical results thus obtained are evaluated in a developed experimental environment. The environment contains a synthetic workload generator and an instrumented server application based on a standard Java 7 ThreadPoolExecutor thread pool. Sojourn time measurements confirm the theoretical results and also give additional insight into sojourn times related to more realistic workload cases that otherwise would be difficult to analyze formally.

Large-scale n-gram models are available for a small number of languages. So far, Croatian was not one of them. The research presented in this paper describes the development of n-gram database system suitable for large-scale language modeling in Croatian. The process of n-gram collection relies on Croatian academic online spellchecker Hascheck, which has been publicly available since 1993, and is today a popular language service, with average daily traffic exceeding million tokens. The approach demonstrated in this paper eliminated the need of n-gram data cleaning in the post-processing phase, which is a serious issue in other languages. The spellchecker dynamics allowed Heaps’ law modeling to be applied to Croatian n-grams, which enabled the prediction of n-gram count growth.

In this paper we describe modeling for verification of business process with Spin model checker. Our primary goal is the development of Promela language description for e–invoice web service. Modeling for verification follows Church’s synthesis problem: for input scenario “data–flow” model, output is Promela model. Sequence of model transformations translates the scenario into the Promela language code. At the end whole process is illustrated with e–invoice web service example.