A Lightweight Formal Method for the Prediction of Non-Functional System Properties
Jörg Barner · 2005
The goal of performance and reliability evaluation during the development of computerbased systems is to predict the compliance of the projected system with a set of non-functional requirements. As an example, consider the expected mean end-to-end delay of data packets in a communication network, which can be predicted on the basis of a stochastic model during the early conceptual design phase. A glance at the software engineering practice reveals that despite their high financial savings potential academic methods of performance evaluation are not applied on a large scale. Frequently quoted reasons for these findings are the cumbersome notation of some stochastic description techniques and the impractical presentation of the theoretical foundations. The successful application of performance evaluation methods thus remains reserved to a handful of well-educated experts. This phenomenon, termed insularity problem by some members of the academic performance evaluation community, can be regarded as a special case of the general problem of low formal method acceptance in industrial software development. The first formal methods were developed by several computer scientists about 40 years ago with the ambitious goal to create programs which are proven to be correct by construction. Because of the quite revolutionary approach to programming and the inability of their developers to show that formal methods are appropriate to solve larger real-world problems they did not become widely accepted and used by the software engineering industry. A promising attempt to bridge this “industry-academia gap” was initiated in the early-mid 1990s with the advent of “lightweight” formal methods for the verification of functional system requirements, some of which could be applied successfully in industrial software development projects. The initial point of view which is adopted in this dissertation is to regard performance evaluation as a branch of requirements verification techniques which are applied during the development of software-based systems. Because of the similarities in the structure and the objectives of the methods in both areas, we assume that the transfer of the lightweight formal method concept to the area of performance evaluation will have a positive effect on the solution of the insularity problem. In order to corroborate this assumption, a new lightweight formal method for the prediction of nonfunctional system requirements is developed within the scope of this thesis. The method consists of a formal description technique which is based on a well-defined syntax and semantics. It enables the user to specify the system structure and behaviour, the interaction of the system with its enviroment as well as the interesting nonfunctional system requirements as a stochastic model on a high abstraction level. The syntax of our description language combines the advantages of the pragmatic network-oriented modelling paradigm with the succinctness of a pure textual notation. The evaluation of the system properties is carried out in a user-friendly manner by the automatic analysis of the model in the evaluation environment prototype which was implemented in the context of this thesis. In order to demonstrate the applicability of the method we present some detailed case studies from the area of communication systems (WLAN, GSM). The keynote of this dissertation is to promote the transfer of technology from academia to industry by the integration of formal methods for performance and reliability evaluation in the early phases of the software development process.