The iframe on this page is empty and contains no contentSkip to content
Search
People

Department of Computing

Home » Research » Technical Reports » 1999

> # 1999 - Technical Reports

> Number | Report Title
> --- | ---
> 1999/1 | FEAST/1 FINAL REPORT M.M. Lehman, 8pp
> 1999/2 | MODELLING AND ANALYSIS OF WORKFLOW PROCESSES C. Karamanolis, G. Giannakopoulou, J. Magee, S. Wheater, 21pp
> 1999/3 | FAIRNESS AND PRIORITY IN PROGRESS PROPERTY ANALYSIS D. Giannakopoulou, J. Magee, J. Kramer, 29pp

> ## FEAST/1 FINAL REPORT

> M.M. Lehman, 8pp
> Report: 1999/1
> Download

> 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:

> - provide objective evidence of the presence and impact of feedback and systems dynamics in the software process
> - demonstrate that they can be exploited for managing and improving industrial processes
> - 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.

> ## MODELLING AND ANALYSIS OF WORKFLOW PROCESSES

> C. Karamanolis, G. Giannakopoulou, J. Magee, S. Wheater, 21pp
> Report: 1999/2
> Download

> 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.

> ## FAIRNESS AND PRIORITY IN PROGRESS PROPERTY ANALYSIS

> D. Giannakopoulou, J. Magee, J. Kramer, 29pp
> Report: 1999/3
> Download

> 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.

Main campus address:
Imperial College London, South Kensington Campus, London SW7 2AZ, tel: +44 (0)20 7589 5111
Campus maps and information | About this site

© Copyright 2008 Imperial College London