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.
Software verification is a very active research field. However, the area of games has been only partially investigated. In @cite_14 , a case study of verification of role-playing game (RPG) is discussed. The authors use the Algebraic Petri Nets Analyzer (ALPiNA) model checker to verify reachability properties of the model, represented by the Petri Nets. The results of the work are very promising, however the game model has not been formally defined, and the necessary steps for constructing it from the game specification were not explicitly discussed. Moreover, examples of more complex game properties have not been studied.
@cite_14
2109613468 2152988203 1503128752 1901568548
We propose a technique for verification of mobile systems. We translate finite control processes, a well-known subset of π-Calculus, into Petri nets, which are subsequently used formodel checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe processes, a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime. We also demonstrate the applicability of our method on a realistic model of an automated manufacturing system. With their intuitive graphical approach and expressive analysis techniques, Petri nets are suitable for a wide range of applications and teaching scenarios, and they have gained wide acceptance as a modeling technique in areas such as software design and control engineering. The core theoretical principles have been studied for many decades and there is now a comprehensive research literature that complements the extensive implementation experience. In this book the author presents a clear, thorough introduction to the essentials of Petri nets. He explains the core modeling techniques and analysis methods and he illustrates their usefulness with examples and case studies. Part I describes how to use Petri nets for modeling; all concepts are explained with the help of examples, starting with a generic, powerful model which is also intuitive and realistic. Part II covers the essential analysis methods that are specific to Petri nets, introducing techniques used to formulate key properties of system nets and algorithms for proving their validity. Part III presents case studies, each introducing new concepts, properties and analysis techniques required for very different modeling tasks. The author offers different paths among the chapters and sections: the elementary strand for readers who wish to study only elementary nets; the modeling strand for those who wish to study the modeling but not the analysis of systems; and finally the elementary models of the modeling strand for those interested in technically simple, but challenging examples and case studies. The author achieves an excellent balance between consistency, comprehensibility and correctness in a book of distinctive design. Among its characteristics, formal arguments are reduced to a minimum in the main text with many of the theoretical formalisms moved to an appendix, the explanations are supported throughout with fully integrated graphical illustrations, and each chapter ends with exercises and recommendations for further reading. The book is suitable for students of computer science and related subjects such as engineering, and for a broad range of researchers and practitioners. We consider verification of safety properties for concurrent real-timed systems modelled as timed Petri nets by performing symbolic forward reachability analysis. We introduce a formalism, called region generators, for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions and provide exact abstractions of sets of reachable states with respect to safety properties. We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples. We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer's protocol, Lynch and Shavit's mutual exclusion protocol and a producer-consumer protocol. We also used the tool to extract finite-state abstractions of these protocols. We describe a software model checking tool founded on game semantics, highlight the underpinning theoretical results and discuss several case studies. The tool is based on an interpretation algorithm defined compositionally on syntax and thus can also handle open programs. Moreover, the models it produces are equationally fully abstract. These features are essential in the modeling and verification of software components such as modules and turn out to lead to very compact models of programs.