Abstract Requirements Engineering (RE) is a socio-technical process that relies on effective communication among stakeholders. Understanding how national cultural influences affect RE activities is crucial, given participants’ diverse cultural backgrounds. This paper presents a refined framework for identifying cultural influences (CIs) on RE-related activities and a web-based application developed to support it. The refined framework incorporates the latest Hofstede scores and covers nearly double the CIs compared to its earlier version. We evaluated the proposed framework against in-depth case studies from 8 countries (Australia, Thailand, China, Pakistan, South Korea, Saudi Arabia, Vietnam, and Bangladesh), where the CIs have been identified on the basis of surveys and interviews. Analysis showed the proposed framework consistently provided better coverage than the original. We extended the framework by assigning evidence-based confidence levels to each CIs based on the evaluation wrt. primary case studies. Our approach allows RE practitioners to evaluate and manage cultural impacts effectively. The framework provides a comprehensive analysis of national cultural influences and delivers more accurate and contextually relevant insights. The tool aids users in obtaining relevant national CIs, confidence levels, and summaries for a selected country. This enables stakeholders, practitioners, researchers, and educators to manage cultural dynamics effectively, enhancing RE-related activities.

The fashion and textiles industry is one of the most significant contributors to global carbon emissions and wastewater pollution. As a result, the fashion industry contributes significantly to climate change and water scarcity. Many studies have demonstrated that social networks and fast fashion marketing influence young people, often promoting unsustainable consumption habits. Environmental and green fashion education at all levels becomes imperative for dealing with this issue, as it promotes changes in consumer behaviour. In this paper, we propose to elaborate an e-Learning framework to teach children about sustainable fashion through interactive games, videos, and activities. This research will include focus group sessions and observation studies to investigate users’ perceptions and interaction patterns. The framework will provide equitable access to sustainability education and an outlook for future careers for children, which will help to address gaps in current educational resources and leverage technology to scale impact. This might be especially useful for children in rural and remote areas as well as children who face socioeconomic disadvantage. The future direction of research will include an analysis of interaction patterns with respect to learning results, as well as an evaluation of the impact of game activity types on the interest of learners in engaging in sustainable fashion.

In this paper, we discuss our experience in designing and teaching a course on Software Engineering Project Management, where the focus is on Agile/Scrum development and Requirement Engineering activities. The course has undergone fundamental changes since 2020 to make the teaching approach more student-centred and flexible. As many universities abandoned having face-to-face exams at the end of the semester, authentic assessments now play an even more important role than before. This makes assessment of students’ work even more challenging, especially if we are dealing with large cohorts of students. The complexity is not only in dealing with diversity in the student cohorts when elaborating the assessment tasks, but also in being able to provide feedback and marks in a timely and fairly. We report our lessons learned, which might provide useful insights for teaching Agile/Scrum concepts to undergraduate and postgraduate students. We also analyse what course structure might be effective to support a blended learning approach, as well as what could be a reasonable structure of online assessments, to keep them both authentic and scalable for large cohorts of students.

In Agile/Scrum software development, sprint planning and retrospective analysis are the key elements of project management. The aim of our work is to support software developers in these activities. In this paper, we present our prototype tool RetroAI++, based on emerging intelligent technologies. In our RetroAI++ prototype, we aim to automate and refine the practical application of Agile/Scrum processes within Sprint Planning and Retrospectives. Leveraging AI insights, our prototype aims to automate and refine the many processes involved in the Sprint Planning, Development and Retrospective stages of Agile/Scrum development projects, offering intelligent suggestions for sprint organisation as well as meaningful insights for retrospective refection.

Requirements Engineering (RE) is one of the most interaction-intensive phases of software development. This means that RE activities might be especially impacted by stakeholders’ national culture. Software development projects increasingly have a very diverse range of stakeholders. To future-proof RE activities, we need to help RE practitioners avoid misunderstandings and conflicts that might arise from not understanding potential Cultural Influences (CIs). Moreover, an awareness of CIs supports diversity and inclusion in the IT profession. Bangladesh has a growing IT sector with some unique socio-cultural characteristics, and has been largely overlooked in this research field. In this study, we aim to investigate how the RE process is adopted in the context of Bangladeshi culture and what cultural influences impact overall RE activities.

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 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 pro posed method shows how to combine general PBT with MT under the same testing framework.

Teaching of Software Engineering courses is challenging from many perspectives, where one of the key aspects is authentic assessment of the student work. Assessment of students’ work becomes especially challenging when we are dealing with large cohorts of students. The assessment typically should be done in a very short time frame, either to provide an early feedback within the semester or to allow for finalisation of the students’ grades for the course. Providing timely and comprehensive feedback is especially important during the semester, when students are more keen to improve their skills on the course topics. In this work we (1) analyse the level of correlation between students’ peer-review skills and their problem solving skills within Requirements Engineering activities, and (2) to what extent the students’ peer-feedback can be used to provide an early feedback within the semester or to mark students’ assessments.

This paper presents a systematic analysis of the existing studies in two research areas: (1) effects that animated objects might have on users, and (2) HCI studies with autistic users. The aim of this work is to broaden current knowledge of the effect of animation on user interface usability. We systematically analysed the state of the art in the related research areas and identified many gaps that should be addressed, as well as proposed the solution to cover these gaps. Our goal is to analyse the performance variance between neurotypical users and autistic individuals in order to gauge task achievement, webpage navigability, and ability to focus.

This paper presents the results of the project conducted within the Research embedded in teaching initiative in collaboration with NostraData. The main objective of the research was to analyse if the peak values of such weather conditions, like rainfall and wind speed, can impact the drug purchase transactions within shorts time periods (one, three, and five days) of time, after the peak values of the weather parameters have appeared. The basis for the automated analysis were the data collected over more than six years, restricted to the Melbourne region in Australia.

This paper presents a short overview of projects conducted at RMIT University in Melbourne, Australia, as a part of the learning and teaching activities in the Science, Technology, Engineering and Mathematics (STEM) College. The focus is on eHealth, bioengineering, biomedical engineering and related application areas. We introduce how these research areas are embedded into the curriculum, as well as, present a number of recent and current projects conducted by our students in collaboration with industrial partners, other academic institutions and medical practitioners.

Requirement Engineering (RE) is a socio-technical activity and it demands intensive communication with the stake-holders to elicit and model all requirements. As both national and organisational cultures influence the behaviour of the individuals and their work practices, they might also influence RE activities deeply. We propose an extension to a formal framework for identifying and analysing cultural influences that could impact RE activities: the aim is to apply the framework not only on the national culture level, but expand it to the level of organisational culture to provide a more nuanced approach.

Requirements Engineering (RE) activities require intensive communication to capture clients' requirements. As culture influences the way in which people communicate and interact, individuals' culture might influence the implementation of RE activities. In this paper, we discuss the differences between formal approach (using the framework we propose) and case-study-based approaches for the identification of cultural influences in RE. We compared the results of the application of our framework with the results of case studies conducted by other researchers from several cultures. The results showed that the framework provided a much higher degree of precision than expected: the framework identified almost all of the cultural influences mentioned in the identified cases studies. This provides evidence of the accuracy and validity of our framework, which can provide similar conclusions based on information about the cultures involved rather than in-depth analysis.

This paper presents an automated solution for security vulnerability scanning of Google Cloud Platform (GCP) projects, to cover gaps in the capabilities of solutions to scan GCP projects for common security issues. The elaborated security inspection tool, GoSecure, can scan multiple GCP instances against industry recognised Center for Internet Security (CIS) benchmarks for GCP. GoSecure covers all categories listed under the CIS benchmarks for GCP, providing an overview of the existing security profile of all GCP projects, along with suggestions for improvement in configurations for the individual projects.

This paper presents a study on automated reading of utility meters using two computer vision techniques: an open-source solution Tensorflow Object Detection (Tensorflow) and a commercial solution Anyline. We aimed to identify the 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. Copyright

Requirements Engineering (RE) is a critical process in the development of any software. It requires intensive communication among many stakeholders in order to identify software requirements accurately. As RE activities require intensive communication, cultural influences might need to be considered to improve these activities and to avoid issues that might affect the software project outcomes. In our work, we explored the influence of national culture on RE activities. We conducted an empirical study in two countries that have different cultural profiles: Saudi Arabia and Australia. To explore this issue, we conducted 41 face-to-face interviews. To consolidate the collected data, we conducted also 30 follow-up interviews with the same practitioners. The aim of our study was to empirically identify the set of cultural influences affecting RE activities, and analyse their implication on RE activities. This paper reports the results of the analysis of participants’ responses with respect to their industrial profiles, in terms of three factors: the type of software methodology applied by the participants (Traditional vs. Agile), the size of their company/organisation (small, medium, and large), and its type (private vs. government). The results showed a number of significant differences in the cultural influences that determine the type of software development methodology, i.e., Traditional or Agile, being applied within the corresponding company. In this paper, we discuss the identified differences and the factors that determine them. This in-depth analysis provides a broader examination of the influence of culture on RE activities, which might assist RE practitioners to select the most suitable RE practices/methodology to overcome any negative effects of these influences.

The goal of this work is to elaborate a lightweight solution to manage multiple Amazon Web Services (AWS) accounts in one place. Currently, no such system is available. In this paper, we present a system that solves this task and allows to visualise the usage of AWS services across a number of customer’s accounts. This system can be also used to enable optimisation cost and performance of the AWS services across the customer’s accounts.

Setting up a virtual machine (VM) in the cloud is a time-consuming task. Typically, VMs are created from so called VM images, a kind of blueprints used to configure and create a VM. However, to create a VM image manually might be very time-consuming, especially if the VM has to meet certain security benchmarks. In this paper, we present VM2 (Virtual Machine Vending Machine), a tool for creation of VM images and testing them wrt. security benchmarks as well as easy sharing the secure images. Our analysis demonstrated a significant reduction in security issues in hardened images created by VM2 in comparison with corresponding publicly available images. Moreover, our tool provided better results wrt. CIS benchmarks in comparison with the corresponding images commercially offered by CIS.

Requirements Engineering (RE) activities require intensive communication among different stakeholders and an understanding of their behaviour in order to accurately identify requirements. As RE requires intensive communication, an individual's culture might influence RE activities. Thus, cultural influences affecting RE activities might need to be considered to improve RE activities and prevent issues that might affect software project outcomes. In our work, we propose a framework for identifying cultural factors that could influence RE activities. In this paper, we present the preliminary results of a case study conducted with Vietnamese practitioners.

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.

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.

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.

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.

Teaching of Software Engineering is challenging, especially when dealing with large cohorts of students, as well as cohorts with the diversity in the students' backgrounds, workloads and availabilities for face-to-face study. Especially challenging it becomes when we aim not only to provide necessary theoretical knowledge, but also to improve students' employability by making the projects really industry-oriented. This paper presents our experience on the redesign of Software Engineering project course to meet the above challenges, the lessons learned and the feedback from the students. The course is provided for both Bachelor and Master students at their final year of study, so our goal is to make students work-ready and to provide opportunities for networking with local and global companies, as well as other university disciplines.

Requirements Engineering (RE) activities are inherently collaborative, requiring software stakeholders to have intensive communication to identify users’ requirements. As the stakeholders’ culture might heavily impact on the way how they collaborate and communicate, RE might be significantly influenced by their cultural background. To analyse stakeholders’ culture, we use one of the most adopt and comprehensive cultural studies in software engineering: Hofstede’s cultural model. Hofstede’s model has six cultural dimensions, where one of them is Power Distance (PD). The aim of this study is to explore the influence of PD cultural aspects on RE activities. We conducted 32 interviews with software developments/requirements engineer practitioners from two different cultures: Saudi Arabia and Australia. Our results revealed that PD significantly affect RE collaboration among software stakeholders. In this paper, we address the core identified cultural aspects as well as the ways to overcome them. The results that we present in this paper would help to increase awareness of the influence of PD, and thus, improve collaboration within RE activities.

The paper presents an open source platform to integrate and analyse the cannabinoids research data gathered from academic publications, industrial and clinical trials as well as patients. The project focuses on the analysis of the usability aspects important for the applications collecting the treatment data as well as data on diverse cannabinoids strains. The collected data will be used to estimate the efficiency of cannabinoid treatment of various disorders, which will provide an evidence-based assistance for doctors, researchers and industry to identify the right cannabinoid profiles for various conditions.

Retrospective (retro) sessions are an important part of Agile/Scrum process for software development. In theory, conducting retro sessions each sprint should improve team dynamics and productivity. In praxis, retro sessions also have some disadvantages/hurdles that are hard to overcome: they are non-anonymous and time consuming. The goal of our project, conducted in collaboration between Shine Solutions and RMIT University, is to analyse the existing hurdles from industry-prospective and to provide an AI-based solution to overcome them. The two main outcomes of the project are (1) a web-based solution to support retro-sessions, and (2) a qualitative analysis of two speech recognition tools, Google Home and Amazon Alexa, to be connected with the elaborated solution to populate the retro board and help in time boxing a retro by using voice activated commands.

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.

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.

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.

The Requirements Engineering (RE) process is crucial for identifying users' requirements and the success of the software development process. As RE is a socio-technical activity in nature, an individuals' culture might influence its activities deeply. The aim of this study is to observe and evaluate the influence of culture on the RE process. In total, we conducted 16 interviews with requirements engineer practitioners in Saudi Arabia and Australia. We found that both cultures have an impact on the RE process. This paper describes the lessons learned from practice on how to improve RE practices, taking into account cultural aspects.

Many businesses prefer to run their web application in a cloud, as this provides an access to large numbers of computing and storage resources. To run a web application in a cloud, a virtual environment with the corresponding technology stack has to be created. The interfaces provided by cloud services (Amazon Web Services, Microsoft Azure, etc.) require micromanagement of all individual components. This makes the management of technology stacks an extremely time consuming and complex task, which involves a high degree of expertise. We present here SMI, a stack management interface that let you think about your cloud infrastructure as stacks of cloud technologies and enables moderately experienced users to manage the stacks as a whole.

This paper introduces the core results of the project conducted at RMIT University. 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. The proposed system would save students time and effort in travelling around the NAS precinct. Additionally, the system would improve students’ study productivity because they could minimise the risk of coming late to their classes. This will lead to increased students’ satisfaction level towards RMIT facilities, because they would be able to utilise the provided facilities efficiently.

The paper presents a SuSoftPro tool for requirement engineers to analyse the requirements' impacts on system sustainability. To perform the analysis of system sustainability, the tool provides quantitative questionnaires for rating high-level requirements within sustainability dimensions via a Fuzzy Rating Scale method. Stakeholders' responses are analysed by applying Technique for Order Preference by Similarity to Ideal Solution. The tool presents sustainability as a five-star rating label, a visualisation of the degree for sustainability dimensions, and a bar graph that illustrates the sustainability level.

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.

This paper presents an approach for modelling and implementation of autonomous humanoid system’s behaviour. The main objective of our project was to analyse possible interaction scenarios between humans and autonomous robots, and to elaborate a framework for providing flexible guided tour options, utilising the features of humanoid PAL REEM robot. The framework can be used to support guided tours through exhibitions, museums, art centres, innovative labs, etc. We introduce the core results of the project and briefly discuss our future work. There are many scenarios where humans interactively conduct some joint activities. Using our approach, presented here, one of the parties could be replaced by humanoid robots. State of the art technology in voice recognition and generation, as well as path planning were used to achieve requested research objectives.

A failure in safety-critical systems, such as vehicles, aircrafts, etc., may endanger human lives. It is crucial that these system behave correctly, in accordance to their specification and fulfilling all the safety-critical properties defined for them. Safety could be guaranteed through the application of analysis techniques, in the form of formal verification and testing. However, verification of a real-size system means having a large number of lemmas, depending on each other. An update in one lemma might require changes in many other lemmas. It would be inefficient to find the existing dependencies out when the proof process is already running. We present a methodology for analysis of the dependencies between lemmas within the provided set of proofs. The application of this methodology to the Isabelle/HOL theories is supported by a tool. The tool provides a quick automated analysis and easy-to-check representation of the results, as well as allows optimisation of the provided set of proofs.

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 opensource 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 co mputing and data management, as well as user-friendly interface.

This paper presents AHR, a formal framework for combinatorial test design that is Agile, Human-centred and Refinement-oriented. The framework (i) allows us to reuse test plans developed for an abstract level at more concrete levels; (ii) has human-centric interface providing queries and alerts whenever the specified test plan is incomplete or invalid; (iii) involves analysis of the testing constraints within combinatorial testing.

The use of Formal Methods (FMs) offers rigour and precision, while reducing ambiguity and inconsistency. The major barriers hindering the adoption of FMs in industry are the problems of understandability, comprehensibility, and scalability. To solve the understandability problem, from one side, the readability of the method have to be increased, but from another side, an appropriate teaching and learning approach have to be introduced. This paper presents an overview of existing approaches on teaching of FMs and Logic, also discusses the common issues in teaching of this subjects.

In this paper we address particular aspects of integration of formal methods in large-scale industrial projects, namely collaborative aspects. We review recent works addressing such aspects, identify some current trends and discuss directions for further research.

This paper presents an approach for an intelligent speed validation and adaptation. The approach focuses on formal modelling of the corresponding smart vehicle units, to increase the road safety as well as to allow formal analysis of the smart vehicle behaviour. We suggest a number of models for speed check/limitation units, which reflect differences in the speed limits in several countries. We also present our results from the case studies, based on two implementations of the model as an iOS and an Android app for Intelligent Speed Adaptation.

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.

This paper presents a formal model for science clouds, capable of predicting and controlling resources scalably, as well as its implementation as an open source solution, called Chiminey. The feasibility of Chiminey is shown using case studies on biophysics and structural chemistry computations. Big data is acquired from scientific instruments such as synchrotrons and atomic force microscopes. The model takes into account the architecture of the overall parallel and distributed system including large-scale data sources; data sinks, for example petabyte research data stores; and cluster or cloud virtual resources and infrastructures characterised by users in simple parameters upfront. Chiminey is developed to control large numbers of processes and to provide a reliable computing and data management, which can be used by researchers without having to learn extensive infrastructure concepts and technologies.

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.

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.

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.

This paper presents an approach towards intelligent route planning in public transport systems. The approach focuses on formal modelling of the semi-dynamic intelligent route planning and optimisation. For these purposes, it is essential to have a well de- veloped formal model covering real-time and space aspects. The proposed solution allows designers to extend a public transport system with additional routes, which are created dynamically based on the requests from passengers. The model can be applied within a sustainable Smart City both for (fully or partially) autonomous transport systems and for the decision support systems of a smart transport system.

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.

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.

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.

Abstract Formal verification of software systems is a challenge that is particularly important in the area of safety-critical automotive systems. Here, approaches like direct code verification are far too complicated, unless the verification is restricted to small textbook examples. Furthermore, the verification of application logic is of limited use in industrial context, unless the underlying operating system and the hardware are verified, too. This paper introduces a generic model stack, allowing the verification of all system layers as well as the concrete application models being used in the upper layers. The presented models and proofs close the gap between the correctness proof for the lower layers of car electronics developed at the Saarland University and the verification procedure for distributed applications developed at the Technische Universität München.