Processes and Data

Lead Research Organisation: Swansea University
Department Name: College of Science

Abstract

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.

Publications

10 25 50
publication icon
G Holland (2009) Towards formal testing of jet engine Rolls-Royce BR725 in Proceeding of the 18th International Conference on Concurrency, Specification and Programming

publication icon
O'Reilly L (2009) CSP-CASL-Prover: A Generic Tool for Process and Data Refinement in Electronic Notes in Theoretical Computer Science

publication icon
Samuel D (2009) The Stable Revivals Model in CSP-Prover in Electronic Notes in Theoretical Computer Science

publication icon
Y Isobe (2010) CSP-Prover - A Proof Tool for the Verification of Scalable Concurrent Systems in Information and Media Technologies

 
Description An integrated setting for specifying, analysing, verifying, and testing from processes and data has been developed.
Exploitation Route The insights provide a sound foundations for questions arising e.g. in the context of the UML.
Sectors Digital/Communication/Information Technologies (including Software)

URL http://www.cs.swan.ac.uk/~csmarkus/ProcessesAndData/
 
Description The findings have influenced various developments in testing theory. Also, they have been of use in the are of security.
Sector Digital/Communication/Information Technologies (including Software)
 
Description AIST 
Organisation National Institute of Advanced Industrial Science and Technology
Country Japan 
Sector Public 
Start Year 2006
 
Description CARUS Information Technology AG 
Organisation C.A.R.U.S. Information Technology
Country Germany 
Sector Private 
Start Year 2006
 
Description Zuehlke Engineering AG 
Organisation Zuehlke Engineering AG
Country Switzerland 
Sector Private 
Start Year 2006