arXiv subjects

Maria Spichkova

Publications and source records attributed to Maria Spichkova.

At least 37 records · Page 2Linked to original sources

arXiv2024

Mobile user experience from the lens of project-based learning

This paper presents an overview of mobile application projects conducted at the RMIT University as a part of the Learning and Teaching activities within Bachelor and Master programs, in collaboration with industrial partners. We discuss the lessons learned over eight years of teaching the corresponding courses and compare the results of our student project to the trends summarised in the recently published approached from other universities and countries.

cs.SE↗

arXiv2024

Cultural influence on autonomous vehicles acceptance

Autonomous vehicles and other intelligent transport systems have been evolving rapidly and are being increasingly deployed worldwide. Previous work has shown that perceptions of autonomous vehicles and attitudes towards them depend on various attributes, including the respondent's age, education level and background. These findings with respect to age and educational level are generally uniform, such as showing that younger respondents are typically more accepting of autonomous vehicles, as are those with higher education levels. However the influence of factors such as culture are much less clear cut. In this paper we analyse the relationship between acceptance of autonomous vehicles and national culture by means of the well-known Hofstede cultural model.

physics.soc-ph↗

arXiv2022

Towards computer vision technologies: Semi-automated reading of automated utility meters

In this report we analysed a possibility of using computer vision techniques for automated reading of utility meters. In our study, we focused on two computer vision techniques: an open-source solution Tensorflow Object Detection (Tensorflow) and a commercial solution Anyline. This report extends our previous publication: We start with presentation of a structured analysis of related approaches. After that we provide a detailed comparison of two computer vision technologies, Tensorflow Object Detection (Tensorflow) and Anyline, applied to semi-automated reading of utility meters. In this paper, we discuss limitations and benefits of each solution applied to utility meters reading, especially focusing on aspects such as accuracy and inference time. Our goal was to determine the solution that is the most suitable for this particular application area, where there are several specific challenges.

cs.CV↗

arXiv2022

Web-based Search: How Do Animated User Interface Elements Affect Autistic and Non-Autistic Users?

Many websites and other user interfaces include animated elements, particularly for advertisements. However, these can have a negative impact on users, with some cohorts, such as autistic users, being more affected. In our mixed methods study on the effect of irrelevant animations on usability we observed the effect on search activities. For those greatly impacted by on-screen animation the effect was not always to slow down a task, but search terms were entered hastily to avoid more exposure, with shorter queries on average and a greater tendency to copy and paste during query formulation. Autistic users found the task more mentally demanding, and were more distracted or annoyed by the animations.

cs.HC↗

arXiv2022

Application of property-based testing tools\\ for metamorphic testing

Metamorphic testing (MT) is a general approach for the testing of a specific kind of software systems -- so-called ``non-testable'', where the ``classical'' testing approaches are difficult to apply. MT is an effective approach for addressing the test oracle problem and test case generation problem. The test oracle problem is when it is difficult to determine the correct expected output of a particular test case or to determine whether the actual outputs agree with the expected outcomes. The core concept in MT is metamorphic relations (MRs) which provide formal specification of the system under test. One of the challenges in MT is \emph{effective test generation}. Property-based testing (PBT) is a testing methodology in which test cases are generated according to desired properties of the software. In some sense, MT can be seen as a very specific kind of PBT.\\ In this paper, we show how to use PBT tools to automate test generation and verification of MT. In addition to automation benefit, the proposed method shows how to combine general PBT with MT under the same testing framework.

cs.SE↗

arXiv2019

Towards Automated Management and Analysis of Heterogeneous Data Within Cannabinoids Domain

Cannabinoid research requires the cooperation of experts from various field biochemistry and chemistry to psychological and social sciences. The data that have to be managed and analysed are highly heterogeneous, especially because they are provided by a very diverse range of sources. A number of approaches focused on data collection and the corresponding analysis, restricting the scope to a sub-domain. Our goal is to elaborate a solution that would allow for automated management and analysis of heterogeneous data within the complete cannabinoids domain. The corresponding integration of diverse data sources would increase the quality and preciseness of the analysis. In this paper, we introduce the core ideas of the proposed framework as well as present the implemented prototype of a cannabinoids data platform.

cs.DL↗

arXiv2019

Easy Mobile Meter Reading for Non-Smart Meters: Comparison of AWS Rekognition and Google Cloud Vision Approaches

Electricity and gas meter reading is a time consuming task, which is done manually in most cases. There are some approaches proposing use of smart meters that report their readings automatically. However, this solution is expensive and requires (1) replacement of the existing meters, even when they are functional and new, and (2) large changes of the whole system dealing with the meter readings. This paper presents results of a project on automation of the meter reading process for the standard (non-smart) meters using computer vision techniques, focusing on the comparison of two computer vision techniques, Google Cloud Vision and AWS Rekognition.

cs.CY↗

arXiv2019

Towards Readability Aspects of Probabilistic Mode Automata

This paper presents a new approach and design model targeting hybrid designer- and operator-defined performance budgets for timing and energy consumption. The approach is based on Petri Nets formalism. As the cognitive load is typically high while using formal methods, this increases the chances of mistakes. Our approach is focused on the readability aspects and aims to decrease the cognitive load of developers. We illustrate the proposed approach on example of a sample embedded multi-media system, a modern digital camera.

cs.SE↗

arXiv2019

Requirements Engineering for Global Systems: Cultural, Regulatory and Technical Aspects

In this paper we present a formal framework for analysis and optimisation of the requirements specifications of systems developed to apply in several countries. As different countries typically have different regulations/laws as well as different cultural restrictions, the corresponding specific requirements might differ in each particular case. Our framework provides a basis for (1) systematic and formal analysis of the diversity and interdependencies within the sets of the requirements, to avoid non-compliance, contradictions and redundancies; (2) corresponding systematic process for change management in the case of global system development.

cs.SE↗

arXiv2018

Monitoring Informed Testing for IoT

Internet of Things (IoT) systems continuously collect a large amount of data from heterogeneous "smart objects" through standardised service interfaces. A key challenge is how to use these data and relevant event logs to construct continuously adapted usage profiles and apply them to enhance testing methods, i.e., prioritization of tests for the testing of continuous integration of an IoT system. In addition, these usage profiles provide relevance weightings to analyse architecture and behaviour of the system. Based on the analysis, testing methods can predict specific system locations that are susceptible to error, and therefore suggest where expanded runtime monitoring is necessary. Furthermore, IoT aims to connect billions of "smart devices" over the network. Testing even a small IoT system connecting a few dozens of smart devices would require a network of test Virtual Machines (VMs) possibly spreading across the Fog and the Cloud. In this paper we propose a framework for testing of each IoT layer in a separate VM environment, and discuss potential difficulties with optimal VM allocation.

cs.SE↗

arXiv2018

Formal FocusST Specification of CAN

This paper presents a formal specification of the Controller Area Network (CAN) protocol using FocusST framework. We formally describe core components of the protocol, which provides a basis for further formal analysis using the Isabelle/HOL theorem prover.

cs.FL↗

arXiv2018

Towards Classification of Lightweight Formal Methods

The use of lightweight formal methods (LFM) for the development of industrial applications has become a major trend. Although the term "lightweight formal methods" has been used for over ten years now, there seems to be no common agreement on what "lightweight" actually means, and different communities apply the term in all kinds of ways. In this paper, we explore the recent trends in the use of LFM, and establish our opinion that cost-effectiveness is the driving force to deploy LFM. Further, we propose a simple framework that should help to classify different LFM approaches and to estimate which of them are most cost-effective for a certain software engineering project. We demonstrate our framework using some examples.

cs.SE↗

arXiv2018

FocusST Solution for Analysis of Cryptographic Properties

To analyse cryptographic properties of distributed systems in a systematic way, a formal theory is required. In this paper, we present a theory that allows (1) to specify distributed systems formally, (2) to verify their cryptographic wrt. composition properties, and (3) to demonstrate the correctness of syntactic interfaces for specified system components automatically. To demonstrate the feasibility of the approach we use a typical example from the domain of crypto-based systems: a variant of the Internet security protocol TLS. A security flaw in the initial version of TLS specification was revealed using a semi-automatic theorem prover, Isabelle/HOL.

cs.SE↗

arXiv2018

Cultural Influences on Requirements Engineering Process in the Context of Saudi Arabia

Software development requires intensive communication between the requirements engineers and software stakeholders, particularly during the Requirements Engineering (RE) phase. Therefore, the individuals' culture might influence both the RE process and the result. Our aims are to investigate the extend of cultural influences on the RE process, and to analyze how the RE process can be adapted to take into account cultural aspects. The model we present is based on Hofstede's cultural theory. The model was applied on a pilot case study in the context of the conservative Saudi Arabian culture. The results reveal 6 RE aspects and 10 cultural factors that have a large impact on the RE practice.

cs.SE↗

arXiv2017

Towards Software Development For Social Robotics Systems

In this paper we introduce the core results of the project on software development for social robotics systems. The usability of maintenance and control features is crucial for many kinds of systems, but in the case of social robotics we also have to take into account that (1) the humanoid robot physically interacts with humans, (2) the conversation with children might have different requirements in comparison to the conversation with adults. The results of our work were implement for the humanoid PAL REEM robot, but their core ideas can be applied for other types of humanoid robots. We developed a web-based solution that supports the management of robot-guided tours, provides recommendations for the users as well as allows for a visual analysis of the data on previous tours.

cs.RO↗

arXiv2017

Formal specification of the FlexRay protocol using FocusST

FlexRay is a communication protocol developed by the FlexRay Consortium. The core members of the Consortium are Freescale Semiconductor, Robert Bosch GmbH, NXP Semiconductors, BMW, Volkswagen, Daimler, and General Motors, and the protocol was respectively oriented towards embedded systems in the automotive domain. This paper presents a formal specification of the FlexRay protocol using the FocusST framework. This work extends our previous research of formal specifications of this protocol using Focus formal language.

cs.LO↗

arXiv2017

Software Engineering Solutions To Support Vertical Transportation

In this paper we introduce the core results of the project on visualisation and analysis of data collected from the vertical transport facilities. The aim of the project was to provide better user experience as well as to help building maintenance staff to increase productivity of their work. We elaborated a web-based system for vertical transportation, to cover the needs of (1) staff working on building maintenance, (2) people who are regularly using the facilities in the corresponding buildings.

cs.HC↗

arXiv2017

(Auto)Focus approaches and their applications: A systematic review

Focus, a framework for formal specification and development of interactive systems, was introduced approx. 25 years ago. Since then this approach was broadly used in academic and industrial studies, as well as provided a basis for a number of another frameworks focusing on particular domains, and for the AF3 modelling tool. In this paper we provide a literature review of the corresponding approaches, academic case studies and industrial applications of these methods.

cs.SE↗