Search

Many very large-scale systems are networks of cyber-physical systems in which humans and autonomous software agents cooperate. To make the cooperation safe for the humans involved, the systems have to follow protocols with rigid real-time and real-space properties, but they also need to be capable of making competitive and collaborative decisions with varying rewards and penalties. Due to these tough requirements, the construction of system control software is often very difficult. This calls for applying a model-based engineering approach, which allows one to formally express the time and space properties and use them as guidance for the whole engineering process from requirement definition via system design to software development. Moreover, it is beneficial, if one can verify with acceptable effort, that the time and space requirements are preserved throughout the development steps. This paper focuses on modelling spatio-temporal properties and their model-checking and simulation using different analysis tools in combination with the methods and tool extensions proposed here. To this end, we provide an informal overview of CASTeL, our CASTeLogic. CASTeL is stochastic and includes real-time concurrency and real-space distribution., Comment: Preprint. Accepted to the 21th International Conference on Mobile and Ubiquitous Systems: Computing, Networking and Services (MobiQuitous 2024). Final version to be published by Springer (In Press)

Designing mobile software that aligns with cultural contexts is crucial for optimizing human-computer interaction. Considering cultural influences is essential not only for the actual set of functional/non-functional requirements, but also for the whole Requirement Engineering (RE) process. Without a clear understanding of cultural influences on RE activities, it's hardly possible to elaborate a correct and complete set of requirements. This research explores the impact of national culture on RE-related activities based on recent studies. We conducted a Systematic Literature Review (SLR) of studies published in 2019-2023 and compared them to an older SLR covering 2000-2018. We identified 17 relevant studies, extracted 33 cultural influences impacting RE activities, and mapped them to the Hofstede model, widely used for cultural analysis in software development research. Our work highlights the critical role of national culture in RE activities, summarizes current research trends, and helps practitioners consider cultural influences for mobile app/software development., Comment: Preprint. Accepted to the 26th International Conference on Mobile Human-Computer Interaction (MOBILEHCI Adjunct '24), September 30-October 3, 2024, Melbourne, Australia. ACM Digital Library. Final version to be published by ACM Digital Library (In Press)

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., Comment: 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)

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., Comment: 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

This work focuses on studying players behaviour in interactive narratives with the aim to simulate their choices. Besides sub-optimal player behaviour due to limited knowledge about the environment, the difference in each player's style and preferences represents a challenge when trying to make an intelligent system mimic their actions. Based on observations from players interactions with an extract from the interactive fiction Anchorhead, we created a player profile to guide the behaviour of a generic player model based on the BDI (Belief-Desire-Intention) model of agency. We evaluated our approach using qualitative and quantitative methods and found that the player profile can improve the performance of the BDI player model. However, we found that players self-assessment did not yield accurate data to populate their player profile under our current approach., Comment: CHI Play 2018

In this paper we present an early Apprenticeship Learning approach to mimic the behaviour of different players in a short adaption of the interactive fiction Anchorhead. Our motivation is the need to understand and simulate player behaviour to create systems to aid the design and personalisation of Interactive Narratives (INs). INs are partially observable for the players and their goals are dynamic as a result. We used Receding Horizon IRL (RHIRL) to learn players' goals in the form of reward functions, and derive policies to imitate their behaviour. Our preliminary results suggest that RHIRL is able to learn action sequences to complete a game, and provided insights towards generating behaviour more similar to specific players., Comment: Extended Abstracts of the 2019 Annual Symposium on Computer-Human Interaction in Play (CHI Play)

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., Comment: Preprint. Accepted to the 13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2018). Final version published by SCITEPRESS

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., Comment: Preprint. Paper accepted to ICEER 2016

The busy beaver problem is a well-known example of a non-computable function. In order to determine a particular value of this function, it is necessary to generate and classify a large number of Turing machines. Previous work on this problem has described the processes used for the generation and classification of these machines, but unfortunately has generally not provided details of the machines considered. While there is no reason to doubt the veracity of the results known so far, it is difficult to accept such results as scientifically proven without being able to inspect the appropriate evidence. In addition, a list of machines and their classifications can be used for other results, such as variations on the busy beaver problem and related problems such as the placid platypus problem. In this paper we investigate how to generate classes of machines to be considered for the busy beaver problem. We discuss the relationship between quadruple and quintuple variants of Turing machines, and show that the latter are more general than the former. We give some formal results to justify our strategy for minimising the number of machines generated, and define a process reflecting this strategy for generating machines. We describe our implementation, and the results of generating various classes of machines with up to 5 states or up to 5 symbols, all of which (together with our code) are available on the author's website.

The busy beaver is a well-known specific example of a non-computable function. Whilst many aspect of this problem have been investigated, it is not always easy to find thorough and convincing evidence for the claims made about the maximality of particular machines, and the phenomenal size of some of the numbers involved means that it is not obvious that the problem can be feasibly addressed at all. In this paper we address both of these issues. We discuss a framework in which the busy beaver problem and similar problems may be addressed, and the appropriate processes for providing evidence of claims made. We also show how a simple heuristic, which we call the observant otter, can be used to evaluate machines with an extremely large number of execution steps required to terminate. We also show empirical results for an implementation of this heuristic which show how this heuristic is effective for all known `monster' machines., Comment: This has been submitted to the Theoretical Computer Science journal

We consider the problem of searching for proofs in sequential presentations of logics with multiplicative (or intensional) connectives. Specifically, we start with the multiplicative fragment of linear logic and extend, on the one hand, to linear logic with its additives and, on the other, to the additives of the logic of bunched implications, BI. We give an algebraic method for calculating the distribution of the side-formulae in multiplicative rules which allows the occurrence or non-occurrence of a formula on a branch of a proof to be determined once sufficient information is available. Each formula in the conclusion of such a rule is assigned a Boolean expression. As a search proceeds, a set of Boolean constraint equations is generated. We show that a solution to such a set of equations determines a proof corresponding to the given search. We explain a range of strategies, from the lazy to the eager, for solving sets of constraint equations. We indicate how to apply our methods systematically to large family of relevant systems., Comment: Submission to ACM Transactions on Computational Logic