Until recently the game industry heavily relied on manual playtesting to test the games it produces. Even if the benefits of introducing automated testing are acknowledged, it is rarely done in practice. Some of the main hurdles include the lack of automated testing tools that can target computer games as well as the complexity of automated game plays which are much more difficult to program than typical simple test sequences. This article presents an agent-based testing framework called aplib that comes with a Domain Specific Language (DSL) that allows complex playtests to be programmed more abstractly. A so-called goal structure is used to abstractly formulate a playtest scenario in terms of main goals and their decomposition into subgoals. Scenarios that are not too complicated can be formulated using static goal structures. More complex scenarios may need a test agent that can dynamically adapt its play according to the situation that evolves during the play. To handle such cases, aplib allows dynamic goals to be expressed as well. Invariants and pre-/post-conditions are used to assert the properties that a play is expected to satisfy. They include differential properties that allow constraints on the current state to be related to that of past states. Three case studies are included in the article. The first one aims to evaluate the performance of playtests programmed with aplib . The second shows that the approach can also be combined with other automated testing approaches, in this case reinforcement learning. The third shows the applicability of such playtests in a 3D setup and for non-functional testing.

Computer 3D games are complex software environments that require novel testing processes to ensure high-quality standards. The Intelligent Verification/Validation for Extended Reality Based Systems ( iv4XR ) framework addresses this need by enabling the implementation of autonomous agents to automate game testing scenarios. This framework facilitates the automation of regression test cases for complex 3D games like Space Engineers. Nevertheless, the technical expertise required to define test scripts using iv4XR can constrain seamless collaboration between developers and testers. This paper reports how integrating a Behavior-Driven Development (BDD) approach with the iv4XR framework allows the industrial company behind Space Engineers to automate regression testing. The success of this industrial collaboration has inspired the iv4XR team to integrate the BDD approach to improve the automation of play-testing for the experimental 3D game LabRecruits. Furthermore, the iv4XR framework has been extended with tactical programming to enable the automation of long-play test scenarios in Space Engineers. These results underscore the versatility of the iv4XR framework in supporting diverse testing approaches while showcasing how BDD empowers users to create, manage, and execute automated game tests using comprehensive and human-readable statements.

As the game industry continues to evolve in pop-ularity, testing the experience of players becomes crucial for attracting and retaining players in the highly competitive market. However, the absence of automated methods for articulating and verifying player experience (PX) specifications led us to introduce EmoSTL, a specialized language that extends Linear Temporal Logic with spatial and time-interval expressions, enabling the capture of complex temporal and spatial aspects of players' emotions and their experiences within games. We conducted a user study to collect suggestive PX requirements for a game under test to assess the capabilities of EmoSTL. Findings reveal that the language formalizes 92 percent of the set PX requirements, and with runtime verification, several PX design issues are iden-tified in the game. Moreoever, EmoSTL performance evaluation demonstrates its linear execution time, showcasing the language potential usage in automated PX testing of games.

As video games become more complex and widespread, player experience (PX) testing becomes crucial in the game industry. Attracting and retaining players are key elements to guarantee the success of a game in the highly competitive market. Although a number of techniques have been introduced to measure the emotional aspect of the experience, automated testing of player experience still needs to be explored. This paper presents PX-MBT, a framework for automated player experience testing with emotion pattern verification. PX-MBT (1) utilizes a model-based testing approach for test suite generation, (2) employs a computational model of emotions developed based on a psychological theory of emotions to model players' emotions during game-plays with an intelligent agent, and (3) verifies emotion patterns given by game designers on executed test suites to identify PX-issues. We explain PX-MBT architecture and provide an example along with its result in emotion pattern verification, which asserts the evolution of emotions over time, and heat-maps to showcase the spatial distribution of emotions on the game map.

Abstract Player eXperience (PX) testing has attracted attention in the game industry as video games become more complex and widespread. Understanding players’ desires and their experience are key elements to guarantee the success of a game in the highly competitive market. Although a number of techniques have been introduced to measure the emotional aspect of the experience, automated testing of player experience still needs to be explored. This paper presents a framework for automated player experience testing by formulating emotion patterns’ requirements and utilizing a computational model of players’ emotions developed based on a psychological theory of emotions along with a model-based testing approach for test suite generation. We evaluate the strength of our framework by performing mutation test. The paper also evaluates the performance of a search-based generated test suite and LTL model checking-based test suite in revealing various variations of temporal and spatial emotion patterns. Results show the contribution of both algorithms in generating complementary test cases for revealing various emotions in different locations of a game level.

Abstract In model-based testing, we may have to deal with a non-deterministic model, e.g. because abstraction was applied, or because the software under test itself is non-deterministic. The same test case may then trigger multiple possible execution paths, depending on some internal decisions made by the software. Consequently, performing precise test analyses, e.g. to calculate the test coverage, are not possible.. This can be mitigated if developers can annotate the model with estimated probabilities for taking each transition. A probabilistic model checking algorithm can subsequently be used to do simple probabilistic coverage analysis. However, in practice developers often want to know what the achieved aggregate coverage is, which unfortunately cannot be re-expressed as a standard model checking problem. This paper presents an extension to allow efficient calculation of probabilistic aggregate coverage, and also of probabilistic aggregate coverage in combination withk-wise coverage.

Few if any would dispute that educating software engineering is a challenging endeavour. Although programming and creating new artefacts can motivate the creativity of students. Other software engineering topics (like e.g. requirement specifications and testing) are not considered very exciting by students. However, these topics are important to develop quality software and insufficient knowledge of students - Europe's future software engineers - in the long run contributes to failing software. The EU Erasmus+ project IMPRESS was set to explore the use of gamification in educating software engineering at the university level. The objective has been to develop a toolset that can help to improve students' engagement, and hence their appreciation, for the taught subjects like software testing and specifications. The proposed tutorial will guide participants through the set of tools developed by the project and introduce how they can use them to improve students' engagement.

Testing for quality assurance (QA) is a crucial step in the development of Extended Reality (XR) systems that typically follow iterative design and development cycles. Bringing automation to these testing procedures will increase the productivity of XR developers. However, given the complexity of the XR environments and the User Experience (UX) demands, achieving this is highly challenging. We propose to address this issue through the creation of autonomous cognitive test agents that will have the ability to cope with the complexity of the interaction space by intelligently explore the most prominent interactions given a test goal and support the assessment of affective properties of the UX by playing the role of users.

This paper presents a case study on applying two model checkers, Spin and Divine, to verify key properties of a C++ software framework, known as ADAPRO, originally developed at CERN. Spin was used for verifying properties on the design level. Divine was used for verifying simple test applications that interacted with the implementation. Both model checkers were found to have their own respective sets of pros and cons, but the overall experience was positive. Because both model checkers were used in a complementary manner, they provided valuable new insights into the framework, which would arguably have been hard to gain by traditional testing and analysis tools only. Translating the C++ source code into the modeling language of the Spin model checker helped to find flaws in the original design. With Divine, defects were found in parts of the code base that had already been subject to hundreds of hours of unit tests, integration tests, and acceptance tests. Most importantly, model checking was found to be easy to integrate into the workflow of the software project and bring added value, not only as verification, but also validation methodology. Therefore, using model checking for developing library-level code seems realistic and worth the effort.

The popularity of JavaScript (JS) is enormous. Together with HTML and CSS, it is the core technology for modern web development. Because of the dynamic nature and complex interplay with HTML, JS applications are often error-prone and vulnerable. Despite active research efforts to devise intricate static and dynamic analyses to facilitate JS testing, the problem of test data generation for JS code interacting with the DOM has not yet been addressed. In this paper, we present a Javascript Evolutionary testing framework with DOM as an Input, called JEDI. In order to reach a target branch, it applies genetic search for relevant input parameters of the JS function in combination with the global DOM state. We conducted an empirical evaluation to study the effectiveness and efficiency of our testing framework. It shows that the genetic with restart algorithm, proposed in this paper, is able to achieve complete branch coverage for all experimental subjects, taking on average 19 seconds per branch.

In this paper, we apply fine-grained slicing techniques to the models generated from the Rebel modeling language before passing them on to an SMT solver. We show that our slicing techniques have a significant positive effect on performance, allowing us to verify larger problem instances and with higher path bounds than with unsliced models. For small and shallow instances, however, the overhead of slicing dominates verification time, and slicing should not be resorted to.

Summary Mobile gaming is already a popular and lucrative market. However, the low performance and reduced power capacity of mobile devices severely limit the complexity of mobile games and the duration of their game sessions. To mitigate these issues, in this article, we explore using computation‐offloading, that is, allowing the compute‐intensive parts of mobile games to execute on remote infrastructure. Computation‐offloading raises the combined challenge of addressing the trade‐offs between performance and power‐consumption while also keeping the game playable. We propose Mirror, a system for computation‐offloading that supports the demanding performance requirements of sophisticated mobile games. Mirror proposes several conceptual contributions: support for fine‐grained partitioning, both offline (set by developers) and dynamic (policy‐based), and real‐time asynchronous offloading and user‐input synchronization protocols that enable Mirror‐based systems to bound the delays introduced by offloading and thus to achieve adequate performance. Mirror is compatible with all games that are tick‐based and user‐input deterministic. We implement a real‐world prototype of Mirror and apply it to the real‐world, complex, popular game OpenTTD. The experimental results show that, in comparison with the non‐offloaded OpenTTD, Mirror‐ed OpenTTD can significantly improve performance and power consumption while also delivering smooth gameplay. As a trade‐off, Mirror introduces acceptable delay on user inputs.

The low performance and power limitations of mobile devices severely limit the complexity and the duration of playing sessions of mobile games. This article examines the possibility of using computation-offloading to mitigate these problems while keeping the game playable. We design Mirror, a framework for offloading computation targeted at the demanding performance requirements of sophisticated mobile games. The key conceptual contributions of Mirror are design decisions that allow for dynamic fine-grained client-side offloading decisions, and a protocol for real-time asynchronous offloading for bounding network delays. We implement a prototype of Mirror and test it by performing offloading for the game OpenTTD. The results are promising, showing that Mirror can increase the performance and decrease the power consumption of games while keeping the gameplay fairly smooth.

Agent-based Modeling (ABM) has become quite popular to the simulation community for its usability and wide area of applicability. However, speed is not usually a trait that ABM tools are characterized of attaining. This paper presents HLogo, a parallel variant of the NetLogo ABM framework, that seeks to increase the performance of ABM by utilizing Software Transactional Memory and multi-core CPUs, all the while maintaining the user friendliness of NetLogo. HLogo is implemented as a Domain Specific Language embedded in the functional language Haskell, which means that it also inherits Haskell,s features, such as its static typing. © Copyright 2016 by SCITEPRESS - Science and Technology Publications, Lda. All rights reserved.

Programs often contain branches to break off from their main execution. These branches contribute to the total cost of testing, because they also need to be tested. The paper presents a new approach to improve the testing of such branches by annotating them. Our tool automatically generates test-sequences. Then, invariants in the form of pre-and post-condition over the executions passing each annotated branch are dynamically inferred, and reported to the programmer for inspection. Contradiction with the programmer's assumption on what the behavior should be indicates a bug. As invariants, a certain class of simple expressions are proposed, which are discriminative enough for testing break-off behavior, while keeping their amount feasible for inspection.

T3i is an automated unit-testing tool to test Java classes. To expose interactions T3i generates test-cases in the form of sequences of calls to the methods of the target class. What separates it from other testing tools is that it treats test suites as first class objects and allows users to e.g. combine, query, and filter them. With these operations, the user can construct a test suite with specific properties. Queries can be used to check correctness properties. Hoare triples, LTL formulas, and algebraic equations can be queried. T3i can be used interactively, thus facilitating more exploratory testing, as well as through a script. The familiar Java syntax can be used to control it, or alternatively one can use the much lighter Groovy syntax.

This paper presents an automatic trace-based unit testing approach to test object-oriented programs. Most automated testing tools test a class C by testing each of its methods in isolation. Such an approach works poorly if specifications are only partial, which is usually the case in practice. In contrast, our approach generates sequences of calls to the methods of C that are checked on-the-fly. This is more interactive, and has the side effect that methods are checking each other. Although simple, it seems to work quite well, even when specifications are only partially provided. We implement the approach in a tool called T2. It targets Java. It can test internal errors, Hoare triple specifications, class invariant, and even temporal properties. Furthermore, T2 accepts ’in-code’ specifications, these are specifications written in the specified class itself, and are written in plain Java; hence reducing the cost usually needed to maintain specifications to minimum.

This paper describes a technique that combines algebraic datatypes and monads to build derivative verification condition generators (VCGs) by extending a base VCG. Extensions are compositional and can be stacked while the base VCG is left unchanged. The technique can be used to build a set of weaker VCGs to do light weight verification. Moreover, it enables us to add an ability to generate validation traces. The paper explains the technique through an example that extends a simple language L/sub 0/ with new constructs to handle exceptions. To deal with exceptions, not only the logic of L/sub 0/ has to be extended with new rules, its structure also needs to be changed. We show that using our technique the extension can be implemented in a simple and compositional way, without any change to the underlying logic.

Abstract UNITY, introduced by Chandy and Misra [ChM88], is a programming logic intended to reason about temporal properties of distributed programs. Despite the fact that UNITY does not have the full power of, for example, linear temporal logic, it enjoys popularity due to its simplicity. There was however a serious problem with the Substitution Rule. The logic is incomplete without the rule, and with the rule it is inconsistent. Latterly Beverly Sanders introduced the concept of strongest invariant and proposed a new definition for UNITY [San91] that fixes the problem with the Substitution Rule. For the benefit of program union, she also introduced the concept of subscripted properties and claimed a generalized version of Substitution Rule for the subscripted properties. This report presents an example that shows that the latter claim is false. A proposal as how to fix this follows.