Formal Methods for Performance Evaluation

The main goal of this contribution is to advocate the increased use of formal methods (FM) in the field of performance evaluation (PE). Moreover, we try to reduce the mutual reservations between both areas, formal specification techniques and performance evaluation since both can profit from such an integration: FMs may find their way into a new and very attractive area of applications and some fundamental problems of PE may be overcome.The first part summarizes the evolution of PE, its methodology and the basic concepts of performance modeling and analysis, elaborated in specific contributions of this book.Classical modeling and analysis techniques have a high standard and have been quite successful. However, there are important problem classes still open, and there are some fundamental deficiencies: Task interdependencies and synchronization, interfacing in modeling hierarchies, methods and tools for automating the performance engineering process are typical examples.We therefore advocate the integration of FMs and PE and survey three advanced approaches, again, treated in detail in specific contributions: Stochastic Petri-Nets, Stochastic Activity Networks and Stochastic Process Algebras.We try to summarize our own experience with these techniques and conclude with a list of challenging topics and current research directions.