Multiplayer computer games play a big role in the ever-growing entertainment industry. Being competitive in this industry means releasing the best possible software, and reliability is a key feature to win the market. Computer games are also actively used to simulate different robotic systems where reliability is even more important, and potentially critical. Traditional software testing approaches can check a subset of all the possible program executions, and they can never guarantee complete absence of errors in the source code. On the other hand, during more than twenty years, Model Checking has demonstrated to be a powerful instrument for formal verification of large hardware and software components. In this paper, we contribute with a novel approach to formally verify computer games. We propose a method of model construction that starts from a computer game description and utilizes Model Checking technique. We apply the method on a case study: the game Penguin Clash. Finally, an approach to game model reduction (and its implementation) is introduced in order to address the state explosion problem.
Robotic system can consist of interacting intelligent components or agents. Such systems are called multi-agent. Gaia methodology was introduced in @cite_18 in order to provide an instrument for building a model of the multi-agent system from its specification. The model is based on role notion with attached responsibilities, permissions and activities. Responsibilities are introduced in order to specify goals of each role reaching which guarantees liveness (something good eventually happen) or safety (something bad never happens) properties of the multi-agent system. Target model gives high level understanding of the system and can help to insure logical correctness but does not impact significantly on reliability of the code.
@cite_18
2110101488
The emergence of multi-agent systems in the past years has led to the development of new methodologies to assist in the requirements and architectural analysis, as well as in the design phases of such systems. Consequently, several Agent Oriented Software Engineering (AOSE) methodologies have been proposed. In this paper, we analyze some AOSE methodologies, including Gaia, which supports the architectural design stage, and some proposed extensions. We then use an adapted version of this methodology to design an abstract generic system meta-model for a multi-robot application, which can be used as a basis for the design of these systems, avoiding or shortening repetitive tasks common to most systems. Based on the proposed Generic Robotic Agent Meta-Model (GRAMM), two distinct models for two different applications are derived, demonstrating the versatility and adaptability of the meta-model. By adapting the Gaia methodology to the design of open systems, this work makes the designers' job faster and easier, decreasing the time needed to complete several tasks, while at the same time maintaining a high-level overview of the system.