Speaker: Temesghen Kahsai, Dep. of Computer Science, Swansea University, UK

Time: Monday, March 2, 2PM
Location: Babbio 221, Stevens Institute of Technology
Host: David Naumann

Abstract:
The EP2 system is an electronic payment system and it stands for 'EFT/POS 2000' short for 'Electronic Fund Transfer / Point of Service 2000', is a joint project established by a number of (mainly Swiss) financial institutes in order to define the infrastructure for credit, debit and electronic purse terminals in Switzerland (www.eftpos2000.ch). The system consists of seven autonomous entities and they are centered around an EP2 Terminal. These entities communicate with the Terminal and, to a certain extent, with one another via XML-messages in a fixed format. Each component is a reactive system defined by a number of use cases. The EP2 Specification consists of 12 documents, each of which describe the different components or some aspect common to the components.

In this talk I will show the modeling of the EP2 specification in the formal specification language CSP-CASL [2]. CSP-CASL allows to formalize computational system in a combined algebraic / process algebraic notation. In [1] we have developed a proof method for various refinement notions of CSP-CASL. Using such proof method we verify the refinement of the different level of the EP2 specification. We also verify properties such as deadlock and livelock freedom using an interactive theorem prover.

References:
[1] T. Kahsai and M. Roggenbach. "Property preserving refinement for CSP-CASL". In A.Corradini and U. Montanari. Recent Trends in Algebraic Development Techniques. Springer-Verlang. To appear.

[2] M. Roggenbach. "CSP-CASL -- A new integration of process algebra and algebraic specification" Theoretical Computer Science, 354:42-71. 2006