99/1

FEAST/1 FINAL REPORT
M.M. Lehman, 8pp

The FEAST/1 project was conceived in 1994 following formulation of the hypothesis that the software evolution process is a feedback system and must be treated as such to achieve major process improvement. The overall goals of the project were to:

1. provide objective evidence of the presence and impact of feedback and systems dynamics in the software process
2. demonstrate that they can be exploited for managing and improving industrial processes
3. produce justification for more substantial study of the feedback perspective and its implications

This paper gives the specific objectives that were identified for the project and describes work carried out, difficulties encountered and results achieved.

99/2

MODELLING AND ANALYSIS OF WORKFLOW PROCESSES
C. Karamanolis, G. Giannakopoulou, J. Magee, S. Wheater, 21pp

Practical experience indicates that the definition of real-world workflow applications is a complex and error-prone process. Existing workflow management systems provide the means, in the best case, for very primitive syntactic verification, which is not enough to guarantee the overall correctness and robustness of workflow applications. The paper introduces a method for formal verification of workflow schemas (definitions).

Workflow behaviour is modelled by means of an automata-based method, which facilitates exhaustive compositional reachability analysis. The workflow behaviour is checked against both safety and liveness properties, which can be either generic (applicable to all workflow schemas) or domain specific (applicable to a given schema). The analysis is performed by automated tools, which are accessible to designers who are not experts in formal methods.

99/3

FAIRNESS AND PRIORITY IN PROGRESS PROPERTY ANALYSIS
D. Giannakopoulou, J. Magee, and J. Kramer, 29pp

The liveness characteristics of a system are intimately related to the notion of fairness. However, the task of modelling explicitly fairness constraints is complicated in practice. To address this issue, we propose to check LTS (Labelled Transition System) models under a strong fairness assumption, which can be relaxed with the use of action priority. The combination of the two provides a novel and practical way of dealing with fairness. The approach is presented in the context of a class of liveness properties termed progress, for which it yields an efficient model-checking algorithm. Progress properties cover a wide range of interesting properties of systems, while presenting a clear intuitive meaning to users. An extensive comparison is provided of the approach proposed with classical LTL model-checking.