Trading systems have become sophisticated multi-agent infrastructures with complex development cycles. This is why the nancial industry constantly seeks for novel approaches to design and validate these systems. We propose the use of models to support such tasks. On the one hand, these models need to describe how objects (e.g., orders to buy/sell securities) are shared by the system and traders. On the other hand, being a dynamic multi-agent system, models of trading systems should have a clear structure, describing how participants interact between each other. In this paper, we address these requirements, integrating notions of various Petri net extensions. In particular, we discuss modeling capabilities/limitations of each extension, and we propose to integrate them into a single approach, allowing for comprehensive modeling of di erent trading system components.
Trading systems are software platforms used in nancial markets to support the
exchange of nancial instruments between market participants.The kind of such
instruments depends on the market type that a trading system works with. For
instance, in commodity markets, participants trade primary goods ranging from
cocoa to gold and oil. In foreign exchange markets, people trade currencies. We
consider trading systems in stock exchanges, where participants submit orders
to buy/sell securities (e.g., company shares) [
Today market environment has become more demanding. On the one hand,
there has been an increase of the number and the variety of participants, each of
which concurrently interacts with a platform according to some trading strategy.
On the other hand, in trading platforms, a plethora of market services and rules
a ecting, for example, order serving and trade execution policies, have to be
implemented. Thus, trading systems have turned into large and sophisticated
multi-agent infrastructures with complex development cycles, which are more
prone to various aws. Reducing or even eliminating the number of such aws
becomes a crucial task. However, within these systems, common alternatives to
analyze implementation aws such as active testing are sacri ced to minimize
latency and overhead, pushing software quality experts to search for clever and
less expensive/intrusive solutions [
In this work, we focus on developing a formalism to support the design and validation phases of trading systems, as illustrated in Fig. 1. To fully support these phases, models constructed with the devised formalism need to provide a holistic view, capturing di erent aspects of trading systems in a convenient level of abstraction. First, similar to business processes, trading system models need to describe the control- ow of system entities, i.e., activities that participants and a trading platform execute as well as their causal order. Second, as in dataaware models, the formalism should allow to describe how objects of the domain (e.g., orders, trades) can be consumed, produced and ultimately shared by the system and processes representing routines executed by the system participants. Finally, being a dynamic multi-agent system by nature, models of trading systems should have a consistent representation, describing how participants (also called agents) asynchronously interact with each other and with the trading platform. Moreover, the number of objects and participants in a model should be able to change dynamically without a ecting the model structure. A formalism meeting all such requirements can lay the basis for further development of comprehensive formal speci cations of trading systems, and it can be used for running multi-perspective validation methods such as simulation, veri cation and conformance checking.
In this paper, we delineate key modeling requirements for trading systems,
integrating notions of di erent Petri net extensions. Petri nets are a well-known
formalism for modeling and analyzing concurrent distributed systems [
As we show with several examples in this paper, none of these extensions can solely provide a holistic view that could fully cover the modeling requirements of trading systems. Thus, we discuss a possible extension that builds on top of di erent Petri net classes, and we demonstrate how it can be used to comprehensively model various trading system components. We point out that this solution is not a mere combination of existing Petri net extensions. For example, in contrast with db-nets, where queries are attached to places, we incorporate the concept of reference tokens with attached queries. The latter allows to model dynamic lists such as order books independently from the model structure.
The remainder of this paper is structured as follows. In Section 2, we provide an introduction to trading systems. In Section 3, we describe Petri net extensions and we discuss modeling capabilities and limitations using examples of trading system models. In Section 4, we informally present our integrated extension, and we demonstrate how to use it for modeling di erent components of trading systems. In Section 5, we present the related work. Finally, Section 6 provides some conclusions and future work. 2
When referring to trading systems, we consider a trading platform and a group of market participants. The former is a software infrastructure supporting the automatic exchange of securities between participants. Fig. 2 depicts a simplied view of the general architecture of trading systems. Communication between participants and a trading platform is typically handled through di erent network interfaces. For instance, a trading interface allows participants to log in the platform and to send/receive trading-related messages. A market information interface disseminates market information to users via a real-time protocol (RTP) channel. A downstream interface exchanges data with external systems: it sends reports to surveillance authorities, and it forwards executed trades to settlement and clearing systems performing the actual exchange of money and securities. market participants
trading platform agent 1
... agent N
trading Interface (FIX) session component market information interface (RTP) system repository downstream interface application component order books management matching engine (trade execution) ...
surveillance, settlement and clearing downstream systems
In this work, we focus on the services provided through the trading interface.
This interface is implemented according to a nance-oriented communication
standard. We consider as a reference the Financial Information Exchange (FIX)
protocol [
In the following, we describe how trading platforms internally manage orders and execute trades. Incoming orders of participants are received and processed sequentially by the corresponding application component, and then they get inserted into order books. Order books are lists where orders trading the same security are placed to be matched. Hence, in a trading platform, there can be an order book for each individual security that can be traded in that system. Each order book has a buy side and a sell side, where buy and sell orders are placed. Orders are placed in order books based on a precedence rule. In our work, we consider the price-time precedence rule, typically employed in most trading systems. This rule places rst buy orders (sell orders) whose prices are the highest (lowest ) in the buy (sell) side; if two orders in the same side have the same price, then the one that arrived earlier is getting placed rst. Table 1 displays an order book, whose orders are placed according to the price-time scheme.
Within a trading platform, there is also a matching engine that executes trades between orders. For a given order book, this engine takes as input the rst orders from the buy side and the sell side. Then, a trade can be executed i the price of the rst buy order is greater or equal than the price of the rst sell order (in other words, the best buyer is willing to pay at least as much as the best seller wants). This situation is exempli ed by the order book in Table 1, where the price of order O1 is greater than the price of order O6. When a trade is executed between a buy order o1 and a sell order o2, which respectively have q1 and q2 stocks, min(q1; q2) stocks are taken from each order (min returns the minimum of two numbers). The quantities of o1 and o2 are decreased according to what they traded, e.g., q10 = q1 min(q1; q2). For each of the two orders, if its remainder goes to zero, then the order is discarded from the order book (that is, the agent successfully sold/bought what she wanted through that order). Otherwise, the order remains in the order book (still as the rst one in its side) waiting to trade its remainder against the next best order of the other side. In Table 1, a trade of 1 stock will be executed with orders O1 and O6. Order O1 will be partially lled, keeping a remainder of 3 stocks, whereas order O6 will be lled and consequently discarded from the order book.
Petri nets. A Petri net consists of two kinds of nodes: places and transitions. Places (drawn as circles) represent conditions or resource bu ers, whereas transitions (drawn as boxes) denote system activities. Places store tokens (drawn as black dots), and they model resources, local threads, etc. Distribution of tokens across places represents a state of a Petri net, which is called a marking. A transition is enabled to re i each of its input places contains at least one token. Firing of an enabled transition consumes a token from each input place and produces a new token in each output place. Fig. 4(a) depicts a small example, where two net components denote agents, whereas a central component consumes orders and produces trades. Whilst we focus on modeling trading platforms and participants, in other cases it might be of interest to analyze atomic elements, i.e., evolution of orders across their lifetime within a platform. The latter can be modeled as a Petri net (see Fig. 4(b)) in which places account for order states and transitions denote activities over orders.
agent 1 buy orders a2 cancel a1
submit receive a3 c1
c2 c3 trade agent 2 sell orders submit b1
b2 cancel b3 receive order submitted t0 new t3 t1 t2 canceled
t1 partially filled t3 t2 filled (a) Interaction of two agents and a middleware receiving orders and producing trades. (b) Handling process of orders. Colored Petri nets. When constructing trading system models, it is needed to describe how domain objects such as orders are handled. For example, one may need to design how the application component of a platform inserts orders in an order book or how order attributes are modi ed. For this task we consider colored Petri nets (CPNs). In CPNs, tokens carry values of di erent data types. Fig. 5 presents a CPN modeling the application component of a trading platform. It models the reception of orders, how these orders are placed in order books according to an employed priority scheme, and how trades are produced. Orders are de ned as tuples o1 = (id,sec,q,p,s,st) where id is an order identi er, sec is the security that the order trades, q and p denote respectively the stock quantity and price per unit, s is the order side (buy or sell), and st is the order state. Place O is the entry point where orders are received.
ob buy_rank (id,sec,q,p,s,active) ob [#5(o1)=buy]
o1 t1 submit
buy order buy_rank ab o1 ab arriving 1`[] buy orders 1AB ORDER_QUEUE (id,sec,q,p,s,st) :: ab ab
new [sec = #2(hd ob)] t3 buy order
ORDER
O o1 [#5(o1)=sell] sseulblmoritder t2 sell_rank sb o1 sb
1`[]
ORDER_QUEUE 1AS abruryivoinrgders (id,sec,q,p,s,st) :: sb sb u1y`,[a(1ct,i1v,e4),,2(220,1,b,3u,y2,0a0c,tbivuey),,a(4ct,i1v,e2),,2(0311,1`,b,[] buy sides of 2,200,buy,active),(5,1,7,198,buy,activ 1 OB order books e)] ORDER_QUEUE if q > q2 then (id, sec, q - q2, p, s, st) (id, sec, q, p, s, st) :: ob :: ob else ob [p >= p2 andalso sec = sec2] (tid, id, id2, Int.min(q,q2)) trade t5
When there is an order in place O, either transition t1 (submit buy order) or t2 (submit sell order) can re, depending on the order side s. When t1 or t2 res, an order is inserted in place AB (resp., AS) for arriving buy (resp., sell) orders. Two list tokens represent an order book, i.e., the two tokens in places OB and OS model the order book in Table 1. More pairs of list tokens may be added to include more order books. Insertion of orders in an order book is modeled as follows. When transition t3 res, an order in place AB is transferred to a list token in place OB. The same principle holds on the sell side. The matching between rst buy and sell orders is done as follows. For two list tokens representing an order book, transition t5 takes the rst elements of each list { the rst buy order and the rst sell order. The ring of t5 is possible if the price p of the rst buy order is greater or equal than the price p2 of the rst sell order. Then, when t5 res, it is produced a token in place T denoting a trade. The remainder (if any) of each rst order is placed back as the rst element of its list.
CPNs provide a language for declaring expressions, formed by variables, constants and functions. In CPN Tools, this language is CPN ML { an implementation of the Standard Meta Language (SML). For example, to insert a buy order in an order book side, a function buy rank is used. The function performs a priority insertion of the order in the list. Thus, precedence rules such as the price-time scheme can be easily implemented. CPNs also provide boolean guards, extending the de nition of transition enabling. For example, transition t5 res only after the order price values have been checked against the guard assigned to t5.
λ1 t1 login agents start
Albeit CPNs meet various requirements to describe data aspects of trading systems, this extension falls short for modeling large multi-agent systems. As we have discussed before, one of the important requirements concerns the ability of having a clear representation of participants, describing how they interact with a trading platform. It is true that subnets denoting participants may be added in a CPN, and such subnets may be connected with the trading platform model using channels (e.g., place O in Fig. 5). However, the latter leads to the increasing complexity of net models that, in most cases, may be unreadable and impractical for analysis, especially in the presence of a large number of participants. Hence, we proceed to present another Petri net extension, where participants can be modeled as dynamic objects with explicitly speci ed behavior.
x x x x Nested Petri nets. Nested Petri nets (NP-nets) represent an extension of classical Petri nets where tokens can be Petri nets themselves. These tokens, called net tokens, account for agents whose behavior is described using Petri nets. Net tokens reside in a Petri net called the system net, denoting the environment in which agents interact. Thus, NP-nets allow to model multi-agent systems. Fig. 6 depicts a NP-net modeling a fragment of a platform session component. The system net models the platform side, whereas net tokens represent market participants. Places in the system net model connection states between agents and a trading platform. It provides a clear visualization, displaying which agents are at a given connection state, and how they move to other states in synchronization with the system. The way net tokens progress through this component depends on their inner states. For instance, transition t1 (activity login) res, if a transition u2 is enabled in an agent work ow (as these transitions are linked by a synchronization label 1). When u2 and t1 are enabled, both transitions re simultaneously, updating the session component and the agent involved: the net token is transferred to the place online agents, whereas her inner state is updated to online. This synchronization mechanism provides a way to model the communication ow at the session layer, depicted in Fig. 3. In general, NPnets have di erent ring steps: (i) an autonomous step, which is the ring of a transition in a net token, (ii) a transfer step, in which net tokens are consumed/produced in the system net without a ecting their inner states, (iii) a vertical synchronization step, which is the simultaneous ring of a transition in the system net and transitions in net tokens, as it was shown for t1 and u2, and (iv) a horizontal synchronization step, which is the simultaneous ring of two transitions in two net tokens residing in the same place of a system net. The main limitation of NP-nets lies in their inability to describe how net tokens and a system net share data. As explained before, when modeling trading systems, it is required to model how participants can send orders and receive trades from the trading platform. In this sense, we proceed with a Petri net extension where non-adjacent net components send/receive data through a shared database. new buy order • PARAMS = (o_id, a_id, sec_id, q, p) new buy order • DEL = { order(o_id, a_id, sec_id, q, p, 'buy', 'submitted')} new buy order • ADD = { order(o_id, a_id, sec_id, q, p, 'buy', 'active') } arriving buy orders for order book 'sec1'
(o_id, a_id, sec_id, q, p, s, st) order(o_id, a_id, 'sec1', q, p, 'buy', 'submitted') new buy order
t 3 order('O4','A4', 'sec1', 2, 20.1 $, 'buy', 'submitted') order('O1','A1', 'sec1', 4, 22.0 $, 'buy', 'submitted')
... DB-nets. This extension combines CPNs and relational databases into a single formalism. A db-net is structured in three layers: (i) a persistence layer consisting of a relational database. A database stores a nite set of facts (hereafter referred to as records), such that the structures of records are de ned by relation schemas ; (ii) a data logic layer which consists of a set of queries and actions used to read/update records in the database, and nally (iii) a control layer, consisting of a Petri net incorporating several features of CPNs. Fig. 7 describes buy order insertions in an order book, where a security sec1 is traded, using db-nets. The database stores, among other records, two orders. For instance, the record order('01','A1','sec1', 4, 22.0$, 'buy','submitted') models an order sent by the participant A1, to buy 4 stocks of sec1 at 22.0$ per stock. To access records in the database, db-nets employ special places called view places that work akin to views in relational databases. More speci cally, every view place is having a query assigned to it that populates the place's content with tokens extracted from the query answer. Let us come back to the dbnet in Fig. 7. The query order (o id,a id,'sec1',q,p,'buy','submitted') is equivalent to the SQL query SELECT o id, a id, sec id, q, p, s, st FROM order WHERE sec id='sec1' AND s='buy' AND st ='submitted', returning all orders planning to buy 'sec1' and whose state is 'submitted'. In Fig. 7, this query returns two records highlighted in the database, resulting in the view place being marked with two tokens that represent such records in the net. Every view place can be connected to transitions only via read arcs. This implicitly results in creating tokens that are \copies" of extracted records.
In db-nets, transitions are equipped with actions that allow to update the database. For example, upon ring, transition t3 invokes an action new buy order assigned to it. Assume that t3 has red and read the token ('O1','A1', 'sec1',4,22.0$,'buy','submitted') from the view place. The action assigned to t3 updates the database by rst deleting a record corresponding to order O1, and then adding to the database the same order, but now with its state value changed to submitted. In this way, manipulation of orders within the order books can be simulated.
In trading systems, the number of securities that are traded may change dynamically. Thus, there can be a variable amount of order books in the system. To deal with this variability, order books need to be independent from the model structure, and to be conceived as dynamic objects, like participants. Fig. 7 shows why db-nets cannot satisfy such requirement. The query to a collection of orders, representing an order book section, is attached to view places. Under this static modeling strategy, the size of the model structure increases according to the number of order books. This issue does not allow to conceptualize a clever management of order books, being created or closed upon demand. We aim to model order books as a combination of dynamic list tokens (e.g., as in the CPN of Fig. 5). In such model, participants should be able to manipulate remotely elements of such lists. This approach can be implemented if queries are attached to tokens (and not to places). Thus, the number of order books can be variable in the model. Such approach is explained in the following section, where we integrate notions of the introduced Petri net extensions into a single solution, addressing all the aforementioned requirements for modeling trading systems. 4
In this section, we propose the integration of the considered Petri net extensions into a single formalism for modeling trading systems. We conceive a Petri net combining the characteristics of CPNs and NP-nets. In addition, following the approach of db-nets, we include in our extension a relational database and queries to consume database records. However, in contrast with db-nets, these queries are going to be directly assigned to reference tokens. Such tokens are carrying direct links to records extracted from the underlying database using such queries. Moreover, any manipulation done with these tokens are mirrored on the records they are pointing at. For example, a token that is consumed by a transition will have its data deleted from the database. ('O2','A2', 'sec1', 3, 20.0 $, 'buy', 'submitted') p1 o
t 3 Using our proposal, a trading system is modeled as a multi-agent system, consisting of a system net and net tokens. The system net models the session and application components of a trading platform as two disjoint components. Net tokens, denoting participants, reside within the session component (as in Fig. 6). Fig. 9 shows a top view of the trading system model. The application component models order insertion in order books and trade executions. Agents interact with the application component via a database. Database records are orders, trades, or agent data, based on a schema derived from the entity-relationship diagram of Fig. 10. For example, trade('T1', 1, 20.0$, 'A1','A6','O1','O6') models a trade between a buyer A1 and a seller A6. Participants and the application component consume/produce records from/to the database using reference tokens. Records in the database are non ordered, so the application component manages orders using reference tokens, whose queries are equipped with sort clauses. Table 2 shows how four reference tokens can model sections of an order book.
System Net .....
Fig. 10: Entity-relationship diagram of the database model. 4.2
Modeling Market Participants Participants can be modeled as net tokens, nested within the session component of the system net. Each net token has an inner Petri net work ow (see Fig. 11) composed by di erent aspects of an agent trading process (control- ow, references to data, and local resources). We describe these aspects, as well as the activities of order submission and trade reception.
Agent control- ow. The control- ow is the agent process backbone. It consists of a set of activities that an agent executes, and it establishes a causal ordering, e.g., activity submit buy order executes i the login activity was executed before. As we resort to the same synchronization steps of nested Petri nets, some transitions in the work ow are linked with transitions in the session component using synchronization labels. In this way, we model the connection management between a participant and the session component of a trading platform. References to shared data. An agent may have references to shared data, for example, to orders that the agent submitted or to upcoming trades. In Fig. 11, reference tokens are created upon the ring of transitions u1 and u2. When u1 res, it creates a reference to a record agent('A1'), as speci ed by the inscription agent( ) on the arc (u1; r1) ( is a unique f resh agent identi er). Other agents subsequently ring u1 would insert agent ('A2'), agent('A3'), etc. After u2 res, references to agent's orders and future trades are created. The queries of these references use the identi er A1.
stock (10,'sec1') portfolio (40,'sec2') λ1
u2 ready login
d 1 start agent(ν) u1 init
a_id r1 reference to agent identifier agent('A1') r 2 ...
u6 online logout end trade(o1, o2, o3, a_id, o5, o6, o7, o8) order(o1, a_id, o3, o4, o5, o6, o7)
r3 reference to reference to agent’s orders agent’s buy trades
trade(o1, o2, o3, 'A1', o5, o6, o7, o8) order(o1, 'A1', o3, o4, o5, o6, o7) d
Agent local resources. Agent local resources (non visible by other agents or the system net) are modeled as places storing tokens with data values. In Fig. 11, places d1 and d2 represent the agent's stock portfolio and capital. The stock portfolio is a set of pairs denoting stock quantities of securities that an agent trades, whereas the capital is the available balance to buy more stocks. Creation and submission of orders. An agent can use her local resources, for instance, to create and submit buy orders. In Fig. 12, the ring of transition u3 produces an order (yet a local data token) in place order created. When transition u4 res, the order is consumed, and it is produced as a record in the database. The latter is accomplished using the reference token to agent's orders in the shared database.
d 1
stock
portfolio
Reception of trade noti cations. Fig. 13 depicts the reception of a trade
noti cation in which an agent was involved as a buyer. The buyer updates her
trade portfolio based on the purchased quantity of stocks informed in the record.
d 1
stock
portfolio
receive
buy trade
a_btrades
(10,'sec1')
(40,'sec2')
(qt,sec_id)
(qt + hd(a_btrades)[
Fig. 13: Agent model fragment describing the reception of trades for a buyer.
Modeling the Application Component of a Trading System The application component processes orders submitted by agents. As explained before, all orders in the database trading the same security are organized using four di erent reference tokens, representing thereby the di erent sections of an order book. As depicted in Fig. 9, these reference tokens are located in di erent places of the application component: two tokens for arriving buy/sell orders, and other two tokens for the buy/sell side of the order book. Using this design, we explain the insertion of an order into an order book side and the execution of trades.
Order insertion in an order book side. The insertion of an arriving order into an order book is managed by changing the state attribute of an order from submitted to active. In this case, the order will be referenced by the reference token which acts as the buy or sell side of an order book. This procedure is exempli ed in Fig. 14. When transition t3 res, it accesses the list of orders referenced by the token at place references to arriving buy orders, removes the rst record of this list (that is O1, which is the next arriving buy order to be served), resulting in the simultaneous deletion of the same record in the database, and then inserts this record in the list carried by the reference token at place references to buy sides of order books. Note that the newly generated token is going to reference a new record as its state is set to active.
order(o1, o2,'sec1', o4, o5, o6, 'buy', 'submitted') sort(o5,o1) desc order('O2','A2', 'sec1', 3, 20.0 $, 'buy', 'submitted') order('O3','A3', 'sec1', 2, 20.0 $, 'buy', 'submitted') order('O1','A1', 'sec1', 4, 22.0 $, 'buy', 'active') order(o1, o2,'sec1', o4, o5, o6, 'buy', 'active') sort(o5, o1) desc references to arriving buy orders ab
ab \ hd(ab)
t3
new
buy order
[hd(ab)[
Fig. 14: Model fragment regarding insertion of orders into an order book.
Trade execution. As explained before, if the rst two orders of each side of
an order book can be matched, then they can produce a trade. We recall that a
trade execution is possible i the price of the rst buy order is greater or equal
than the price of the rst sell order. Fig. 15 presents a fragment of the application
component modeling this situation. The guard in transition t4 (activity trade)
models the inequality condition between the fth attributes (the price) of the
rst records in each side. Then, when transition t4 res, it consumes these rst
orders, it produces a trade record with the stock quantity traded, and nally it
places back these rst orders to their sides in case they have any stock remainder.
ob
os
references to sell sides
of order books
The increasing amount and heterogeneity of participants and market rules has
driven the nancial industry to look for novel approaches to design and
validate trading systems. In this regard, passive testing techniques have drawn the
attention of practitioners [
However, to detect deviations that occur due to agent or data corruption,
integrated formalisms modeling agent and data aspects become essential. As it
has been proposed in [
To model trading systems, we are interested in using Petri-net based techniques that can describe persistent data storage with all the complexity of an underlying data model to capture data manipulation, as well as to represent autonomous agents together with a logic that allows them to interact with each other and the environment. As we have already demonstrated before, existing Petri net formalisms do not fully capture all the requirements needed to faithfully model trading systems. We brie y discuss formalisms used in this work and other Petri net classes related to them.
In order to model autonomous agents that interact with each other and the
environment, we considered nested Petri nets [
In Section 3, we showed that colored Petri nets could be used for describing
processes that manipulate complex data objects. In CPNs, colors abstractly
account for data types, and the control threads (i.e., tokens), traversing the
net, carry data conforming to colors. However, when it comes to the analysis of
CPN models, one needs to severely restrict the contribution of data by requiring
colors to have a nite domain [
There are still other data-aware Petri net classes in which tokens are
associated to more complex data structures such as nested relations [
Given that the data representation and manipulation are crucial for
modeling trading systems, in this paper we opted for db-nets [
In this work, we primarily focused on formal modeling of trading systems in the context of Petri net theory so as to provide a basis for testing their correctness using trading system logs. To this end, we identi ed and presented a number of crucial design requirements that would allow to capture a holistic view over the systems under consideration. Then, it has been shown how such requirements could be addressed using currently existing formalisms of Petri nets. We argued that each of such formalisms can be suitable for representing only a certain type of the trading system abstraction (and supported our observations with concrete examples), and that currently there is no approach that could fully address all the requirements. Therefore, we informally proposed a new framework that combines relevant features of the discussed Petri net formalisms, and we demonstrated using detailed examples how it can be employed for modeling di erent components of trading systems.
A next step is to thoroughly formalize the proposed approach by
combining already existing theories of CPNs, db-nets and NP-nets, and to develop a
prototype supporting modeling and simulation. We also plan to study how to
analyze the models of the devised formalism. Indeed, given such a rich setting,
performing formal analysis can be a complex task. In this case, one can proceed
independently following two directions. First, it is possible to focus only on the
simulation task supported by the prototypical implementation of the proposed
approach. This can be further applied to perform model-based passive testing.
More speci cally, one would need to develop a conformance checking technique
that accounts both for data and agents interacting with the system net, and that
uses execution traces of the trading system software. Notably, the latter can be
extracted from trading system logs following the approach presented in [