Using Functional Specification to Detect Failed Error Propagation in Stateful Services: An Industrial Case-Study

In stateful transactional services, latent internal errors often fail to manifest at the output level, eluding traditional black-box testing methods. This phenomenon, known as Failed Error Propagation (FEP), represents a critical blind spot in software quality assurance, particularly in business-critical domains such as financial trading systems. In this paper, we present a novel specification-based testing approach for FEP detection using high-level functional specifications written in Haskell. Our method integrates definition-use (du) path coverage analysis into the test generation process and leverages search-based techniques to synthesize test suites that increase the probability of exposing FEP. We evaluate our approach on a production-grade stock exchange order matching engine and uncover two previously undetected FEP-related bugs, demonstrating the practical effectiveness of our technique. Additionally, our empirical results show a significant improvement in fault detection sensitivity when combining expression coverage with du-path analysis. These findings highlight the value of specification-based, data-flow- aware testing for uncovering subtle yet impactful faults in complex systems. 1 Received: Added at production Revised: Added at production Accepted: Added at production DOI: xxx/xxxx A R T I C L E T Y P E Using Functional Specification to Detect Failed Error Propagation in Stateful Services: An Industrial Case-Study Arvin Zakeriyan Ramtin Khosravi School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran Correspondence Ramtin Khosravi, School of Electrical and Computer Engineering, University College of Engineering, University of Tehran, N. Kargar Ave., Tehran, Iran. Email: [email protected]

In stateful transactional services, latent internal errors often fail to manifest at the output level, eluding tradi- tional black-box testing methods. This phenomenon, known as Failed Error Propagation(FEP), represents a critical blind spot in software quality assurance, particularly in business-critical domains such as financial trading systems. In this paper, we present a novel specification-based testing approach for FEP detection using high-level functional specifications written in Haskell. Our method integrates definition-use (du) path coverage analysis into the test generation process and leverages search-based techniques to synthesize test suites that increase the probability of exposing FEP. We evaluate our approach on a production-grade stock exchange order matching engine and uncover two previously undetected FEP-related bugs, demonstrating the practical effectiveness of our technique. Additionally, our empirical results show a significant improvement in fault detection sensitivity when combining expression coverage with du-path analysis. These findings highlight the value of specification- based, data-flow-aware testing for uncovering subtle yet impactful faults in complex systems. K E Y W O R D S Automatic Test Case Generation, Specification-Based Testing, Functional Languages, Search-Based Software Testing, Failed Error propagation 1 INTRODUCTION1 In many industries, software systems have evolved into the backbone of business-critical operations. This is particularly evident2 in domains such as finance, telecommunications, and healthcare, where correctness, reliability, and timeliness are especially3 important.Failures in these domains are rarely negligible: unnoticed data corruption or subtle logic errors can result in financial4 loss, reputational damage, or regulatory non-compliance. Given these stakes, testing plays a critical role in ensuring the5 quality of such systems. One such example is stock exchange platforms, where software systems must not only maintain strict6 correctness guarantees but also meet high levels of non-functional requirements. These properties necessitate the integration of7 non-domain elements into the system, ranging from frameworks and libraries at the architectural level to micro-optimizations at8 the implementation level. Although these non-domain elements are added to improve quality-related features, their presence and9 interaction can introduce new execution paths that may produce incorrect outputs.10 In testing industrial-grade transactional services, black-box model-based testing can be highly effective. Rather than relying on11 access to implementation internals—which are often complex (due to architectural patterns like inversion of control to increase12 testability and dynamic configuration) or partially unavailable (due to third-party libraries and frameworks)—model-based13 approaches focus on high-level specifications of the system’s intended behavior. These specifications serve both as reference14 models from which test cases can be automatically generated and as oracles to determine the expected outputs.15 In our previous work 1, we developed such a framework using Haskell as the specification language. By leveraging the16 expressive power of functional programming and strong typing, we were able to model complex stateful behavior in a concise17 and analyzable manner. Our test case generation approach treated the system under test (SUT) as a function of the form: Request18 Journal 2023;00:1–21 wileyonlinelibrary.com/journal/ © 2023 Copyright Holder Name 1 2 ZAKERIY ANET AL . × State → Response × State, where the state encapsulates business-critical data such as order books, shareholder stock positions,19 and broker credits. Using search-based techniques and structural coverage metrics on the specification, we generated test suites20 that explored diverse execution paths through the SUT and achieved high structural coverage scores.21 However, despite achieving high coverage, we encountered a significant limitation: some faults in the SUT did not manifest in22 its observable behavior. That is, although an fault occurred during computation and corrupted the internal state, the system still23 produced outputs that were syntactically and semantically correct from the external observer’s perspective. Such faults could24 be observed if the internal state were logged after each request execution; however, this is uncommon due to performance and25 security concerns. Consequently, these types of faults remain hidden. This phenomenon, known asFailed Error Propagation26 (FEP), represents a critical blind spot in conventional black-box testing techniques.27 FEP is particularly problematic in transactional stateful services, where errors in one operation can silently propagate into the28 internal state and later affect the outcomes of subsequent operations. For example, a miscalculation when updating a broker’s29 credit might not lead to immediate failure if the resulting value remains within acceptable bounds. However, over time, such30 errors can accumulate and cause serious violations of business rules. In traditional single-request test cases, these issues may31 never surface, as the incorrect state remains latent and unused.32 In 2, the authors show that the frequency of FEP is substantially higher in system-level testing than in unit-level testing. This is33 because detecting FEP using black-box testing is challenging for several reasons. First, many internal state variables are only34 indirectly reflected in system outputs, and only under specific input conditions. Second, the manifestation of an error often35 depends on complex sequences of state transitions, which are unlikely to be triggered by tests based on isolated inputs.36 To overcome these challenges, we extend our previous work 1 and propose a novel approach that integrates data-flow37 coverage—particularly definition-use (du) path coverage—of the specification into the test generation process. Our key insight is38 that FEP can be more effectively detected by focusing on how internal state variables are modified and subsequently used across39 execution paths. By tracing du-paths over state variables within the specification, we can generate tests that explicitly exercise40 these paths, increasing the likelihood of surfacing hidden errors.41 Moreover, we use a test case model that supports sequences of operations, allowing a single test case to contain multiple42 requests. This design decision is crucial: in many cases, the use of a corrupted state variable occurs in a later operation, not43 the one that introduced the fault. By allowing stateful chains of requests in a single test case, we enable the accumulation and44 exposure of errors that would otherwise go undetected.45 Our contributions in this paper can be summarized as follows:46 • We identify the problem of FEP in stateful transactional services and highlight its implications for black-box testing.47 • We introduce a semi-automated data-flow analysis mechanism tailored for high-level functional specifications written in48 Haskell. This mechanism extracts du-paths for internal state variables and supports execution-time instrumentation for49 coverage analysis.50 • We propose a test generation framework that incorporates du-path coverage as a fitness objective, and we explore both total51 and unique path coverage metrics.52 • We evaluate our approach on a production-grade stock market order matching engine. Despite the system’s maturity and53 extensive test coverage, our method detected previously unknown faults that had evaded traditional testing.54 The remainder of this paper is organized as follows. In Section 2, we present the background and provide an overview of the55 system under test. Section 3 details our FEP-aware test generation strategy. Section 4 details the test case generation approach.56 Section 5 reports the results of our empirical study. In Section 6, we discuss related work, and Section 7 concludes the paper.57 2 BACKGROUND58 2.1 Introduction to the Matching Engine59 This work focuses on testing an industrial-grade stock market order matching engine,‡ which forms the core of the electronic60 trading platform used by the Tehran Stock Exchange. The matching engine is responsible for processing and matching various61 ‡ https://en.wikipedia.org/wiki/Order_matching_system USING FUNCTIONAL SPECIFICATION TO DETECT FAILED ERROR PROPAGATION IN STATEFUL SERVICES 3 Order Book Before Matching Buy Sell ID Price Qty ID Price Qty 1 50 500 4 55 500 2 40 1000 5 60 300 3 40 800 6 70 1000 Order Book After Matching Buy Sell ID Price Qty ID Price Qty 7 60 400 6 70 1000 1 50 500 2 40 1000 3 40 800 Input Buy Order ID Price Qty Broker ID Shareholder ID 7 60 1200 112 921 Output T rades BID SID Price Qty 7 4 55 500 7 5 60 300 F I G U R E 1 Example of matching a limit order. Buy order ID 7 is matched with two sell orders. The unmatched remainder is stored in the buy queue. types of trading orders (e.g., Limit §, Iceberg¶, Cross#) and supports multiple qualifiers such as Fill and Kill (also known as62 Immediate or Cancel∥) and Minimum Quantity∗∗.63 In addition to matching, the system performs critical pre- and post-matching checks, including validation of broker credit64 limits and shareholder position thresholds.65 Like other high-performance matching engines, the system is subject to strict non-functional requirements—particularly ultra-66 low latency, where each request must be processed within sub-millisecond timeframes. Meeting these requirements necessitates a67 sophisticated software architecture, combining advanced design decisions, performance optimizations, and the use of specialized68 frameworks and libraries. For instance, the system leverages the Disruptor framework†† for high-throughput event processing,69 Project Lombok‡‡ for reducing boilerplate code, and the Spring framework for dependency injection and configurability.70 To avoid the latency introduced by interactions with external databases, the system uses custom in-memory data structures to71 manage broker credits, shareholder positions, and order books. Alongside architectural optimizations, the codebase incorporates72 low-level performance tuning to ensure responsiveness and scalability under high load.73 2.1.1 Running Example74 To assist readers unfamiliar with trading systems, we introduce a simplified matching algorithm that serves as a running example75 throughout this paper. One of the most common order types is the limit order, defined as: “An order to buy or sell a stock at a76 specific price or better”.§§ A limit buy order can only be matched with sell orders at the same or lower price, while a limit sell77 order can only be matched with buy orders at the same or higher price.78 Each limit order contains key attributes: an order ID, stock symbol, limit price, quantity, and the identifiers of the shareholder79 and broker. If no match is immediately available, the order is stored in anorder book—a data structure containing two priority80 queues: one for buy orders and one for sell orders. Buy orders are prioritized by highest price first; sell orders by lowest price81 first. For orders with equal prices, earlier entries take priority.82 Figure 1 presents a concrete example. A new buy order (ID 7) with a limit price of 60 and quantity of 1200 arrives. The order’s83 broker ID is 112 and it belongs to shareholder 921. The engine attempts to match it with existing sell orders. The first two sell84 orders (ID 4 at 55 and ID 5 at 60) satisfy the price constraint and are partially matched. The third sell order (ID 6 at 70) exceeds85 the limit price and is not matched. The unmatched quantity (400 units) from the new order is then added to the buy queue.86 The matching engine maintains an internal state comprising broker credits, shareholder stock positions, order books, and87 metadata for each stock symbol. When a new order is submitted, several pre-trade validations are executed. For instance, the88 system verifies whether the submitting broker has sufficient credit to cover the order value (price× quantity). In the example,89 upon placing the new order, the system checks that broker with ID 112 has more than 72,000 in credit.90 § https://www.investopedia.com/terms/l/limitorder.asp ¶ https://www.investopedia.com/terms/i/icebergorder.asp # https://www.investopedia.com/terms/c/cross.asp ∥ https://www.investopedia.com/terms/i/immediateorcancel.asp ∗∗ https://www.netsuite.com/portal/resource/articles/inventory-management/minimum-order-quantity-moq.shtml †† https://lmax-exchange.github.io/disruptor/disruptor.html ‡‡ https://projectlombok.org §§ https://www.sec.gov/fast-answers/answerslimithtm.html 4 ZAKERIY ANET AL . Post-trade, the internal state is updated accordingly: broker credits are debited or credited, and shareholder positions are91 adjusted to reflect the new ownership after each executed trade. In our example, the ownership position of shareholder 92192 increases by 800—the total matched quantity. Additionally, the credits of the brokers who placed orders 4 and 5 are increased93 based on the value of the trades they participated in. The credit of broker 112 is decreased by 400 × 60, reflecting the value of94 the queued order.95 2.2 Overview of Our Testing Approach96 In prior work1, we introduced an automatic test case generation framework based on a functional specification of the SUT written97 in Haskell. We modeled the domain logic for stateful transactional services in form of handlers and decorators. The handler has98 the responsibility of handling the each request. It has the general form of Request × State → Response × State. In this model,99 the handler function operates on the new request and based on the internal state and the new request generates the observable100 response and updates the internal state. As each request may require some pre-or post-check and calculation to happen during101 it’s process, we use a recursive pattern similar to the Decorator design pattern. A decorator is a higher order function of type102 Decorator = Handler → Handler which encapsulate the inner handler which in turn may be composed of multiple decorators103 applied to a request handler. A detailed sample of the handler and decorator functions is presented in appendix A.104 To facilitate this specification, we recommend modeling the internal state using domain-appropriate data structures. These105 components are then unified into a composite data structure representing the system state. The Haskell specification not only106 captures the functional behavior of each operation but also enables automatic derivation of test oracles and guides the test107 generation process using search-based algorithms.108 Our framework uses this specification to synthesize black-box test cases that explore meaningful execution paths and validate109 correctness through functional assertions. However, as discussed later in the paper, some faults—especially those related to silent110 state corruption—can evade detection through conventional output-based validation, motivating the work presented in this paper.111 3 TESTING FOR FAILED ERROR PROPAGATION112 The challenge of FEP has been a persistent concern in software testing, particularly in the context of transactional stateful services113 where undetected errors can lead to significant operational failures. There has been much research focusing on measuring the114 likelihood of FEP occurring in a system or on evaluating the strength of tests to capture FEP. In this work, we choose a different115 approach: we incorporate the possibility of FEP directly into our test case generation mechanism and aim to generate tests that116 better detect FEP in the system.117 3.1 The Challenge of Failed Error Propagation118 FEP poses a significant and persistent challenge in software testing, especially for transactional stateful services. In such systems,119 latent internal faults can remain undetected, failing to manifest as observable errors in the system’s outputs. This lack of error120 propagation can lead to severe operational failures, as the underlying corruption can accumulate and eventually trigger critical121 issues. The consequences of FEP are especially pronounced in business-critical domains such as financial platforms, where even122 seemingly minor data inconsistencies can have substantial and harmful repercussions. For instance, FEP in a banking system123 might result in an unnoticed incorrect account balance, while in a stock market matching engine, it could lead to an incorrect124 calculation of a shareholder’s position.125 To illustrate the concept of FEP, consider the Haskell code snippet presented in Listing 1. This simplified example demonstrates126 how a subtle internal fault can remain hidden from typical black-box testing. In this example, we assume there is only one broker127 whose credit is stored in the credit field of the state. The function match simulates processing an order. After matching128 the order against the order book, it first checks if the buyer has sufficient credit usinghasEnoughCredit, then updates the129 credit variable in the state using decreaseCredit. However, the decreaseCredit function contains a subtle bug: it130 intentionally deducts an extra 10 units from the credit. This is not a crash or an immediately obvious error but a silent data131 corruption. The main function then executes a single test case: applying a buy order of price 5 and quantity 10 against an132 order book which contains enough sell orders such that the new order is matched completely, starting with an initial credit of133 USING FUNCTIONAL SPECIFICATION TO DETECT FAILED ERROR PROPAGATION IN STATEFUL SERVICES 5 100. Despite the presence of the bug in decreaseCredit, this specific test case fails to reveal the fault. The test execution134 first checks if there is enough credit considering the new order which there is. After this checking the credit is updated to an135 incorrect value.But since this value is not used from this point on and the credit values are note present in the final outputs of136 the system, this fault can not be discovered. Thus, the test reports a set of trades, masking the underlying data corruption. This137 highlights a key limitation of black-box testing: it often lacks visibility into the system’s internal state, making the detection of138 non-propagating errors difficult.139 Listing 1 Sample Failed Error Propagation Program 1 type Credit = Int140 2141 3 data State = State142 4 { credit :: Credit143 5 -- other parts of the state such as order book144 6 }145 7 deriving (Show, Eq)146 8147 9 initialState :: State148 10 initialState = State { credit = 100 } -- the rest of definition of initial state149 11150 12 data Order = Order151 13 { price :: Int,152 14 qty :: Int153 15 }154 16 deriving (Show, Eq)155 17156 18 data Trade = Trade157 19 { price :: Int,158 20 qty :: Int159 21 }160 22 deriving (Show, Eq)161 23162 24 -- Function to calculate the worth of a trade163 25 worth :: Trade -> Int164 26 worth trade = price trade * qty trade165 27166 28 hasEnoughCredit :: State -> Int -> Bool167 29 hasEnoughCredit state worth = credit state >= worth168 30169 31 decreaseCredit :: State -> Int -> State170 32 decreaseCredit state worth = state { credit = credit state - worth - 10 }171 33172 34 match :: Order -> State -> (Maybe [Trade], State)173 35 match order state =174 36 let trades = [] -- match order against the orderbook and create the list of possible trades175 37 tradesWorth = sum $ map worth trades176 38 in if hasEnoughCredit state tradesWorth177 39 then (Just trades, decreaseCredit state tradesWorth)178 40 else (Nothing, state)179 41 -- the rest of matching validation and post checkings180 42181 43 checkMatchResult :: (Maybe [Trade], State) -> String182 44 checkMatchResult (Nothing, _) = "No trades occurred"183 45 checkMatchResult (Just [], _) = "No trades occurred (empty list)"184 46 checkMatchResult (Just trades, _) = "Trades occurred: " ++ show trades185 47186 48 main :: IO ()187 49 main = do188 50 let buyOrder = Order 5 10189 51 let (trades, updatedState) = match buyOrder initialState190 52 putStrLn (checkMatchResult (trades, updatedState))191 Existing research on FEP has largely concentrated on assessing and predicting the likelihood of FEP occurring within a192 system, rather than on generating tests designed to capture it. One significant branch of this work employs techniques rooted in193 information theory and static code analysis. Here, researchers develop metrics and models to estimate the probability of FEP194 6 ZAKERIY ANET AL . based on the system’s structure, complexity, and potential for information loss during error propagation. The goal is to identify195 system characteristics or code patterns that might inherently make it more susceptible to internal faults not manifesting externally.196 Another line of research frames FEP from the perspective of fault localization in the context of code coverage. In this view,197 FEP is considered an undesired state where a fault exists but is not revealed by the executed test cases, leading to low correlation198 between code coverage and fault detection. These studies often analyze how different coverage criteria (e.g., statement coverage,199 branch coverage) perform in revealing faults that lead to FEP. The focus is on understanding why certain faults remain hidden200 despite achieving seemingly adequate code coverage and on improving fault localization techniques to better pinpoint the source201 of such non-propagating errors.202 Our research aims to address the challenge of FEP from a novel perspective. We focus on black-box testing of stateful203 transactional services, where test cases are automatically generated from specifications implemented in a high-level programming204 language like Haskell. Our approach incorporates specific strategies into the test case generation process to enhance the205 probability of detecting FEP. Specifically, we leverage metaheuristic search algorithms for test case generation and integrate206 coverage criteria designed to improve FEP detection into the fitness functions guiding the search. By doing so, we aim to207 generate test suites with a significantly higher likelihood of uncovering subtle, non-propagating errors within the SUT.208 3.2 Leveraging Data Flow Coverage for Test Case Generation209 In the context of transactional stateful services, we can model services as functions that transform a system’s state based on210 an input request, producing a response and a potentially modified state: Request × State → Response × State.211 FEP in such systems occurs when an internal fault originating from the Request or the processing logic (represented by the212 left-hand side of the function signature) leads to an incorrect alteration of the State, yet this error does not manifest in the213 observable Response. To enhance the likelihood of detecting such FEP scenarios through testing, our strategy should prioritize214 the examination of how variables within the State are manipulated and utilized.215 Among the various test coverage criteria, data flow coverage seems particularly effective for capturing FEP. This effectiveness216 stems from the fact that FEP often arises from subtle discrepancies in the updating of state variables that do not immediately217 propagate to the observable outputs. Data flow coverage criteria, such as du-path coverage, specifically focus on tracing the flow218 of data through the system. A du-path connects the point where a variable is defined (assigned a value) to the points where that219 value is subsequently used. By ensuring coverage of these paths that originate from the beginning of program execution and220 extend to a termination or output point, we can effectively track how changes to state variables propagate (or fail to propagate) to221 the system’s observable behavior during test execution. In essence, by directing our test generation efforts towards covering the222 definition and subsequent uses of state variables, we increase the probability of detecting inconsistencies or errors in how these223 variables are updated and utilized, ultimately improving our chances of capturing FEP. For instance, by meticulously tracking the224 du-paths of the credit variable — from where it is modified during a transaction to where its value influences a later decision225 or output — we can detect if the erroneous –10 unit adjustment has occurred, even if the final transaction appears superficially226 successful. In contrast, simpler criteria like branch coverage might only ensure that all conditional branches in the code are227 executed, but they may not adequately cover the data dependencies and the flow of state variables that are crucial for detecting228 FEP.229 Furthermore, the utilization of functional specifications implemented in a high-level programming language plays a crucial230 role in generating effective FEP-detecting test cases. These specifications provide a clear and abstract representation of the231 application’s intended functional behavior, which simplifies the identification of key internal state variables. This is in contrast to232 the implementation level, where state variables might be fragmented into multiple concrete variables and their modifications might233 be scattered across various execution paths influenced by non-functional requirements or programming language constraints that234 are not directly derived from the core functional requirements. By generating tests from a high-level specification that explicitly235 defines the state and its transformations, we can create test cases that are more directly targeted at scrutinizing the intended236 behavior of these critical state variables and their potential for contributing to FEP.237 3.2.1 Challenges in Defining Data Flow Analysis for Haskell Specifications238 Generating accurate data flow information for Haskell programs presents substantial hurdles due to the language’s inherent239 characteristics, notably purity, immutability, and lazy evaluation. Unlike imperative programming paradigms where data flow is240 USING FUNCTIONAL SPECIFICATION TO DETECT FAILED ERROR PROPAGATION IN STATEFUL SERVICES 7 often tightly coupled with explicit control flow structures, Haskell’s functional nature and its strategy of deferred computation241 significantly complicate the construction of precise data flow graphs. Some of these difficulties echo those encountered in the242 analysis of other functional languages like Erlang and Scheme, as highlighted in the works of Widera and Zeller3 and Shivers4.243 These authors underscore the complexity arising from features such as higher-order functions, recursive definitions, and the244 absence of explicit sequential control flow instructions. They note that extracting the flow graph without considering the data245 flow is impossible, as the higher-order functions present themselves as expressions in early iterations of flow graph generation.246 While some prior research has explored the generation of data flow information for Haskell programs, to the best of our247 knowledge at the time of writing, a fully automatic tool for generating comprehensive data flow graphs and subsequently248 extracting du-paths directly from Haskell code was not readily available. As an initial exploration, we attempted to implement a249 tool aimed at measuring du-path coverage during program execution. Our tool’s design involved two main components: a static250 analysis phase that parsed the Haskell source code to construct its Abstract Syntax Tree (AST), and an annotation phase that251 instrumented the program to record a detailed execution trace at the expression level during runtime. By analyzing this runtime252 trace in conjunction with the program’s AST, we aimed to identify the specific du-paths that were exercised during a particular253 execution. We also intended to statically extract all potential du-paths from the AST to calculate a coverage score based on the254 executed paths.255 However, this initial attempt encountered a significant obstacle due to Haskell’s lazy evaluation strategy. The deferred256 evaluation resulted in a non-trivial and often discontinuous execution trace, characterized by jumps and out-of-order evaluation257 of expressions. This made it exceedingly difficult to reconstruct consistent and meaningful du-paths from the runtime data.258 Consider the illustrative example presented in Listing 2 and its corresponding flow graph in Figure 2. The flow graph is manually259 generated based on the work of 3.260 Listing 2 The impact of lazy evaluation on data flow extrac- tion for Haskell programs 1 getMax :: Int -> Int -> Int 2 getMax a b 3 | a > b = a 4 | otherwise = b 5 6 ampilfy :: Int -> Int -> Int 7 amplify c d 8 | d Int -> Int 12 f a b = amplify c 4 13 where 14 c = getMax a b f: import(Arg1, Arg2) context() return res1res1 = amplify c 4 getMax:import(Arg3, Arg4) context() Arg3, Arg4 Arg3 > Arg4 Arg3 ≤ Arg4 ret2 = Arg3 ret2 = Arg4 c = getMax Arg1 Arg2 amplify:import(Arg5, Arg6) context() Arg6 Arg6 < 5 Arg6 ≥ 5 ret3 = 2 × Arg5 ret3 = 3 × Arg5 return ret3 return ret2 1 4 2 3 5 6 3 6 F I G U R E 2 The statically generated flow graph of example Listing 2 in the style of3. 8 ZAKERIY ANET AL . F I G U R E 3 Encapsulating the state with reader and writer functions to control the access to the state As the static creation of the flow graph shows, in the execution of function f, first a call to getMax function should be261 made and then the return value of that function should be passed to the amplify function to create the f → getMax →262 amplify trace. The authors of3 introduced the concept of du-chains to address the problem of immutable variables and we263 used the same notion for creation of the flow graph. So the definitions of variables a and b are considered in line 2 and then they264 pass through getMax function where one of them is passed as the value to amplify function and then it is used to calculate265 the return value of it. So the expected execution trace is 1 → 2 → 3 → 4 → 5 → 6. Note that on each execution, one266 of the nodes marked as 3 and 6 is executed based on the input values. But the runtime execution trace generates the flow f267 → amplify → getMax → the rest of amplify (1 → 4 → 5 → 6 → 3 → 6). This jump in execution268 happens because the return value of getMax function is not calculated until it is needed. So the call to getMax function269 happens in the middle of execution of amplify function and the generated execution trace is different from the statically270 generated one shown in Figure 2.271 Given that the automatic generation of comprehensive data flow analysis information was a complex undertaking and272 represented only a part of the broader research objectives, and considering the limited time available, we made the decision273 to remove the automatic data flow generation component from the immediate scope of this paper. We intend to address this274 challenging aspect in more detail in a separate research. For the purposes of this paper, we adopted a semi-automatic approach to275 extract du-paths for key state variables as a proof of concept, acknowledging the limitations and manual effort involved.276 3.2.2 Semi-Automatic Data Flow Analysis Using Monads277 In our prior work 1, we developed a test coverage calculation mechanism leveraging the monadic structure of our specification.278 This mechanism strategically embedded instrumentation points within monadic computations to collect and output coverage279 data during execution. For this work, we extended that mechanism to capture data relevant to state variable data flow analysis in280 our Haskell specification.281 Our approach encapsulates direct access to the system’s state components via intermediary accessor and mutator functions.282 These controlled interfaces not only perform the intended state manipulations but also update the data flow trace within the monad.283 Figure 3 presents the diagram for using monads as wrapper for accessor method in state variable. The appendix B illustrates this284 design pattern: the function signatures evolve from State → AType → . . . → State to State → AType → . . . →285 Coverage State , where Coverage is a monad that wraps state operations to record data flow events.286 For example, consider the code snippet in Listing 3, extracted from our matching engine specification. Here, broker credit287 balances are updated based on transaction value. The updateCredit and getCredit functions serve as encapsulated inter-288 faces for modifying and retrieving credit information, respectively. These functions are instrumented to record definition points289 (e.g., "DF-D-credit-" ++ show bid ) and usage points (e.g., "DF-U-credit-" ++ show bid ), corresponding to290 the definition-use pairs critical for du-path coverage. By replacing all direct state accesses with calls to these functions, we291 decouple core specification logic from data flow instrumentation, facilitating flexible and modular trace collection. The recorded292 sequences of definition and usage events enable extraction of executed du-paths for coverage analysis.293 USING FUNCTIONAL SPECIFICATION TO DETECT FAILED ERROR PROPAGATION IN STATEFUL SERVICES 9 Listing 3 Defining data flow points using monads in specification 1 updateBuyerCreditByTrade :: MEState -> Trade -> Coverage MEState 2 updateBuyerCreditByTrade state t = 3 updateCredit state bid newCredit 4 where 5 bid = buyerBrId t 6 newCredit = getCredit bid - valueTraded t 7 8 9 updateCredit :: MEState -> BrokerId -> Int -> Coverage MEState 10 updateCredit state bid value = 11 state {creditInfo = Map.insert bid newCredit ci} 12 ‘covers‘ ("DF-D-credit-" ++ show bid) 13 where 14 ci = creditInfo state 15 newCredit = creditInfo state Map.! bid + value 16 -- Assuming ’value’ is the change in credit 17 18 getCredit :: MEState -> BrokerId -> Coverage Int 19 getCredit state bid = ci Map.! bid ‘covers‘ ("DF-U-credit-" ++ show bid) 20 where 21 ci = creditInfo state 294 3.3 The Need for Multiple Requests within a Test Case for Enhanced FEP Detection295 In our earlier work1, incorporating multiple requests within a single test case served primarily to model diverse initial states296 for the specification, thereby streamlining the test case generation process. However, for the specific goal of uncovering FEP,297 executing a sequence of multiple requests within the same continuous execution context becomes critically important.298 As previously discussed, employing data flow coverage to detect FEP necessitates focusing on execution paths that encompass299 a sub-path originating from the definition of a state variable to a subsequent usage of that same variable. For many internal300 state variables, such a complete du-path might not be fully traversed within the execution scope of a single isolated request.301 This limitation arises because, after a state variable is modified by a request, its updated value might not be utilized within the302 remaining execution flow of that same request, thus preventing any fault in the state variable’s modification from manifesting in303 the request’s output.304 However, by executing multiple requests sequentially within a single test case, we can construct execution paths that span305 across request boundaries. Specifically, a state variable might be altered by an error within the processing of one request, and306 its incorrectly modified value might then be used in a subsequent, related request within the same test case. This inter-request307 dependency allows the impact of erroneous state variable calculations to propagate and become observable in the outputs of308 these later requests, thereby significantly enhancing our ability to detect FEP.309 Consider the FEP example illustrated in Listing 1. When each test case is limited to a single request, the data corruption of the310 credit state can not be revealed as the updated value of credit is never used from that point on. In contrast, if a test case contains311 more than one request, there is a du-path that starts from one request and finished in the next request. Generating tests for this312 path increase the chance of discovering the subtle fault possible. If there is more than two requests, considering this execution313 path multiple times makes the discovery of this bug much easier as each execution leads to bigger deviation from the intended314 internal state.315 While the conventional practice for testing transactional systems often involves a single request per test case – a methodology316 that aligns well with the abstract, isolated nature of individual transactions and simplifies the verification of individual test317 outcomes – our approach leverages the specification itself as a test oracle. Because we can readily execute a sequence of requests318 against our Haskell specification and observe the resulting state transitions and outputs for each request in the sequence, the319 complexity of handling and verifying test results for multi-request test cases is significantly mitigated. This capability allows us320 to effectively harness the power of multi-request test cases to improve FEP detection without being unduly burdened by the321 challenges typically associated with verifying such complex test scenarios in traditional testing frameworks.322 10 ZAKERIY ANET AL . 4 TEST CASE GENERATION323 The primary objective of our approach is to generate an effective test suite for a SUT based on a formal specification. Given324 that we employ a metaheuristic approach, specifically a genetic algorithm, for test case generation, the design of robust fitness325 functions is paramount. This section details the metaheuristic approach we utilized and the various fitness functions we proposed326 to optimize test suite generation, particularly for capturing FEP.327 4.1 Multi-Objective Test Case Generation Approach328 We adopted a genetic algorithm as our metaheuristic search strategy for test case generation. While this approach builds upon329 the conceptual framework established in our previous work, it required a significantly refined implementation of the genetic330 algorithm itself. In our earlier research, our genetic algorithm aimed to optimize two primary objectives: minimizing the size331 of the generated test suite and maximizing the coverage achieved over the formal specification. These two objectives were332 combined into a single fitness value using a weighted linear formula. However, subsequent in-depth analysis revealed a critical333

the assigned weights to these objectives had a disproportionately large and often unpredictable impact on the genetic334 algorithm’s search behavior. Given the inherent interdependency between test suite size and specification coverage, even small335 adjustments to the weights could lead to substantial and difficult-to-predict changes in the algorithm’s performance, making the336 determination of optimal weight values a significant challenge.337 To overcome this limitation and enable a more robust and principled optimization process, we transitioned to employing a338 multi-objective genetic algorithm. This paradigm allows for the simultaneous optimization of multiple potentially conflicting339

without the need to manually define and tune arbitrary weightings. Specifically, we utilized the Non-dominated340 Sorting Genetic Algorithm II (NSGA-II), an established and widely used multi-objective evolutionary algorithm. We employed341 an off-the-shelf implementation of NSGA-II readily available from the Pymoo library ¶¶. NSGA-II operates based on the342 principle of non-dominated sorting, where individuals (in our case, candidate test suites) are ranked according to their dominance343 relationships. Solutions that are not dominated by any other solution in the population are prioritized, effectively guiding the344 search towards the Pareto frontier – a set of optimal solutions representing the best possible trade-offs between the different345 objectives. For the crossover operation, we utilized the Simulated Binary Crossover (SBX) implementation provided by the346 Pymoo library. SBX is particularly well-suited for problems with continuous variables, as it effectively explores the range of347 possible values between parent solutions, facilitating a more comprehensive search of the solution space. Similarly, for the348 mutation operator, we employed the Polynomial Mutation implementation from Pymoo. Polynomial mutation is designed to349 efficiently explore the valid ranges of the problem variables, introducing small random changes to the offspring to maintain350 diversity within the population and prevent premature convergence.351 Through the iterative processes of non-dominated sorting-based selection, SBX crossover, and polynomial mutation, NSGA-352 II effectively navigates the multi-dimensional objective space, identifying a diverse set of non-dominated test suites. These353 solutions represent a range of optimal trade-offs between the defined objectives, offering a comprehensive and balanced coverage354 of the specification while also considering the size of the generated test suite.355 4.1.1 Problem Formulation356 We adopted a problem formulation for our genetic algorithm that closely mirrors our previous work 1. To ensure this paper357 remains self-contained, we provide a concise overview of this formulation here. A key design principle of our test case generation358 approach is that the fitness of a candidate solution is evaluated over theentire test suite it represents, rather than on individual359 test cases in isolation. This idea was first presented in5. The holistic evaluation strategy is crucial for mitigating issues such as360 accidental coverage. Our initial exploratory experiments, where fitness was assessed at the individual test case level, revealed a361 tendency for simpler coverage metrics like expression coverage to become dominant early in the evolutionary process. This362 dominance often led to “accidental coverage” of other parts of the specification without the test cases being specifically designed363 to target those areas, rendering the optimization of other important objectives ineffective.364 ¶¶ https://pymoo.org/algorithms/moo/nsga2.html USING FUNCTIONAL SPECIFICATION TO DETECT FAILED ERROR PROPAGATION IN STATEFUL SERVICES 11 TC 1 TC 2 … TC 40 Flag Fixture Orders Credits Shares Ref Price Order 1 Order 2 … Order 10 Shares 1 Shares 2 … Shares 10 Order ID Broker Shareholder Price �uantity Disclosed �uantityFill and KillMin �uantitySide F I G U R E 4 The structure of a chromosome representing a test suite Figure 4 illustrates the structure of a single chromosome within our genetic algorithm, where each chromosome represents a365 complete test suite. A test suite is composed of a variable number of test cases, up to a predefined maximum.366 • Flag: specifies the presence of a test case in the final test suite. With this flag, the search-based algorithm can dynamically367 manage the number of test cases in the test suite.368 • Fixture: defines the initial state of the system before the execution of the associated Orders. This initial state includes369 parameters such as the initial credit balance for each broker, the initial ownership quantities of shares for each shareholder,370 and a reference price for the security being traded. This reference price serves to define valid ranges for order prices during371 test case generation.372 • Order: is comprised of parameters specific to different types of trading orders, along with a unique Order ID. This Order ID373 provides a mechanism to selectively exclude specific orders from a test suite during the evolutionary process, allowing the374 algorithm to explore solutions with varying numbers of orders, potentially fewer than the maximum allowed per test case.375 As previously discussed in Section 3.3, the inclusion of multiple requests within a single test case is a deliberate design choice.376 This facilitates the modeling of more complex, real-world scenarios where sequences of requests are common and, crucially,377 enhances our ability to detect FEP.378 4.2 Fitness Function379 The fitness function plays a crucial role in guiding the search process of our metaheuristic test case generation approach. In the380 context of evolutionary algorithms like genetic algorithms, the fitness function evaluates the quality of each candidate solution381 (in our case, a test suite), providing a measure that the algorithm aims to optimize. While our approach leverages the formal382 specification to compute these fitness values, our ultimate goal is to generate effective test cases for the SUT. We acknowledge383 that the relationship between specification coverage and SUT coverage is not always straightforward, necessitating careful384 consideration in our fitness function design.385 Our previous work indicated thatexpression coverage of the specification yielded the most effective test suites when evaluated386 against the SUT. Expression coverage is a source code coverage metric that considers every expression at any level of the abstract387 syntax tree for execution during testing. Building upon this prior finding, we utilize expression coverage as a baseline objective in388 our multi-objective fitness functions, particularly for capturing aspects related to control flow coverage within the specification.389 As highlighted in subsection 3.2, data flow coverage is theoretically well-suited for detecting FEP, as FEP often arises from390 issues in how state variables are defined and subsequently used. To incorporate data flow considerations into our fitness function,391 we explored two distinct methods for quantifying the data flow exercised by a test suite within the specification:392 1. Total Def-Use Path Count: This method calculates the cumulative number of def-use paths that are executed at least once393 across all test cases within the generated test suite. It aims to maximize the overall exercise of data dependencies, without394 explicitly penalizing the repeated execution of the same paths. The underlying assumption is that a higher total count of395 def-use path executions involving internal state variables increases the probability of triggering and observing FEP.396 12 ZAKERIY ANET AL . 2. Unique Def-Use Path Count: This method, in contrast, focuses on the diversity of the data flow coverage. It counts only397 the number of unique def-use paths that are executed by the test suite, regardless of how many times each unique path is398 traversed. The rationale behind this approach is that exploring a wider variety of data flow relationships involving internal399 state variables, by covering different def-use paths, might lead to a more effective detection of FEP by exposing faults under400 different execution scenarios.401 Based on these two distinct ways of measuring data flow coverage, we proposed and evaluated five different fitness functions402 for our test case generation process:403 1. Expression Coverage: This serves as our baseline fitness objective, allowing us to compare the performance of our data404 flow-oriented fitness functions against a previously established effective coverage metric. Due to changes in the genetic405 algorithm implementation, we could not directly reuse the quantitative results from our prior work, necessitating this406 baseline comparison.407 2. Du-Path Count: This fitness function directly utilizes the first data flow measurement method, aiming to maximize the408 total number of def-use paths executed within the specification by the generated test suite.409 3. Du-Unique Paths: This fitness function directly utilizes the second data flow measurement method, aiming to maximize410 the number of unique def-use paths executed within the specification by the generated test suite, prioritizing diversity in411 data flow coverage.412 4. Expression Coverage + Du-Path Count: This is a multi-objective fitness function that simultaneously optimizes two413

the expression coverage of the specification and the total count of def-use paths executed. By leveraging the414 capabilities of NSGA-II, we aim to find a balance between achieving good structural coverage (via expression coverage)415 and maximizing the exercise of data dependencies relevant to FEP.416 5. Expression Coverage + Du-Unique Paths: This is another multi-objective fitness function that simultaneously optimizes417 expression coverage of the specification and the number of unique def-use paths executed. Similar to the previous multi-418

function, this aims to balance structural coverage with the diversity of data flow coverage, hypothesizing that this419 combination will lead to more effective FEP detection in the SUT.420 We introduced the multi-objective fitness functions (options 4 and 5) because we hypothesized that relying solely on data421 flow coverage as the fitness measure for test case generation might not adequately address the structural coverage of the SUT.422 We suspected that optimizing only for data flow could potentially lead to the generation of test suites that effectively target423 data dependencies relevant to FEP but might neglect other important aspects of the SUT’s functionality, resulting in a less424 comprehensive and ultimately less effective test suite overall. Also, our current semi-automatic methodology for extracting425 def-use paths from the specification only considers paths that both originate and terminate at points where internal system state426 variables are defined or used. This limited scope means that the broader context of these du-paths within the overall application427 execution flow is not fully captured. Consequently, optimizing solely for these isolated du-paths can lead to a lack of diversity in428 the explored execution scenarios, which in turn reduces the probability of triggering the specific conditions required to expose429 FEP in the SUT. Therefore, combining data flow coverage with expression coverage aims to create a more balanced and robust430 approach to test case generation.431 5 EV ALUATION432 To rigorously assess the effectiveness of our proposed approach, we selected a real-world implementation of a stock exchange433 matching engine software system as our SUT. This complex system, consisting of approximately 148,000 lines of Java code,434 has undergone substantial testing efforts by its development team, and they were almost confident about the correctness of the435 system. Their existing test infrastructure includes a comprehensive suite of nearly 3,300 unit and Behavior-Driven Development436 (BDD) tests, more than 90 end-to-end integration tests, and a large-scale test suite containing over one million order transactions437 derived from real-world usage data of the currently active legacy system. This extensive legacy data is used to verify various438 aspects of the order processing behavior under realistic load and conditions. The development team’s estimation that testing439 activities consumed over 30% of their total development effort underscores the significant emphasis they placed on ensuring the440 quality and reliability of this critical software system.441 USING FUNCTIONAL SPECIFICATION TO DETECT FAILED ERROR PROPAGATION IN STATEFUL SERVICES 13 Haskell Specification Test Case Generation Algorithm Adapter TestExecution Engine Coverage Measurements NSGA-II Library Test Suite SUT F I G U R E 5 The high level view of our evaluation process including test case generation and execution of test on SUT Despite this impressive level of prior testing, we deliberately chose this mature and seemingly well-tested system as our442 evaluation target. Our rationale was that such a system presents a realistic and challenging scenario for our FEP-focused test443 case generation approach. We hypothesized that even in systems subjected to extensive traditional testing methodologies, subtle444 vulnerabilities related to FEP, particularly those involving the system’s internal state and its evolution across transactions, might445 still persist and remain undetected. Therefore, this sophisticated and actively used stock exchange matching engine provides a446 strong and relevant benchmark against which we can objectively evaluate the potential of our technique to uncover these elusive447 FEP issues.448 To facilitate our evaluation, we developed a formal Haskell specification that models a significant portion of the SUT’s overall449 specification, with a specific focus on the core order processing logic and the management of the system’s internal state during450 trade execution. Furthermore, we engineered a crucial adapter component. This adapter serves as a bridge between our test case451 generation framework and the SUT. Its responsibilities include converting the abstract test suites generated by our Haskell-based452 approach into the specific input format expected by the Java-based matching engine application. Additionally, the adapter is453 responsible for setting up the necessary test environment for each generated test case based on the initial state defined in the test454 case specification. This ensures consistent and reproducible execution of our generated tests against the SUT. Figure 5 provides455 an overview of our evaluation process.456 5.1 Fault Model and Targeted Mutation457 We use mutation-based fault injection for evaluating the effectiveness of a test suite in detecting FEP. To apply fault injection458 in a meaningful way, we first needed to establish a well-defined fault model that specifically targets potential FEP scenarios459 within our SUT. The internal state of the matching engine consists of order book, broker credit and position ownership, and460 security internal variables. A detailed analysis of the SUT’s specification and its observable outputs identified two critical areas461 within the system’s internal state that are particularly susceptible to FEP: broker credit and position (share) ownership. The462 order book and security internal variables are not considered since there are messages in the system output that expose them.463 Credit and position, while not directly exposed as outputs of individual transactions, play a fundamental role in the core order464 processing logic. They directly influence whether incoming orders are accepted or rejected and are updated as a consequence of465 each successful transaction. Our fault model for detecting FEP, therefore, focuses on introducing errors in the calculations and466 comparisons involving these two key aspects of the internal system state.467 To effectively model potential faults that could lead to FEP, we designed and implemented a novel, domain-specific mutation468 operator that we apply to the SUT’s codebase. There is an innate difference between the common mutation operators and469 our mutation operator. Mutation operators commonly generate bugs by changing an operation in the execution as a bug that470 might happen during development, but our mutation operator aggregates all the miscalculations that can happen during the471 execution procedure and simulates it by introducing a ratio-based perturbation to the calculated change in these values. Listing 4472 shows a simplified example of how this mutation is applied to the updateCredit method in the SUT (written in Java). The473 commented-out line represents the original, correct implementation of the credit update. The active line below it shows the474 mutated version, where the calculated amount representing the change in credit is multiplied by a RATIO before being applied475 to the broker’s credit. ThisRATIO serves as an abstraction for a range of potential miscalculations that could occur during credit476 updates, including mathematical errors in the calculation itself or incorrect conditional evaluations that ultimately lead to an477 altered change in the credit as an internal state variable. During our mutation testing experiments, we systematically varied478 14 ZAKERIY ANET AL . the RATIO and recorded the smallest deviation from 1.0 that resulted in a test failure, providing a measure of the test suite’s479 sensitivity to this type of fault.480 The RATIO parameter effectively controls the severity of the injected fault. A RATIO value very close to 1.0 represents a481 small, subtle miscalculation that leads to FEP, as the internal state is slightly corrupted without immediately causing an obvious482 failure. Conversely, a RATIO value further away from 1.0 simulates a larger, more significant miscalculation that is more likely483 to be detected by even basic testing. This tunable nature of our mutation operator allows us to simulate faulty versions of the484 SUT with varying degrees of error subtlety, enabling us to evaluate the test suite’s ability to detect FEP across a spectrum of485 fault severities. By using this ratio-based perturbation, we effectively abstract our fault model, allowing us to systematically486 explore a range of potential FEP scenarios related to miscalculations in critical internal state updates.487 Listing 4 Our mutation operator applied to the updateCredit method in the SUT 1 public void updateCredit(Money amount){488 2 {489 3 // credit = credit.increase(amount);490 4 credit = credit.increase(amount.multiply(RATIO));491 5 }492 5.2 Evaluation Methodology493 To quantify the effectiveness of our proposed test case generation approach, we employed themutation score as our primary494 evaluation metric. Mutation score is a widely accepted measure in software testing that assesses the ability of a test suite to495 detect injected faults (mutants) in the SUT. As highlighted by Jahangirova et al. 2, the characteristics and prevalence of FEP496 can significantly differ when considering system-level testing compared to unit-level testing. Their findings suggest that the497 probability of FEP occurring at the system level is substantially higher than at the unit level, both for real-world faults and498 for artificially injected faults (mutants). This crucial observation implied that the existing unit-level tests developed for our499 SUT were not a suitable baseline for evaluating the effectiveness of our system-level FEP detection strategies. Furthermore, the500 manually developed end-to-end tests, while valuable for integration testing, were also deemed inappropriate as a baseline due to501 their limited coverage of the overall system behaviors.502 Given these considerations, and building upon the findings of our previous work1, we recognized that test suites generated503 using expression coverage of the specification demonstrated superior coverage compared to the existing manually developed504 tests for our SUT. Therefore, to specifically measure the impact of incorporating data flow considerations into our test case505 generation process on the effectiveness of the resulting test suites (particularly for FEP detection), we elected to use test suites506 generated solely based on expression coverage of our Haskell specification as the baseline for our evaluation. It is important to507 note that, as mentioned in subsection 4.2, due to a different implementation of the underlying genetic algorithm in this work508 compared to our previous research, we could not directly utilize the test suites generated in 1. Instead, we generated a new set of509 baseline test suites specifically for this evaluation by optimizing solely for expression coverage of our Haskell specification510 using our current genetic algorithm framework. This ensures a fair and direct comparison with the test suites generated using our511 novel FEP-focused fitness functions.512 5.3 Bug Detection513 A significant outcome of our evaluation was the successful detection of two previously unknown FEP bugs within the real-world514 stock exchange matching engine application (SUT). This is in addition to the instances of bugs that we identified in our earlier515 work on this same system. It is important to note that these bugs cannot be discovered by our previous approach since we focused516 on generating tests that provide maximum expression coverage and, as a result, the generated tests did not focus on including the517 internal state across multiple requests to access for FEP.518 The first bug we uncovered was related to the management of position ownership. Specifically, we found a discrepancy between519 the behavior defined in our Haskell specification and the actual implementation in the SUT concerning the comparison of current520 ownership with maximum allowable ownership limits. According to our specification, if a transaction would result in a broker’s521 position ownership being equal to the maximum allowed value, the transaction should be rejected. However, we discovered that522 USING FUNCTIONAL SPECIFICATION TO DETECT FAILED ERROR PROPAGATION IN STATEFUL SERVICES 15 the SUT implementation incorrectly accepted such transactions, potentially leading to violations of ownership constraints within523 the system. This represents a subtle error in the handling of boundary conditions for a critical internal state variable.524 The second bug we identified pertained to the calculation of commission credit transactions within the SUT. The system525 has a feature to calculate and apply commission credits based on the value of placed orders. The default configuration for the526 system, which was active during the execution of our generated test suites, sets the commission rate to zero. Under this default527 setting, the intended behavior for performance optimization is that no credit transaction for commission should be created.528 Furthermore, there were explicit assertions within the SUT’s code to verify that no credit transaction with a value of zero is ever529 created. However, our generated test cases triggered a specific, less frequently executed path in the order processing logic. In this530 particular code path, a commission credit transaction was always created, regardless of the commission value. Consequently,531 when the commission rate was zero, this path led to the creation of a credit transaction with a zero value, directly violating one532 of the internal assertions designed to prevent such transactions. This scenario highlights how our approach can uncover bugs in533 less common execution paths that might be missed by more traditional testing methods.534 The discovery of these two distinct and non-trivial bugs in a mature and extensively tested real-world application provides535 empirical evidence for the practical utility and effectiveness of our specification-based test case generation approach, particularly536 in its ability to uncover subtle defects, including those related to the management of internal state and potential instances of FEP.537 5.4 Mutation Score Analysis538 To quantitatively evaluate the effectiveness of our approach in detecting injected faults related to FEP, we conducted a series of539 experiments using five different fitness functions to guide the test case generation process:540 1. Expression coverage541 2. Total du-path coverage542 3. Unique du-path coverage543 4. Combined expression and total du-path coverage544 5. Combined expression and unique du-path coverage545 For each of these five fitness functions, we generated 10 independent test suites using our genetic algorithm. To mitigate the546 potential influence of the algorithm’s inherent randomness on the results, we then calculated the average mutation ratio achieved547 by these 10 test suites for each fitness function. It’s important to note that for our mutation testing, we exclusively utilized our548 custom-designed mutation operator (as described in subsubsection 4.1.1), and the average mutation ratios for credit and position549 ownership were measured and are reported separately for each fitness function in Table 1.550 T A B L E 1 Average mutation ratio of each fitness function with regard to credit and position ownership (lower ratio indicates better fault detection). Fitness Function Mutation Ratio Credit Position Ownership Without du (expression coverage) 2.10 2.17 Total du-path 2.07 2.34 Unique du-path 2.24 2.55 Combined with total du-path 1.47 1.46 Combined with unique du-path 1.43 1.66 The results presented in Table 1 clearly indicate that employing a multi-objective fitness function that combines expression551 coverage with du-path coverage (both total and unique) yields significantly better mutation ratios (lower ratios signify more552 effective fault detection) compared to using each criterion in isolation. Test suites generated by optimizing solely for expression553 coverage, while aiming to cover all expressions in the specification, appear to lack sufficient focus on exercising the internal554 system state in ways that are likely to reveal potential FEPs. These test suites might cover the control flow logic well but may not555 adequately explore execution paths that involve multiple interactions with the same state variables across different requests.556 Similarly, simply maximizing either the total count or the number of unique du-paths in isolation also proves to be less557 effective than the combined approaches. There are two primary reasons for this. First, as mentioned in subsection 4.2, our558 du-path coverage method does not capture all the paths of execution scenarios, and as a result, optimizing solely for these559 16 ZAKERIY ANET AL . isolated du-paths can lead to a lack of diversity in the explored execution scenarios, which in turn reduces the probability of560 triggering the specific conditions required to expose FEP in the SUT.561 Second, inherent discrepancies can exist between the execution paths within our high-level Haskell specification and the562 corresponding execution paths in the Java implementation of the SUT. These differences can arise due to various factors such as563 performance optimizations implemented in the SUT or fundamental differences between the two programming paradigms. This564 was not the case when using expression coverage as the fitness function for test case generation, since our results in1 showed565 that using expression coverage can generate test suites that have near perfect branch coverage score. But, achieving high du-path566 coverage in the specification does not guarantee equivalent coverage of relevant data flows in the SUT, and there might be crucial567 execution paths in the SUT that are not directly represented as du-paths in our specification.568 The combined fitness functions effectively address these shortcomings. By simultaneously encouraging the generation of569 test suites that explore a wider range of execution paths (through expression coverage) and specifically focusing on those570 paths that involve interactions with the internal system state (through du-path coverage), we achieve a significantly enhanced571 capability for detecting FEP. Notably, the combined fitness function utilizing total du-path coverage achieved an approximate572 40% improvement in the average mutation ratio compared to the baseline fitness function that only considered expression573 coverage. This substantial improvement underscores the value of integrating data flow considerations into the test case generation574 process for effectively uncovering subtle, state-related bugs like those that can lead to FEP.575 5.5 Evaluating the Impact of Test Case Generation Parameters576 To gain a deeper understanding of how the configuration of our genetic algorithm influences its performance, we conducted577 evaluations focusing on two key parameters that we hypothesized could significantly impact the results.578 F I G U R E 6 Impact of varying test suite size and test case size on mutation ‘RATIO’ (lower is better) F I G U R E 7 Impact of varying test suite size and test case size on execution time of the genetic algorithm The first set of parameters we investigated were the test suite size (the number of test cases in a generated suite) and the test579 case size (the number of requests within a single test case). As mentioned previously, our base size settings for these parameters580 were 40 and 10, respectively. To assess their impact on the quality of the generated test suites, we conducted experiments with581 both larger and smaller values for these sizes. Figure 6 and Figure 7 illustrate the resulting average mutation ‘RATIO’ and582 execution time for these different configurations. The results indicate a trend: increasing both the test case size and the overall583 test suite size generally leads to lower mutation ‘RATIO’ but increases the execution time. Since a lower mutation ‘RATIO’584 signifies a greater ability of the test suite to detect the injected faults (indicating the discovery of more subtle errors), this suggests585 that if the longer execution time can be tolerated, larger test suites with more requests per test case tend to be more effective in586 uncovering FEP. This improvement occurs because larger test suites and longer test cases provide more opportunities to create587 diverse sequences of actions and interactions with the system’s internal state, thus increasing the chances of exercising du-paths588 USING FUNCTIONAL SPECIFICATION TO DETECT FAILED ERROR PROPAGATION IN STATEFUL SERVICES 17 that expose subtle errors. However, it is important to note that increasing these sizes also typically leads to a significant increase589 in the overall execution time required to run the generated test suites against the SUT.590 F I G U R E 8 Impact of varying the initialization space (range of valid parameter values) on mutation ‘RATIO’ (lower is better) F I G U R E 9 Impact of varying the initialization space (range of parameter values) on execution time of the genetic algorithm The second parameter we examined was the range of values for the various parameters within our genetic algorithm’s591 problem formulation. As outlined in subsubsection 4.1.1, each parameter that defines a test case (e.g., order price, quantity,592 initial credit ranges) has a defined range of permissible values. Restricting these ranges effectively reduces the size of the search593 space explored by the genetic algorithm during test case generation. Figure 8 and Figure 9 show the impact of varying these594 value ranges on the average mutation ‘RATIO’ and execution time.595 Our initial intuition was that a smaller state space would be easier to explore, so we set the initial values for base size to a small596 set of values. However, the results generally demonstrate that widening the range of possible values for the test case parameters597 tends to result in lower (better) mutation ‘RATIO’ while not meaningfully impacting the execution time. The occasional slight598 deviations from this pattern are likely due to averaging results across multiple independent runs, where in some specific test599 suites with wider ranges, the random initialization might not have produced individuals that effectively targeted the injected600 faults. Despite these minor fluctuations, the overall trend suggests that a larger, more diverse initial search space is beneficial for601 generating test suites that are effective at detecting FEP. This is because a larger state space offers more flexibility in generating602 the specific input sequences needed to trigger and observe the effects of subtle state-related faults. Consider the FEP example603 in Listing 1 from subsection 3.1. If the initial credit is constrained to a small range (e.g., 10 or less), the fault (the extra 10604 deduction) might only be revealed by generating a sequence of two orders whose combined worth is just under the initial credit.605 However, by allowing a wider range for the initial credit, the genetic algorithm has more opportunities to generate scenarios606 where a single order (or a sequence of orders) leads to the faulty path being taken and the error in the credit update becoming607 observable in subsequent operations or the final state.608 6 RELATED WORK609 Although specification-based test case generation has received considerable attention in the software testing literature, we are610 not aware of any research that directly incorporates the problem of FEP into the test generation process with the explicit goal of611 producing test cases that are more likely to detect FEP. In this section, we provide a structured overview of existing research612 related to FEP and data-flow coverage in functional languages. It should be noted that related work on using functional languages613 for specification-based test case generation has been covered in depth in1, and we encourage the reader to consult that paper for614 further details.615 18 ZAKERIY ANET AL . 6.1 Failed Error Propagation616 FEP is a well-recognized issue in software testing, especially in the context of complex, stateful, and safety-critical systems.617 While terminology and framing may differ across domains, the underlying problem of internal errors that fail to manifest at the618 output has been studied in various contexts. We categorize the literature on FEP into five major areas:619 6.1.0.1 Software Architecture-Level FEP Analysis620 Some research investigates how FEP occurs at the architectural level, focusing on error propagation between software components.621 These studies treat FEP as a reliability issue. For example, Malik et al. 6 propose a method for estimating system reliability622 by statically analyzing component interconnections to compute error propagation probabilities. The estimation is then used623 to identify the components most sensitive to system reliability. Similarly, Abdelmoez et al.7 use state information and inter-624 component messaging to quantify propagation likelihoods between software modules, aiming to identify components more625 likely to detect errors.626 6.1.0.2 Error Propagation Analysis (EPA)627 EPA techniques examine how runtime faults spread during system execution. Rubio-González and Liblit8 perform interprocedural628 static analysis to detect error propagation by comparing program execution traces to a golden (fault-free) run. For concurrent629 systems, Chan 9 addresses propagation analysis in multi-threaded applications, where golden runs are harder to establish, by630 automatically deriving invariants through source code instrumentation. Cinque et al.10 propose an empirical approach using631 runtime log analysis to build error propagation graphs, highlighting real-world traceability challenges in FEP detection.632 6.1.0.3 Sensitivity Analysis and the PIE Framework633 A major body of research examines the probability of a fault leading to an observable failure, known as sensitivity. This is634 commonly modeled using the Propagation, Infection, Execution (PIE) framework introduced by V oas11,12, which decomposes635 failure probability into three conditional probabilities for each step. Based on this framework, sensitivity analysis indicates the636 probability that a fault at a program location will lead to a failure. This work was later extended by V oas13 to address optimal637 oracle placement, where the most sensitive locations are the best candidates for placing assertions to check internal states. Xiong638 et al. 14 extend this idea by proposing inner oracles, i.e., input-specific assertions on internal states, to improve fault detection.639 However, as Jahangirova et al.2 demonstrate, FEP is rare in unit testing and becomes more prominent at the system level, where640 internal states are generally inaccessible to black-box testing techniques, making the use of inner oracles less practical.641 6.1.0.4 FEP in Coverage-Based Fault Localization (CBFL)642 In CBFL, coincidental correctness—tests that execute faulty code without causing a failure—is often treated as a symptom of643 FEP. Techniques such as those in15,16 attempt to refine fault localization using enhanced coverage metrics. Clustering-based644 and learning-based approaches 17,18,19,20 aim to identify coincidentally correct tests and isolate them from failing ones, thus645 improving the accuracy of diagnosis.646 6.1.0.5 Information-Theoretic Approaches647 FEP has also been studied through the lens of information theory. Androutsopoulos et al. 21 define squeeziness as the probability648 that different program states yield identical outputs, leading to FEP. They propose several entropy-based metrics to estimate649 this risk. Ibias et al. 22 extend this work by developing a neural network-based expert system trained on thousands of synthetic650 systems to predict FEP likelihood. Clark et al. 23 introduce normalized squeeziness, which accounts for differences in input651 domain sizes and enables more consistent comparisons across systems.652 The main difference between these works and ours is that they focus on estimating the presence of FEP in the system, whereas653 we aim to generate tests with a higher chance of revealing FEP explicitly. This difference leads to each approach providing654 estimates and hotspot locations where FEP can occur, while our approach generates test cases that make the presence of FEP655 explicit in the system outputs.656 6.2 Data-Flow in Functional Programs657 While data-flow coverage is well-studied in procedural programming, its extension to functional languages is relatively limited.658 Widera3,24 formalizes the concepts of data flow in declarative programs and provides the required definitions, focusing on a659 USING FUNCTIONAL SPECIFICATION TO DETECT FAILED ERROR PROPAGATION IN STATEFUL SERVICES 19 subset of Erlang. They note that calculating the flow graph is not possible without considering the data flow of the application,660 due to the presence of higher-order functions, which are treated as expressions in the initial extraction of the flow graph. To661 support immutable variables, they introduce the concept of du-chains, where passing a value through multiple variables is662 considered one du-path. A key point in their work is that Erlang does not employ lazy evaluation, which leads to new challenges663 in defining the flow graph.664 Fischer et al. 25 propose a mechanism and tool for calculating data flow in Haskell programs. Their approach transforms665 Haskell programs into Curry, augmenting the program to extract the definitions and usages of variables. Converting to Curry is666 advantageous because, while it preserves Haskell’s lazy evaluation, Curry enables execution using free variables. They perform a667 symbolic execution-like approach to extract data flows, supporting dynamic narrowing to capture def-use relationships. Although668 they claim their approach can work with pre-generated input values, no implementation has been provided to test this claim.669 Moreover, their approach incurs high execution times, making it impractical for use in test case generation via meta-heuristic670 algorithms. Consequently, we developed our own mechanism for extracting data flow information from program execution.671 7 CONCLUSION672 In this paper, we addressed the persistent challenge of Failed Error Propagation (FEP) in black-box testing of stateful transactional673 services. While traditional black-box testing approaches often focus on output correctness, they typically fail to detect silent674 internal state corruptions that do not immediately manifest in observable outputs. To bridge this gap, we proposed a novel675 FEP-aware test generation technique based on functional specifications written in Haskell.676 Our approach integrates du-path coverage over internal state variables as a key fitness objective within a multi-objective genetic677 algorithm. By supporting multi-request test cases and instrumenting specifications for runtime coverage tracking, we were able678 to generate test suites that more effectively detect FEP. We validated our method on a real-world financial application—a stock679 exchange order matching engine—and uncovered subtle yet critical faults that had previously gone undetected despite extensive680 manual and automated testing.681 Empirical evaluation showed that combining expression coverage with data-flow coverage leads to significantly better682 mutation scores, confirming the hypothesis that FEP detection benefits from a balanced focus on both control and data flow.683 Furthermore, our results demonstrated that parameter configurations such as test case size, test suite size, and input value ranges684 meaningfully impact fault detection effectiveness. This highlights the importance of parameter optimization in our test case685 generation approach.686 Overall, our research demonstrates that functional specifications can serve not only as a foundation for test generation but also687 as a powerful tool for uncovering hard-to-find, state-related defects. Future work includes fully automating data flow analysis for688 lazy functional programs and extending this approach to other domains with complex internal states and long execution traces.689 REFERENCES690 1. Zakeriyan A, Khosravi R, Safari H, Khamespanah E, Shamsabadi SM. Automated testing of an industrial stock market trading platform based on691 functional specification. Science of Computer Programming. 2023;225:102908.692 2. Jahangirova G, Clark D, Harman M, Tonella P. An empirical study on failed error propagation in Java programs with real faults.arXiv preprint693 arXiv:2011.10787. 2020.694 3. Widera M. Data flow considerations for source code directed testing of functional programs. In: 2004.695 4. Shivers O. Control flow analysis in Scheme. In: 1988:164–174.696 5. Fraser G, Arcuri A. Whole test suite generation. IEEE Transactions on Software Engineering. 2012;39(2):276–291.697 6. Malik P, Nautiyal L, Ram M. A method for considering error propagation in reliability estimation of component-based software systems.698 International Journal of Mathematical, Engineering and Management Sciences. 2019;4(3):635.699 7. Abdelmoez W, Nassar D, Shereshevsky M, et al. Error propagation in software architectures. In: IEEE. 2004:384–393.700 8. Rubio-González C, Gunawi HS, Liblit B, Arpaci-Dusseau RH, Arpaci-Dusseau AC. Error propagation analysis for file systems. In: 2009:270–280.701 9. Chan A, Winter S, Saissi H, Pattabiraman K, Suri N. Ipa: Error propagation analysis of multi-threaded programs using likely invariants. In: IEEE.702 2017:184–195.703 10. Cinque M, Della Corte R, Pecchia A. An empirical analysis of error propagation in critical software systems. Empirical Software Engineering.704 2020;25(4):2450–2484.705 11. V oas J, Morell L, Miller K. Predicting where faults can hide from testing.IEEE Software. 1991;8(2):41–48.706 12. V oas JM. PIE: A dynamic failure-based technique.IEEE Transactions on software Engineering. 1992;18(8):717.707 13. V oas JM, Miller KW. Putting assertions in their place. In: IEEE. 1994:152–157.708 14. Xiong Y , Hao D, Zhang L, Zhu T, Zhu M, Lan T. Inner oracles: Input-specific assertions on internal states. In: 2015:902–905.709 15. Wong WE, Qi Y , Zhao L, Cai KY . Effective fault localization using code coverage. In: . 1. IEEE. 2007:449–456.710 16. Baudry B, Fleurey F, Le Traon Y . Improving test suites for efficient fault localization. In: 2006:82–91.711 17. Masri W, Abou Assi R. Cleansing test suites from coincidental correctness to enhance fault-localization. In: IEEE. 2010:165–174.712 20 ZAKERIY ANET AL . 18. Masri W, Assi RA. Prevalence of coincidental correctness and mitigation of its impact on fault localization. ACM transactions on software713 engineering and methodology (TOSEM). 2014;23(1):1–28.714 19. Li Y , Liu C. Using cluster analysis to identify coincidental correctness in fault localization. In: IEEE. 2012:357–360.715 20. Xue X, Pang Y , Namin AS. Trimming test suites with coincidentally correct test cases for enhancing fault localizations. In: IEEE. 2014:239–244.716 21. Androutsopoulos K, Clark D, Dan H, Hierons RM, Harman M. An analysis of the relationship between conditional entropy and failed error717 propagation in software testing. In: 2014:573–583.718 22. Ibias A, Núñez M. SqSelect: Automatic assessment of failed error propagation in state-based systems. Expert Systems with Applications.719 2021;174:114748.720 23. Clark D, Hierons RM, Patel K. Normalised squeeziness and failed error propagation. Information Processing Letters. 2019;149:6–9.721 24. Widera M. Data flow coverage for testing Erlang programs. In: 2005.722 25. Fischer S, Kuchen H. Data-flow testing of declarative programs. ACM Sigplan Notices. 2008;43(9):201–212.723 724 APPENDIX725 A HANDLERS AND DECORATORS726 The code in Listing 5 presents a sample parts of the Haskell specification as a modular and composable request-processing727 pipeline for handling new orders, using monadic instrumentation to track coverage information(described at B).728 Listing 5 Defining Data Flow Points Using Monads in Specification 1 type Handler = Request -> MEState -> Coverage (Response, MEState) 2 type Decorator = Handler -> Handler 3 4 newOrderMatcher :: Handler 5 newOrderMatcher (NewOrderRq o) s = do 6 (ob, ts) 12 case rq of 13 (NewOrderRq o) -> do 14 { (rs, s’) handler rq s 21 22 -- other decorator functions 23 24 newOrderHandler :: Handler 25 newOrderHandler = 26 fillAndKillProc $ 27 ownershipCheck $ 28 creditLimitProc $ 29 newOrderMatcher 729 The core abstraction is a Handler, a function that takes a Request and current MEState (matching engine state), and730 returns a Response and updated state within the Coverage monad. A Decorator is a higher-order function that transforms731 a Handler into another one, enabling the composition of preprocessing or postprocessing logic around the base handler.732 The function newOrderMatcher represents the core order-matching logic: it processes a NewOrderRq request by733 invoking matchNewOrder, updating the order book, and returning the corresponding trades in the response.734 creditLimitProc is a sample Decorator that wraps a handler to enforce credit limits on incoming orders. It first735 delegates the request to the wrapped handler, and then checks whether the resulting trades comply with the broker’s credit limits.736 USING FUNCTIONAL SPECIFICATION TO DETECT FAILED ERROR PROPAGATION IN STATEFUL SERVICES 21 If the check passes, it updates the credit state and tags the execution path with the coverage label "CLP1"; otherwise, it rejects737 the order, returns the original state, and logs "CLP2".738 newOrderHandler composes multiple decorators, including creditLimitProc, fillAndKillProc, and739 ownershipCheck, around the base newOrderMatcher. This layered design promotes modularity and reuse while740 supporting fine-grained runtime tracking of control and data flow for test coverage analysis.741 B COVERAGE MONAD CODE742 The code in Listing 6 illustrates the use of Haskell’s State monad to track data flow coverage points during specification743 execution.744 Listing 6 Defining Data Flow Points Using Monads in Specification 1 type CoverageItem = String 2 type CoverageInfo = [CoverageItem] 3 4 emptyCoverage :: CoverageInfo 5 emptyCoverage = [] 6 7 coverageScore :: CoverageInfo -> Int 8 coverageScore = Set.size . Set.fromList 9 10 type Coverage = State CoverageInfo 11 12 covers :: a -> CoverageItem -> Coverage a 13 covers value item = do 14 curCoverage <- get 15 put (item:curCoverage) 16 return value 745 Here, CoverageInfo is defined as a list of strings representing unique coverage items, such as variable definitions and746 uses within the program. The function covers acts as an instrumentation helper that records a coverage point by updating the747 state with the given coverage item, while transparently passing through the associated value. This mechanism enables seamless748 embedding of coverage tracking into the functional specification, facilitating runtime monitoring of du-path coverage during test749 execution without disrupting the program’s logic.750