The formal and systematic specification of market structures and trading services

The paper supplies methodological support for trading system development. It provides a formal framework for the systematic definition of market structures and the specification of trading services. The first describes the interaction among traders, the second identifies the trading system interface and switches to a description of the system behaviour. The framework shows how to apply trace specifications as a formal description technique for both, and explains how to prove market structure and trading service properties. The framework moreover introduces concepts for building market structure taxonomies which support the systematic search and development of alternative forms of markets. They are collections of trace specifications for market structures with specialization and extension relationships defined between them