|
Computer systems often involve the distributed processing of data. Atypical example of this are electronic payment systems. The amount ofmoney that a customer wants to pay by credit card needs to becommunicated from a terminal to the financial institute which actuallycarries out the money transfer. On the other hand, the terminal andthe finance institute act as independent processes. To synchronisetheir behaviour, terminal and finance institute communicate with eachother. In the language of computer science, they form a reactivesystem.The aim of this research proposal is to improve the technologyavailable to develop distributed systems. The proposal belongs to thearea of formal methods. Here, mathematics is used in a systematic wayto ensure that computer systems behave as expected. In our example ofmoney transfer by a credit card, for instance, we would expect that thesystem does not get stuck in its actions. In the language of computerscience, the system should be deadlock free. Another importantproperty would be that exactly the amount of money is transfered whichthe credit card holder typed in at the terminal. Such properties needto specified. For this purpose we will use a language with the nameCSP-CASL.Distributed systems usually consists of different components. Thus, itis desirable to first describe these components individually, and thento build the system description from the component descriptions. Thefirst objective of our proposal is to equip CSP-CASL with suchpossibilities.In order to cope with complex systems, it is convenient to give firsta rough overview of them. This overview can then be equipped with moreand more details. For example, in the overview of an electronicpayment system we could state which components it has and how they areconnected: there is a credit card terminal, which is connected with apoint of service, the terminal can be updated from a service centre,etc. Later we make it more precise, how the various connectionswork. The relation between these two views of the system, the abstractand the more concrete one, is called refinement. The second objectiveof our proposal is to develop mathematically precise notions ofrefinement that capture the human intuition.Having described a distributed system in a mathematical way, we canprove that it has certain properties. This can only be done with thehelp of a computer, as system descriptions of real world applicationsbecome quite large. The third objective of our proposal is to developcomputer support to analyse descriptions of distributed systems.Describing and analysing a system is of course not enough: in the end,we want to build a concrete system and make sure that it workscorrectly. Consequently, objective four of our proposal is toestablish the correctness of an implementation by systematicallytesting it against the properties prescribed by its specifications.The results of our research will be applied and evaluated in anindustrial case study. Here, we have chosen ep2, which is a newstandard for electronic payment systems. Currently, the first ep2terminals are being installed in the UK. In this context, we expectthat our research will improve the ep2 standard as well as the qualityassurance mechanisms for ep2 terminals.Besides this concrete impact on one specific product, the results ofour proposal will be of interest for the large research community informal methods, especially in process algebra, algebraic methods,theorem proving, and testing theory.
|