Showing 1–45 of 45 results for author: Spichkova, M

Cultural influence on autonomous vehicles acceptance

Authors: Chowdhury Shahriar Muzammel, Maria Spichkova, James Harland

Abstract: 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, s… ▽ More 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. △ Less

Submitted 3 April, 2024; originally announced April 2024.

Comments: Preprint. Accepted to the 20th International Conference on Mobile and Ubiquitous Systems: Computing, Networking and Services (MobiQuitous 2023), Melbourne, Australia, November, 2023. Springer. Final version to be published by Springer (In Press)

Mobile user experience from the lens of project-based learning

Authors: Maria Spichkova

Abstract: 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… ▽ More 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. △ Less

Submitted 3 April, 2024; originally announced April 2024.

Comments: Preprint. Accepted to the 20th International Conference on Mobile and Ubiquitous Systems: Computing, Networking and Services (MobiQuitous 2023), Melbourne, Australia, November, 2023. Springer. Final version to be published by Springer (In Press)

Creating a Trajectory for Code Writing: Algorithmic Reasoning Tasks

Authors: Shruthi Ravikumar, Margaret Hamilton, Charles Thevathayan, Maria Spichkova, Kashif Ali, Gayan Wijesinghe

Abstract: Many students in introductory programming courses fare poorly in the code writing tasks of the final summative assessment. Such tasks are designed to assess whether novices have developed the analytical skills to translate from the given problem domain to coding. In the past researchers have used instruments such as code-explain and found that the extent of cognitive depth reached in these tasks c… ▽ More Many students in introductory programming courses fare poorly in the code writing tasks of the final summative assessment. Such tasks are designed to assess whether novices have developed the analytical skills to translate from the given problem domain to coding. In the past researchers have used instruments such as code-explain and found that the extent of cognitive depth reached in these tasks correlated well with code writing ability. However, the need for manual marking and personalized interviews used for identifying cognitive difficulties limited the study to a small group of stragglers. To extend this work to larger groups, we have devised several question types with varying cognitive demands collectively called Algorithmic Reasoning Tasks (ARTs), which do not require manual marking. These tasks require levels of reasoning which can define a learning trajectory. This paper describes these instruments and the machine learning models used for validating them. We have used the data collected in an introductory programming course in the penultimate week of the semester which required attempting ART type instruments and code writing. Our preliminary research suggests ART type instruments can be combined with specific machine learning models to act as an effective learning trajectory and early prediction of code-writing skills. △ Less

Submitted 3 April, 2024; originally announced April 2024.

Comments: Preprint. Accepted to the 19th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2024). Final version to be published by SCITEPRESS, http://www.scitepress.org

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

Authors: Maria Spichkova, Johan van Zyl

Abstract: 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. A… ▽ More 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. △ Less

Submitted 24 November, 2022; originally announced November 2022.

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

Authors: Nasser Alzahrani, Maria Spichkova, James Harland

Abstract: 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 parti… ▽ More 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. △ Less

Submitted 21 November, 2022; originally announced November 2022.

Comments: Preprint. Accepted to the 17th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2022). Final version published by SCITEPRESS, http://www.scitepress.org

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

Authors: Alexandra L. Uitdenbogerd, Maria Spichkova, Mona Alzahrani

Abstract: 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… ▽ More 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. △ Less

Submitted 21 November, 2022; originally announced November 2022.

Comments: Preprint. Accepted to the 17th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2022). Final version published by SCITEPRESS, http://www.scitepress.org

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

Authors: Maria Spichkova, Johan van Zyl, Siddharth Sachdev, Ashish Bhardwaj, Nirav Desai

Abstract: 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. T… ▽ More 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. △ Less

Submitted 21 October, 2019; originally announced October 2019.

Comments: Preprint. Accepted to the 14th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2019). Final version published by SCITEPRESS

Towards Automated Management and Analysis of Heterogeneous Data Within Cannabinoids Domain

Authors: Kenji Koga, Maria Spichkova, Nitin Mantri

Abstract: 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-d… ▽ More 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. △ Less

Submitted 21 October, 2019; originally announced October 2019.

Comments: Preprint. Accepted to the 14th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2019). Final version published by SCITEPRESS

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

Authors: Maria Spichkova, Heinz Schmidt

Abstract: 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 an… ▽ More 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. △ Less

Submitted 11 October, 2019; originally announced October 2019.

Comments: Preprint. Accepted to 14th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2019). Final version published by SciTePress

Towards Readability Aspects of Probabilistic Mode Automata

Authors: Heinz Schmidt, Maria Spichkova

Abstract: 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… ▽ More 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. △ Less

Submitted 11 October, 2019; originally announced October 2019.

Comments: Preprint. Accepted to 14th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2019). Final version published by SciTePress

Monitoring Informed Testing for IoT

Authors: Ahmed Abdullah, Heinz W. Schmidt, Maria Spichkova, Huai Liu

Abstract: 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.… ▽ More 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. △ Less

Submitted 13 December, 2018; originally announced December 2018.

Comments: PREPRINT. Paper accepted to the 25th Australasian Software Engineering Conference (ASWEC 2018)

Formal FocusST Specification of CAN

Authors: Maria Spichkova

Abstract: 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. 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. △ Less

Submitted 20 November, 2018; originally announced November 2018.

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

Authors: Tawfeeq Alsanoosy, Maria Spichkova, James Harland

Abstract: 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 ta… ▽ More 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. △ Less

Submitted 5 July, 2018; originally announced July 2018.

Comments: Preprint. Accepted to the 13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2018). Final version published by SCITEPRESS

FocusST Solution for Analysis of Cryptographic Properties

Authors: Maria Spichkova, Radhika Bhat

Abstract: 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 feasibi… ▽ More 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. △ Less

Submitted 5 July, 2018; originally announced July 2018.

Comments: Preprint. Accepted to the 13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2018). Final version published by SCITEPRESS

Towards Classification of Lightweight Formal Methods

Authors: Anna Zamansky, Maria Spichkova, Guillermo Rodriguez-Navas, Peter Herrmann, Jan Olaf Blech

Abstract: 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 L… ▽ More 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. △ Less

Submitted 5 July, 2018; originally announced July 2018.

Comments: Preprint. Accepted to the 13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2013). Final version published by SCITEPRESS

Formal specification of the FlexRay protocol using FocusST

Authors: Maria Spichkova

Abstract: 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… ▽ More 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. △ Less

Submitted 14 December, 2017; originally announced January 2018.

Towards Software Development For Social Robotics Systems

Authors: Chong Sun, Jiongyan Zhang, Cong Liu, Barry Chew Bao King, Yuwei Zhang, Matthew Galle, Maria Spichkova

Abstract: 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… ▽ More 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. △ Less

Submitted 22 December, 2017; originally announced December 2017.

Software Engineering Solutions To Support Vertical Transportation

Authors: Alber J. Christianto, Peng Chen, Osheen Walawedura, Annie Vuong, Jun Feng, Dong Wang, Maria Spichkova

Abstract: 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 b… ▽ More 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. △ Less

Submitted 13 December, 2017; originally announced December 2017.

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

Authors: Maria Spichkova

Abstract: 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 approach… ▽ More 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. △ Less

Submitted 21 November, 2017; originally announced November 2017.

From Temporal Models to Property-Based Testing

Authors: Nasser Alzahrani, Maria Spichkova, Jan Olaf Blech

Abstract: This paper presents a framework to apply property-based testing (PBT) on top of temporal formal models. The aim of this work is to help software engineers to understand temporal models that are presented formally and to make use of the advantages of formal methods: the core time-based constructs of a formal method are schematically translated to the BeSpaceD extension of the Scala programming lang… ▽ More This paper presents a framework to apply property-based testing (PBT) on top of temporal formal models. The aim of this work is to help software engineers to understand temporal models that are presented formally and to make use of the advantages of formal methods: the core time-based constructs of a formal method are schematically translated to the BeSpaceD extension of the Scala programming language. This allows us to have an executable Scala code that corresponds to the formal model, as well as to perform PBT of the models functionality. To model temporal properties of the systems, in the current work we focus on two formal languages, TLA+ and FocusST. △ Less

Submitted 28 May, 2017; originally announced May 2017.

Comments: Preprint. Accepted to the 12th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2017). Final version published by SCITEPRESS, http://www.scitepress.org

Individual and Social Requirement Aspects of Sustainable eLearning Systems

Authors: Ahmed D. Alharthi, Maria Spichkova

Abstract: Internationalization of the higher education has created the so-called borderless university, which provides better opportunities for learning and increases the human and social sustainability. eLearning systems are a special kind of software systems, developed to provide a platform for accessible teaching and learning, including also online access to learning materials and online support for lear… ▽ More Internationalization of the higher education has created the so-called borderless university, which provides better opportunities for learning and increases the human and social sustainability. eLearning systems are a special kind of software systems, developed to provide a platform for accessible teaching and learning, including also online access to learning materials and online support for learning and teaching. The aim of our current work is to extract, analyse, and combine the results from multiple studies in order to develop an RE framework for sustainable eLearning systems. We call a system sustainable, if it has a positive effect on and whose direct and indirect negative impacts resulting from its development, deployment, and usage are minimal. Sustainability has various dimensions. We classify sustainability requirements of eLearning system to five dimensions: individual (human), social, technical, environmental, and economic. In this paper, we focus on human and social aspects (i.e., individual needs the relationship of people within society), as the eLearning systems have a very strong impact on human dimension of sustainability, where their impact on environmental dimension is rather small. This also provides us a basis to identify the corresponding requirements for sustainable eLearning systems. These requirements include collaboration, learner-centred features, leadership development and the reuse of the learning materials. As a result, achieving individual and social requirements for eLearning systems would provide higher quality of leaning and teaching, as well as better opportunities for learning and increasing the human and social sustainability. △ Less

Submitted 16 January, 2017; originally announced January 2017.

Comments: Preprint. Paper accepted to ICEER 2016

Spatio-temporal Models for Formal Analysis and Property-based Testing

Authors: Nasser Alzahrani, Maria Spichkova, Jan Olaf Blech

Abstract: This paper presents our ongoing work on spatio-temporal models for formal analysis and property-based testing. Our proposed framework aims at reducing the impedance mismatch between formal methods and practitioners. We introduce a set of formal methods and explain their interplay and benefits in terms of usability. This paper presents our ongoing work on spatio-temporal models for formal analysis and property-based testing. Our proposed framework aims at reducing the impedance mismatch between formal methods and practitioners. We introduce a set of formal methods and explain their interplay and benefits in terms of usability. △ Less

Submitted 9 December, 2016; v1 submitted 6 December, 2016; originally announced December 2016.

Comments: Preprint. Accepted to the Software Technologies: Applications and Foundations (STAF 2016). Final version published by Springer International Publishing AG

"Boring formal methods" or "Sherlock Holmes deduction methods"?

Authors: Maria Spichkova

Abstract: This paper provides an overview of common challenges in teaching of logic and formal methods to Computer Science and IT students. We discuss our experiences from the course IN3050: Applied Logic in Engineering, introduced as a "logic for everybody" elective course at at TU Munich, Germany, to engage pupils studying Computer Science, IT and engineering subjects on Bachelor and Master levels. Our go… ▽ More This paper provides an overview of common challenges in teaching of logic and formal methods to Computer Science and IT students. We discuss our experiences from the course IN3050: Applied Logic in Engineering, introduced as a "logic for everybody" elective course at at TU Munich, Germany, to engage pupils studying Computer Science, IT and engineering subjects on Bachelor and Master levels. Our goal was to overcome the bias that logic and formal methods are not only very complicated but also very boring to study and to apply. In this paper, we present the core structure of the course, provide examples of exercises and evaluate the course based on the students' surveys. △ Less

Submitted 6 December, 2016; originally announced December 2016.

Comments: Preprint. Accepted to the Software Technologies: Applications and Foundations (STAF 2016). Final version published by Springer International Publishing AG. arXiv admin note: substantial text overlap with arXiv:1602.05170

Model-based generation of natural language specifications

Authors: Phan Vo Thu Nhat, Maria Spichkova

Abstract: Application of formal models provides many benefits for the software and system development, however, the learning curve of formal languages could be a critical factor for an industrial project. Thus, a natural language specification that reflects all the aspects of the formal model might help to understand the model and be especially useful for the stakeholders who do not know the corresponding f… ▽ More Application of formal models provides many benefits for the software and system development, however, the learning curve of formal languages could be a critical factor for an industrial project. Thus, a natural language specification that reflects all the aspects of the formal model might help to understand the model and be especially useful for the stakeholders who do not know the corresponding formal language. Moreover, an automated generation of the documentation from the model would replace manual updates of the documentation for the cases the model is modified. This paper presents an ongoing work on generating natural language specifications from formal models. Our goal is to generate documentation in English from the basic modelling artefacts, such as data types, state machines, and architectural components. To allow further formal analysis of the generated specification, we restrict English to its subset, Attempto Controlled English. △ Less

Submitted 6 December, 2016; originally announced December 2016.

Comments: Preprint. Accepted to the Software Technologies: Applications and Foundations (STAF 2016). Final version published by Springer International Publishing AG

Managing Usability and Reliability Aspects in Cloud Computing

Authors: Maria Spichkova, Heinz W. Schmidt, Ian E. Thomas, Iman I. Yusuf, Steve Androulakis, Grischa R. Meyer

Abstract: Cloud computing provides a great opportunity for scientists, as it enables large-scale experiments that cannot are too long to run on local desktop machines. Cloud-based computations can be highly parallel, long running and data-intensive, which is desirable for many kinds of scientific experiments. However, to unlock this power, we need a user-friendly interface and an easy-to-use methodology for… ▽ More Cloud computing provides a great opportunity for scientists, as it enables large-scale experiments that cannot are too long to run on local desktop machines. Cloud-based computations can be highly parallel, long running and data-intensive, which is desirable for many kinds of scientific experiments. However, to unlock this power, we need a user-friendly interface and an easy-to-use methodology for conducting these experiments. For this reason, we introduce here a formal model of a cloud-based platform and the corresponding open-source implementation. The proposed solution allows to conduct experiments without having a deep technical understanding of cloud-computing, HPC, fault tolerance, or data management in order to leverage the benefits of cloud computing. In the current version, we have focused on biophysics and structural chemistry experiments, based on the analysis of big data from synchrotrons and atomic force microscopy. The domain experts noted the time savings for computing and data management, as well as user-friendly interface. △ Less

Submitted 6 December, 2016; originally announced December 2016.

Comments: Preprint. Accepted to the 11th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2016). Final version published by SCITEPRESS, http://www.scitepress.org

Spatio-temporal features of FocusST

Authors: Maria Spichkova

Abstract: In this technical report we summarise the spatio-temporal features and present the core operators of FocusST specification framework. We present the general idea of these operators, using a Steam Boiler System example to illustrate how the specification framework can be applied. FocusST was inspired by Focus, a framework for formal specification and development of interactive systems. In contras… ▽ More In this technical report we summarise the spatio-temporal features and present the core operators of FocusST specification framework. We present the general idea of these operators, using a Steam Boiler System example to illustrate how the specification framework can be applied. FocusST was inspired by Focus, a framework for formal specification and development of interactive systems. In contrast to Focus, FocusST is devoted to specify and to analyse spatial (S) and timing (T) aspects of the systems, which is also reflected in the name of the framework: the extension ST highlights the spatio-temporal nature of the specifications. △ Less

Submitted 25 October, 2016; originally announced October 2016.

Applied Logic in Engineering

Authors: Maria Spichkova

Abstract: Logic not only helps to solve complicated and safety-critical problems, but also disciplines the mind and helps to develop abstract thinking, which is very important for any area of Engineering. In this technical report, we present an overview of common challenges in teaching of formal methods and discuss our experiences from the course Applied Logic in Engineering. This course was taught at TU Mu… ▽ More Logic not only helps to solve complicated and safety-critical problems, but also disciplines the mind and helps to develop abstract thinking, which is very important for any area of Engineering. In this technical report, we present an overview of common challenges in teaching of formal methods and discuss our experiences from the course Applied Logic in Engineering. This course was taught at TU Munich, Germany, in Winter Semester 2012/2013. △ Less

Submitted 9 February, 2016; originally announced February 2016.

Towards a Human-Centred Approach in Modelling and Testing of Cyber-Physical Systems

Authors: Maria Spichkova, Anna Zamansky, Eitan Farchi

Abstract: The ability to capture different levels of abstraction in a system model is especially important for remote integration, testing/verification, and manufacturing of cyber-physical systems (CPSs). However, the complexity of modelling and testing of CPSs makes these processes extremely prone to human error. In this paper we present our ongoing work on introducing human-centred considerations into mod… ▽ More The ability to capture different levels of abstraction in a system model is especially important for remote integration, testing/verification, and manufacturing of cyber-physical systems (CPSs). However, the complexity of modelling and testing of CPSs makes these processes extremely prone to human error. In this paper we present our ongoing work on introducing human-centred considerations into modelling and testing of CPSs, which allow for agile iterative refinement processes of different levels of abstraction when errors are discovered or missing information is completed. △ Less

Submitted 22 January, 2016; originally announced January 2016.

Comments: Preprint. Accepted to the Workshop on Automated Testing for Cyber-Physical Systems in the Cloud at ICPADS 2015

Model-based Hazard and Impact Analysis

Authors: Sonila Dobi, Mario Gleirscher, Maria Spichkova, Peter Struss

Abstract: Hazard and impact analysis is an indispensable task during the specification and development of safety-critical technical systems, and particularly of their software-intensive control parts. There is a lack of methods supporting an effective (reusable, automated) and integrated (cross-disciplinary) way to carry out such analyses. This report was motivated by an industrial project whose goal was… ▽ More Hazard and impact analysis is an indispensable task during the specification and development of safety-critical technical systems, and particularly of their software-intensive control parts. There is a lack of methods supporting an effective (reusable, automated) and integrated (cross-disciplinary) way to carry out such analyses. This report was motivated by an industrial project whose goal was to survey and propose methods and models for documentation and analysis of a system and its environment to support hazard and impact analysis as an important task of safety engineering and system development. We present and investigate three perspectives of how to properly encode safety-relevant domain knowledge for better reuse and automation, identify and assess all relevant hazards, as well as pre-process this information and make it easily accessible for reuse in other safety and systems engineering activities and, moreover, in similar engineering projects. △ Less

Submitted 9 December, 2015; originally announced December 2015.

Report number: TUM I1333

Requirements Engineering Aspects of a Geographically Distributed Architecture

Authors: Maria Spichkova, Heinz Schmidt

Abstract: We present our ongoing work on requirements specification and analysis for the geographically distributed software and systems. Develo** software and systems within/for different countries or states or even within/for different organisations means that the requirements to them can differ in each particular case. These aspects naturally impact on the software architecture and on the development p… ▽ More We present our ongoing work on requirements specification and analysis for the geographically distributed software and systems. Develo** software and systems within/for different countries or states or even within/for different organisations means that the requirements to them can differ in each particular case. These aspects naturally impact on the software architecture and on the development process as a whole. The challenge is to deal with this diversity in a systematic way, avoiding contradictions and non-compliance. In this paper, we present a formal framework for the analysis of the requirements diversity, which comes from the differences in the regulations, laws and cultural aspects for different countries or organisations. The framework also provides the corresponding architectural view and the methods for requirements structuring and optimisation. △ Less

Submitted 7 August, 2015; originally announced August 2015.

Comments: Preprint. Accepted to the 10th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2015)

Chiminey: Reliable Computing and Data Management Platform in the Cloud

Authors: Iman I. Yusuf, Ian E. Thomas, Maria Spichkova, Steve Androulakis, Grischa R. Meyer, Daniel W. Drumm, George Opletal, Salvy P. Russo, Ashley M. Buckle, Heinz W. Schmidt

Abstract: The enabling of scientific experiments that are embarrassingly parallel, long running and data-intensive into a cloud-based execution environment is a desirable, though complex undertaking for many researchers. The management of such virtual environments is cumbersome and not necessarily within the core skill set for scientists and engineers. We present here Chiminey, a software platform that enab… ▽ More The enabling of scientific experiments that are embarrassingly parallel, long running and data-intensive into a cloud-based execution environment is a desirable, though complex undertaking for many researchers. The management of such virtual environments is cumbersome and not necessarily within the core skill set for scientists and engineers. We present here Chiminey, a software platform that enables researchers to (i) run applications on both traditional high-performance computing and cloud-based computing infrastructures, (ii) handle failure during execution, (iii) curate and visualise execution outputs, (iv) share such data with collaborators or the public, and (v) search for publicly available data. △ Less

Submitted 5 July, 2015; originally announced July 2015.

Comments: Preprint, ICSE 2015

Human Factors in Software Reliability Engineering

Authors: Maria Spichkova, Huai Liu, Mohsen Laali, Heinz W. Schmidt

Abstract: In this paper, we present our vision of the integration of human factors engineering into the software development process. The aim of this approach is to improve the quality of software and to deal with human errors in a systematic way. In this paper, we present our vision of the integration of human factors engineering into the software development process. The aim of this approach is to improve the quality of software and to deal with human errors in a systematic way. △ Less

Submitted 12 March, 2015; originally announced March 2015.

Comments: Preprint, Workshop on Applications of Human Error Research to Improve Software Engineering (WAHESE) at ICSE 2015

Reconciling a component and process view

Authors: Maria Spichkova, Heinz Schmidt

Abstract: In many cases we need to represent on the same abstraction level not only system components but also processes within the system, and if for both representation different frameworks are used, the system model becomes hard to read and to understand. We suggest a solution how to cover this gap and to reconcile component and process views on system representation: a formal framework that gives the ad… ▽ More In many cases we need to represent on the same abstraction level not only system components but also processes within the system, and if for both representation different frameworks are used, the system model becomes hard to read and to understand. We suggest a solution how to cover this gap and to reconcile component and process views on system representation: a formal framework that gives the advantage of solving design problems for large-scale component systems. △ Less

Submitted 11 March, 2015; originally announced March 2015.

Comments: Preprint, 7th International Workshop on Modeling in Software Engineering (MiSE) at ICSE 2015

Towards Logical Architecture and Formal Analysis of Dependencies Between Services

Authors: Maria Spichkova, Heinrich Schmidt

Abstract: This paper presents a formal approach to modelling and analysis of data and control flow dependencies between services within remotely deployed distributed systems of services. Our work aims at elaborating for a concrete system, which parts of the system (or system model) are necessary to check a given property. The approach allows services decomposition oriented towards efficient checking of syst… ▽ More This paper presents a formal approach to modelling and analysis of data and control flow dependencies between services within remotely deployed distributed systems of services. Our work aims at elaborating for a concrete system, which parts of the system (or system model) are necessary to check a given property. The approach allows services decomposition oriented towards efficient checking of system properties as well as analysis of dependencies within a system. △ Less

Submitted 10 December, 2014; originally announced December 2014.

Comments: Preprint, The 2014 Asia-Pacific Services Computing Conference (APSCC 2014)

Cyber-Virtual Systems: Simulation, Validation & Visualization

Authors: Jan Olaf Blech, Maria Spichkova, Ian Peake, Heinz Schmidt

Abstract: We describe our ongoing work and view on simulation, validation and visualization of cyber-physical systems in industrial automation during development, operation and maintenance. System models may represent an existing physical part - for example an existing robot installation - and a software simulated part - for example a possible future extension. We call such systems cyber-virtual systems.… ▽ More We describe our ongoing work and view on simulation, validation and visualization of cyber-physical systems in industrial automation during development, operation and maintenance. System models may represent an existing physical part - for example an existing robot installation - and a software simulated part - for example a possible future extension. We call such systems cyber-virtual systems. In this paper, we present the existing VITELab infrastructure for visualization tasks in industrial automation. The new methodology for simulation and validation motivated in this paper integrates this infrastructure. We are targeting scenarios, where industrial sites which may be in remote locations are modeled and visualized from different sites anywhere in the world. Complementing the visualization work, here, we are also concentrating on software modeling challenges related to cyber-virtual systems and simulation, testing, validation and verification techniques for them. Software models of industrial sites require behavioural models of the components of the industrial sites such as models for tools, robots, workpieces and other machinery as well as communication and sensor facilities. Furthermore, collaboration between sites is an important goal of our work. △ Less

Submitted 6 October, 2014; originally announced October 2014.

Comments: Preprint, 9th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2014)

Formalisation and Analysis of Component Dependencies

Authors: Maria Spichkova

Abstract: This set of theories presents a formalisation in Isabelle/HOL+Isar of data dependencies between components. The approach allows to analyse system structure oriented towards efficient checking of system: it aims at elaborating for a concrete system, which parts of the system (or system model) are necessary to check a given property. This set of theories presents a formalisation in Isabelle/HOL+Isar of data dependencies between components. The approach allows to analyse system structure oriented towards efficient checking of system: it aims at elaborating for a concrete system, which parts of the system (or system model) are necessary to check a given property. △ Less

Submitted 12 May, 2014; originally announced May 2014.

Comments: Preprint with an extended introduction, Archive of Formal Proofs, 2014, ISSN: 2150-914x

Compositional properties of crypto-based components

Authors: Maria Spichkova

Abstract: This paper presents an Isabelle/HOL+Isar set of theories which allows to specify crypto-based components and to verify their composition properties wrt. cryptographic aspects. We introduce a formalisation of the security property of data secrecy, the corresponding definitions and proofs. This paper presents an Isabelle/HOL+Isar set of theories which allows to specify crypto-based components and to verify their composition properties wrt. cryptographic aspects. We introduce a formalisation of the security property of data secrecy, the corresponding definitions and proofs. △ Less

Submitted 12 May, 2014; originally announced May 2014.

Comments: Preprint. Archive of Formal Proofs, 2014, ISSN: 2150-914x

Stream processing components: Isabelle/HOL formalisation and case studies

Authors: Maria Spichkova

Abstract: This set of theories presents an Isabelle/HOL+Isar formalisation of stream processing components introduces in Focus, a framework for formal specification and development of interactive systems. This is an extended and updated version of the formalisation, which was elaborated within the methodology 'Focus on Isabelle'. In addition, we also applied the formalisation on three case studies that cove… ▽ More This set of theories presents an Isabelle/HOL+Isar formalisation of stream processing components introduces in Focus, a framework for formal specification and development of interactive systems. This is an extended and updated version of the formalisation, which was elaborated within the methodology 'Focus on Isabelle'. In addition, we also applied the formalisation on three case studies that cover different application areas: process control (Steam Boiler System), data transmission (FlexRay communication protocol), memory and processing components (Automotive-Gateway System). △ Less

Submitted 7 May, 2014; originally announced May 2014.

Comments: Preprint with an extended introduction

Journal ref: Archive of Formal Proofs, 2013, ISSN: 2150-914x

Do we really need to write documentation for a system? CASE tool add-ons: generator+editor for a precise documentation

Authors: Maria Spichkova, Xiuna Zhu, Dongyue Mou

Abstract: One of the common problems of system development projects is that the system documentation is often outdated and does not describe the latest version of the system. The situation is even more complicated if we are speaking not about a natural language description of the system, but about its formal specification. In this paper we discuss how the problem could be solved by updating the documentatio… ▽ More One of the common problems of system development projects is that the system documentation is often outdated and does not describe the latest version of the system. The situation is even more complicated if we are speaking not about a natural language description of the system, but about its formal specification. In this paper we discuss how the problem could be solved by updating the documentation automatically, by generating a new formal specification from the model if the model is frequently changed. △ Less

Submitted 29 April, 2014; originally announced April 2014.

Comments: In Proceedings International Conference on Model-Driven Engineering and Software Development (MODELSWARD'13)

Refinement-Based Specification: Requirements and Architecture

Authors: Maria Spichkova

Abstract: This paper presents the methodology for the system requirements and architecture w.r.t. their decomposition and refinement. It also introduces ideas of refinement layers and of refinement-based verification. This paper presents the methodology for the system requirements and architecture w.r.t. their decomposition and refinement. It also introduces ideas of refinement layers and of refinement-based verification. △ Less

Submitted 29 April, 2014; originally announced April 2014.

Comments: In Software Engineering 2011 (SE)

Human Factors of Formal Methods

Authors: Maria Spichkova

Abstract: This paper provides a brief introduction to the work that aims to apply the achievements within the area of engineering psychology to the area of formal methods, focusing on the specification phase of a system development process. This paper provides a brief introduction to the work that aims to apply the achievements within the area of engineering psychology to the area of formal methods, focusing on the specification phase of a system development process. △ Less

Submitted 29 April, 2014; originally announced April 2014.

Comments: Preprint. Final version published in Proceedings of IADIS International Conference Interfaces and Human Computer Interaction 2012 (IHCI 2012), 2012

Towards system development methodologies: From software to cyber-physical domain

Authors: Maria Spichkova, Alarico Campetelli

Abstract: In many cases, it is more profitable to apply existing methodologies than to develop new ones. This holds, especially, for system development within the cyber-physical domain: until a certain abstraction level we can (re)use the methodologies for the software system development to benefit from the advantages of these techniques. In many cases, it is more profitable to apply existing methodologies than to develop new ones. This holds, especially, for system development within the cyber-physical domain: until a certain abstraction level we can (re)use the methodologies for the software system development to benefit from the advantages of these techniques. △ Less

Submitted 12 March, 2014; originally announced March 2014.

Comments: First International Workshop on Formal Techniques for Safety-Critical Systems 2012 (FTSCS 2012), ICFEM 2012 Satellite Event

MSC Class: 68M15

Towards Focus on Time

Authors: Maria Spichkova

Abstract: This short paper introduces a model for the specification and verification of real-time system design: timed state transition diagrams. This short paper introduces a model for the specification and verification of real-time system design: timed state transition diagrams. △ Less

Submitted 5 March, 2014; originally announced March 2014.

Comments: 12th International Workshop on Automated Verification of Critical Systems (AVoCS'12), 2012

MSC Class: 68Q60

From abstract modelling to remote cyber-physical integration/interoperability testing

Authors: Maria Spichkova, Heinrich Schmidt, Ian Peake

Abstract: An appropriate system model gives developers a better overview, and the ability to fix more inconsistencies more effectively and earlier in system development, reducing overall effort and cost. However, modelling assumes abstraction of several aspects of the system and its environment, and this abstraction should be not overlooked, but properly taken into account during later development phases. T… ▽ More An appropriate system model gives developers a better overview, and the ability to fix more inconsistencies more effectively and earlier in system development, reducing overall effort and cost. However, modelling assumes abstraction of several aspects of the system and its environment, and this abstraction should be not overlooked, but properly taken into account during later development phases. This is especially especially important for the cases of remote integration, testing/verification, and manufacturing of cyber-physical systems. For this reason we introduce a development methodology for cyber-physical systems (CPS) with a focus on the abstraction levels of the system representation, based on the idea of refinement-based development of complex, interactive systems. △ Less

Submitted 30 April, 2014; v1 submitted 4 March, 2014; originally announced March 2014.

Comments: In Improving Systems and Software Engineering Conference (iSSEC) 2013 incorporating SEPG(SM) Asia-Pacific Conference, 2013

Verified System Development with the AutoFocus Tool Chain

Authors: Maria Spichkova, Florian Hölzl, David Trachtenherz

Abstract: This work presents a model-based development methodology for verified software systems as well as a tool support for it: an applied AutoFocus tool chain and its basic principles emphasizing the verification of the system under development as well as the check mechanisms we used to raise the level of confidence in the correctness of the implementation of the automatic generators. This work presents a model-based development methodology for verified software systems as well as a tool support for it: an applied AutoFocus tool chain and its basic principles emphasizing the verification of the system under development as well as the check mechanisms we used to raise the level of confidence in the correctness of the implementation of the automatic generators. △ Less

Submitted 10 July, 2012; originally announced July 2012.

Comments: In Proceedings WS-FMDS 2012, arXiv:1207.1841

ACM Class: D.2.1; D.2.2; D.2.4

Journal ref: EPTCS 86, 2012, pp. 17-24