arXiv subjects

Maria Spichkova

Publications and source records attributed to Maria Spichkova.

At least 55 records · Page 3Linked to original sources

arXiv2017

From Temporal Models to Property-Based Testing

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.

cs.SE↗

arXiv2017

Online Support System for Transnational Education

The number of students who travel abroad to study or are enrolled in a distance learning program outside their home country is growing. According to UNESCO, such students are called internationally mobile students (IMSs) and 5 destination countries accounted for almost 50% of IMSs: United States (18%), United Kingdom (11%), France (7%), Australia (6%), and Germany (5%). Internationalisation of the higher education has created the so-called borderless university, providing better opportunities for learning and increases the human and social sustainability. In this paper, we propose an online system to support transnational education (TNE) in Australia. This system will consist of both an online module and quiz, and an automated assistance module. The first part will ensure that students understand TNE-related potential problems, such as the importance of submission deadlines, and provide students early hints and help to avoid the TNE-related problems. The second part will provide assistance with general issues related to studying and living in Australia, and more specific ones tailored to a specific institution. The ability to provide an immediate response when required will help overcome feelings of isolation, and provide appropriate advice on matters such as plagiarism and related issues, many of which arise from misunderstandings due to divergent cultural backgrounds and a lack of awareness about differences in socio-cultural environments.

physics.ed-ph↗

arXiv2017

Individual and Social Requirement Aspects of Sustainable eLearning Systems

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.

cs.CY↗

arXiv2016

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

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.

cs.SE↗

arXiv2016

Managing Usability and Reliability Aspects in Cloud Computing

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.

cs.SE↗

arXiv2016

Model-based generation of natural language specifications

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.

cs.SE↗

arXiv2016

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

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.

cs.LO↗

arXiv2016

Spatio-temporal features of FocusST

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.

cs.SE↗

arXiv2016

Applied Logic in Engineering

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.

cs.CY↗

arXiv2016

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

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.

cs.SE↗

arXiv2015

Model-based Hazard and Impact Analysis

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.

cs.SE↗

arXiv2015

Requirements Engineering Aspects of a Geographically Distributed Architecture

We present our ongoing work on requirements specification and analysis for the geographically distributed software and systems. Developing 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.

cs.SE↗

arXiv2015

Chiminey: Reliable Computing and Data Management Platform in the Cloud

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.

cs.SE↗

arXiv2015

Human Factors in Software Reliability Engineering

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.

cs.SE↗

arXiv2015

Reconciling a component and process view

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.

cs.SE↗

arXiv2014

Towards Logical Architecture and Formal Analysis of Dependencies Between Services

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.

cs.SE↗

arXiv2014

Cyber-Virtual Systems: Simulation, Validation & Visualization

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.

cs.SE↗

arXiv2014

Compositional properties of crypto-based components

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.

cs.CR↗