Property-based testing for Spark Streaming
Adri\'an Riesco, Juan Rodr\'iguez-Hortal\'a
TL;DR
This paper introduces a novel approach combining temporal logic and property-based testing to improve testing of Spark Streaming programs, formalizing the method and implementing it in a dedicated ScalaCheck extension.
Contribution
It presents a formal temporal logic framework and a practical testing library for Spark Streaming in Scala, enhancing expressiveness and testing capabilities.
Findings
Formalization of temporal logic for stream testing
Development of sscheck testing library
Application to Spark Streaming programs
Abstract
Stream processing has reached the mainstream in the last years, as a new generation of open source distributed stream processing systems, designed for scaling horizontally on commodity hardware, has brought the capability for processing high volume and high velocity data streams to companies of all sizes. In this work we propose a combination of temporal logic and property-based testing (PBT) for dealing with the challenges of testing programs that employ this programming model. We formalize our approach in a discrete time temporal logic for finite words, with some additions to improve the expressiveness of properties, which includes timeouts for temporal operators and a binding operator for letters. In particular we focus on testing Spark Streaming programs written with the Spark API for the functional language Scala, using the PBT library ScalaCheck. For that we add temporal logic…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Advanced Database Systems and Queries · Logic, programming, and type systems
Property-based testing for Spark Streaming
A. RIESCO
Universidad Complutense de Madrid
Spain
J. RODRÍGUEZ-HORTALÁ
[email protected] [email protected]
(2001)
Abstract
Stream processing has reached the mainstream in the last years, as a new generation of open source distributed stream processing systems, designed for scaling horizontally on commodity hardware, has brought the capability for processing high volume and high velocity data streams to companies of all sizes. In this work we propose a combination of temporal logic and property-based testing (PBT) for dealing with the challenges of testing programs that employ this programming model. We formalize our approach in a discrete time temporal logic for finite words, with some additions to improve the expressiveness of properties, which includes timeouts for temporal operators and a binding operator for letters. In particular we focus on testing Spark Streaming programs written with the Spark API for the functional language Scala, using the PBT library ScalaCheck. For that we add temporal logic operators to a set of new ScalaCheck generators and properties, as part of our testing library sscheck. Under consideration in Theory and Practice of Logic Programming (TPLP).
doi:
S0956796801004857
keywords:
Property-based testing, Linear temporal logic, First-order modal logic, Spark Streaming, Scala
1 Introduction
With the rise of Big Data technologies [Marz and Warren, 2015], distributed stream processing systems (SPS) [Akidau et al., 2013, Marz and Warren, 2015] have gained popularity in the last years. This later generation of SPS systems, characterized by a distributed architecture designed for horizontal scaling, was pioneered by Internet-related companies, that had to find innovative solutions to scale their systems to cope with the fast growth of the Internet. These companies are able to continuously process high volume streams of data by using systems like MillWheel [Akidau et al., 2013], Apache Storm [Marz and Warren, 2015], Heron [Ramasamy, 2015], S4 [Neumeyer et al., 2010], and Samza [Gorawski et al., 2014]. However, the first precedents of stream processing systems come back as far as the early synchronous data-flow programming languages like Lutin [Raymond et al., 2008] or Lustre [Halbwachs, 1992]. A plethora of new distributed SPS have arisen in the last years, with proposals like Apache Flink [Carbone et al., 2015a], Akka Streams [Kuhn and Allen, 2014], and Spark Streaming [Zaharia et al., 2013]. Among them Spark Streaming stands out as a particularly popular option in the industry. A basic indicator for that is the evolution of the search terms for different SPS on Google Trends, showing Spark Streaming as the most popular SPS from January 2016 onwards [GoogleTrends, 2018]. Spark [Zaharia et al., 2012] is a distributed processing engine designed for processing large collections of data [White, 2012]. The core abstraction of Spark is the notion of Resilient Distributed Dataset (RDD), which provides a fault tolerant implementation of distributed collections. Spark Streaming is a SPS built on top of Spark, and it is based on the notion of DStreams (Discretized Streams), which are series of RDDs corresponding to splitting an input data stream into fixed time windows called micro-batches, that are generated at a fixed rate according to a configured batch interval. Spark Streaming is synchronous in the sense that the batches for all DStreams in the program are generated at the same time, as the batch interval is met. See B for a quick introduction to Spark and Spark Streaming.
In this work we present a framework to test temporal properties on stream-processing systems. Among others, we consider that safety (something bad never happens) and liveness (something good eventually happens) properties are especially relevant in this kind of systems and might be useful for programmers. Specifically, we explore the problem of developing a testing library for Spark Streaming. We focus on Spark Streaming because its popularity implies a bigger set of potential users for our system, and in particular on its Scala API. We are interested in logic-based approaches, that nevertheless can be applied by software developers without the assistance of formal verification experts, as part of a test-driven development (TDD) cycle [Beck, 2003]. Testing an SPS-based program is intrinsically hard, because it requires handling time and events. Among the different proposals in the literature that tackle the problem of testing and modeling systems that deal with time, we follow Pnueli’s approach [Pnueli, 1986], that uses temporal logic for testing reactive systems. We define the logic , a variant of first-order linear temporal logic (LTL) [Blackburn et al., 2006] that is suitable for expressing Spark Streaming computations, which we expose to programmers as the sscheck library [Riesco and Rodríguez-Hortalá, 2017b]. This library extends ScalaCheck [Nilsson, 2014], a popular property-based testing (PBT) [Claessen and Hughes, 2011] library for Scala. In ScalaCheck a test is expressed as a property, which is a formula in a restricted version of first-order logic that relates program inputs and outputs. Each quantifier in the formula is bound to a generator function, that randomly produces values for some data type. The testing framework checks the property by evaluating it against a specified number of inputs that are produced by the generators. That provides a sound procedure for checking the validity of the formulas implied by the properties, that is not complete but that it is fast and lightweight enough to integrate in a TDD cycle—see C for an overview of PBT and ScalaCheck. sscheck extends ScalaCheck with temporal logic operators that can be used both in the generator functions for the input DStreams, and in the quantified formula that relates input and output DStreams, which simplifies expressing complex conditions on the sequence of batches for each DStream.
As DStreams are discrete, uses discrete time. Our logic also considers finite words, like those used in the field of runtime verification [Leucker and Schallhart, 2009], instead of infinite -words as usual in model checking. That allows us to easily integrate with the simple property checking mechanism of ScalaCheck. Although Spark DStreams are supposed to run indefinitely, so we might had modeled each DStream by an infinite word, in our setting we only model a finite prefix of the DStream. This allows us to implement a simple, fast, and sound procedure for evaluating test cases, based on evaluating the property on the generated finite prefix. On the other hand the procedure is not complete because only a prefix of the DStream is evaluated, but anyway PBT was not complete in the first place. Hence a test case will be a tuple of finite prefixes of DStreams, which corresponds to a finite word in this logic, and the aforementioned external quantifier ranges over the domain of finite words. We provide a precise formulation for our logic in Section 2.1, while details on how to implement properties are presented in Section 3.2, but for now let’s consider a concrete example in order to get a quick grasp of our proposal.
Example 1
We would like to test a Spark Streaming program that receives a stream of events describing user activity in some system. The program outputs a stream with the identifiers of banned users, which are users that the system has detected as abusing the system based on their activity. To keep the example simple, we assume that the input records are pairs containing a Long user id, and a Boolean value indicating whether the user has been honest at that instant. The output stream should include the ids of all those users that have been malicious now or in a previous instant. So, the test subject that implements it has type testSubject: DStream[(Long, Boolean)] => DStream[Long]).
To define a property that captures the expected behavior, we start by using sscheck to define a generator for (finite prefixes of) the input stream. As we want this input to change with time, we use a temporal logic formula to specify the generator. We start by defining the atomic non-temporal propositions, which are generators of micro batches with type Gen[Batch[(Long, Boolean)]], where Batch is a class extending Seq that represents a micro batch. We can generate good batches, where all the users are honest, and bad batches, where a user has been malicious. We generate batches of 20 elements, and use 15L as the id for the malicious user:
val batchSize = 20 val (badId, goodIds) = (15L, Gen.choose(1L, 50L)) val goodBatch = BatchGen.ofN(batchSize, goodIds.map((_, true))) val badBatch = goodBatch + BatchGen.ofN(1, (badId, false)) *
where BatchGen.ofN is a function that generates a batch with the specified number of elements, that are generated by the generator function in its second argument. In our logic , that corresponds to some predicate symbols under an interpretation structure where the domain is the set of all Scala expressions. As we are verifying a Spark Streaming program, given a for the set of all Spark RDDs, we use timed letters in that correspond to an RDD for the input and another for the output DStream, together with the time at which the letter is produced. The interpretation function would be defined as follows, assuming the usual meaning for the cardinal () and inclusion () operators for , and identifying Scala number literals with the corresponding numbers by abuse of notation.
[TABLE]
So far generators are oblivious to the passage of time. But in order to exercise the test subject thoroughly, we want to ensure that a bad batch is indeed generated, and that several arbitrary batches are generated after it, so we can check that once a user is detected as malicious, it is also considered malicious in subsequent instants. Moreover, we want all this to happen within the confines of the generated finite DStream prefix. This is where timeouts come into play. In our temporal logic we associate a timeout to each temporal operator, that constrains the time it takes for the operator to resolve. For example in a use of until with a timeout of , the second formula must hold before instants have passed, while the first one must hold until that moment. Translated to generators this means that in each generated DStream prefix a batch for the second generator is generated before batches have passed, i.e. between the first and the -th batch. This way we facilitate that the interesting events had enough time to happen during the limited fraction of time considered during the evaluation of the property:
val (headTimeout, tailTimeout, nestedTimeout) = (10, 10, 5) val gen = BatchGen.until(goodBatch, badBatch, headTimeout) ++ BatchGen.always(Gen.oneOf(goodBatch, badBatch), tailTimeout) *
The resulting generator gen has type Gen[PDStream[(Long, Boolean)]], where PDStream is a class that represents sequences of micro batches corresponding to a DStream prefix. Here headTimeout limits the number of batches before the bad batch occurs, while tailTimeout limits the number of arbitrary batches generated after that. That generator corresponds to the formula below, that is defined employing versions with timeout of classical temporal logic operators like (always for batches), or (until for batches), as well as a new “consume” operator that is basically a variant of the classical “next” operator that binds a variable to the current letter and time in the input word.
[TABLE]
The output DStream is the result of applying the test subject to the input stream. We define the assertion that completes the property as a temporal logic formula:
type U = (RDD[(Long, Boolean)], RDD[Long]) val (inBatch, outBatch) = ((: U).1, (: U).2) val formula = { val allGoodInputs = at(inBatch)( should foreachRecord(.2 == true)) val badInput = at(inBatch)( should existsRecord(_ == (badId, false))) val noIdBanned = at(outBatch)(.isEmpty) val badIdBanned = at(outBatch)( should existsRecord(_ == badId))
((allGoodInputs and noIdBanned) until badIdBanned on headTimeout) and (always { badInput ==> (always(badIdBanned) during nestedTimeout) } during tailTimeout) } *
Atomic non-temporal propositions correspond to assertions on the micro batches for the input and output DStreams. We use a syntax where the function at below is used with a projection function like inBatch or outBatch to apply an assertion on part of the current letter, e.g. the batch for the current input. The assertions foreachRecord and existsRecord are custom Specs2 assertions that allow users to check whether a predicate holds or not for all or for any of the records in an RDD, respectively. This way we are able to define non-temporal atomic propositions like allGoodInputs, that states that all the records in the input DStream correspond to honest users. But we know that allGoodInputs will not be happening forever, because gen eventually creates a bad batch, so we combine the atomic propositions using temporal operators to state things like “we have good inputs and no id banned until we ban the bad id” and “each time we get a bad input we ban the bad id for some time.” Here we use the same timeouts we used for the generators, to enforce the formula within the time interval where the interesting events are generated. Also, we use an additional nestedTimeout for the nested always. Timeouts for operators that apply an universal quantification on time, like always, limit the number of instants that the quantified formula needs to be true for the whole formula to hold. In this case we only have to check badIdBanned for nestedTimeout batches for the nested always to be evaluated to true. That corresponds to the following formula , assuming the interpretation of the predicate symbols , , , and as specified below.
[TABLE]
Finally, we use our temporal universal quantifier forAllDStream to put together the temporal generator and formula, getting a property that checks the formula for all the finite DStreams prefixes produced by the generator:
- forAllDStream(gen)(testSubject)(formula).set(minTestsOk = 20)
*The property fails as expected for a faulty stateless implementation that is not able to remember which users had been malicious in the past, and succeeds for a correct stateful implementation (see [Riesco and Rodríguez-Hortalá, 2018] for details). *
We carried out these ideas on the library sscheck [Riesco and Rodríguez-Hortalá, 2017b], previously presented in the tool paper [Riesco and Rodríguez-Hortalá, 2016b], and in a leading engineering conference [Riesco and Rodríguez-Hortalá, 2016a]. Moreover, sscheck has been discussed by others [Karau, 2015] and it has also been referred in books and technical blogs remarkable in the field [Holden Karau, 2015a, Karau and Warren, 2017], showing that it presents a good performance and that it stands as an alternative choice for state-of-the-art testing frameworks.
The present paper extends the published works above by:
- •
Improving the logic by (i) redefining the semantics of formulas using a first order structure for letters, that are evaluated under a given interpretation, (ii) introducing a new operator that allows us to bind the content and the time in the current batch, (iii) redefining the previous results for the new logic, and (iv) defining a new recursive definition that allows us to simplify formulas in a lazy way.
- •
Formally proving the theoretical results arising from the new formulation.
- •
Formalizing the generation of words from formulas.
- •
Providing extensive examples of sscheck properties, including safety and liveness properties.
The rest of the paper is organized as follows: Section 2 describes our logic for testing stream processing systems, while Section 3 presents its implementation for Spark. Section 4 discusses some related work. Finally, Section 5 concludes and presents some subjects of future work. The code of the tool, examples, and much more information is available in https://github.com/juanrh/sscheck. An extended version of this paper can be found in [Riesco and Rodríguez-Hortalá, 2018].
2 A Logic for Testing Stream Systems
We present in this section our linear temporal logic for defining properties on Spark Streaming programs. We first define the basics of the logic, then we show a stepwise formula evaluation procedure that is the basis for our prototype, and finally we formalize the generation of test cases from formulas.
2.1 A Linear Temporal Logic with Timeouts for practical specification of stream processing systems
The basis of our proposal is the logic, a linear temporal logic that combines and specializes both [Bauer et al., 2006] and First-order Modal Logic [Fitting and Mendelsohn, 1998], borrowing some ideas from TraceContract [Barringer and Havelund, 2011]. is an extension of [Alur and Henzinger, 1994] for runtime verification that takes into account that only finite executions can be checked, and hence a new value ? (inconclusive) can be returned in case a property cannot be effectively evaluated to either true () or false () in the given execution, because the word considered was too short. These values form a lattice with . uses the same domain as for evaluating formulas, and the same truth tables for the basic non-temporal logical connectives —see [Riesco and Rodríguez-Hortalá, 2018] for details. is also influenced by First-order Modal Logic, an extension to First-order of the standard propositional modal logic approach [Blackburn et al., 2006]. Although the propositional approach in [Riesco and Rodríguez-Hortalá, 2016b] was enough for generating new values and dealing with some interesting properties —including safety properties— we noticed that some other properties involving variables bound in previous letters —e.g. some liveness properties— could not be easily specified in our logic. For this reason we have extended the original version of with a binding operator inspired by a similar construction from TraceContract [Barringer and Havelund, 2011], which provides a form of universal quantification over letters, that makes it easy to define liveness properties, as we will explain in Section 3.3. Note that timeouts for universal time quantifiers help relaxing the formula so its evaluation is conclusive more often, while timeouts for existential time quantifiers like until make the formula more strict. We consider that it is important to facilitate expressing properties with a definite result, as quantifiers like exists, that often lead properties to an inconclusive evaluation, have been abandoned in practice by the PBT user community [Nilsson, 2014, Venners, 2015].
Formulae Syntax
We assume a denumerable set of variables (), a denumerable set of predicate symbols () with associated arity—with the set of predicate symbols with arity , and —, and a denumerable set of function symbols () with associated arity—with the set of function symbols with arity . Then, terms are built as:
[TABLE]
Typically, propositional formulations of LTL [Alur and Henzinger, 1994] consider words that use the power set of atomic propositions as its alphabet. However, we consider the alphabet of timed terms. Over this alphabet we define the set of finite words , i.e. finite sequences of timed terms. We use for the empty word, and the notation to denote that has length equal to , and is the letter at position in . Each letter corresponds to the term that can be observed at instant after units of time have been elapsed. For example, for a Spark Streaming program with one input DStream and one output DStream, the term would correspond to a pair of RDDs, one representing the micro batch for the input DStream at time , and another the micro batch for the output DStream at time .
It is important to distinguish between the instant , which refers to logic time and can be understood as a “counter of states,” and , which refers to real time. This real time satisfies the usual condition of monotonicity (), but does not satisfy progress (, ), since we work with finite words. It is also important to note that time is discrete but the time between successive states may be arbitrary. Also note that by the condition , time literals are also terms, and therefore we can replaces variables by terms and still obtain a term, as we will do later on in this section when defining the semantics of formulas.
The set of formulas is defined as follows:
[TABLE]
We will use the notation , as a shortcut for applications of the operator to . Although we provide a precise formulation for the interpretation of these formulas later in this section, the underlying intuitions are as follows:
- •
The first eight formulas are based on classical first order non-temporal logical connectives, including contradiction, tautology, atomic formulas based on predicate application and equality, and the negation and the usual binary connectives.
- •
, read “next ”, indicates that the formula should hold in the next state.
- •
, read “eventually in ,” indicates that holds in any of the next states (including the current one).
- •
, read “always in ,” indicates that holds in all of the next states (including the current one).
- •
, read “ holds until in ,” indicates that holds until holds in the next states, including the current one, and must hold eventually. Note that it is enough for to hold until the state previous to the one where holds.
- •
, read “ is released by in ,” indicates that holds until both and hold in the next states, including the current one. However, if never holds and always holds the formula holds as well.
- •
, read “consume the current letter to produce ”, indicates that given the letter for the current state, then the formula resulting from replacing in the variables and by and , respectively, should hold in the next state. We call this the consume operator.
We say that a formula is timeless when it does not contain any of the temporal logical connectives. An formula or term is closed or ground if it has no free variables. In our framework variables are only bound by , so in the following we will consider a function that computes the free variables of , discarding the appearances of and from when is found and collecting the rest of them, including those appearing in temporal connectives.
We will only consider closed formulas in the following. Moreover, we will use the notation to indicate that and are substituted by and , respectively. A detailed explanation on how to compute the free variables and how to apply substitutions is available in [Riesco and Rodríguez-Hortalá, 2018].
Logic for finite words
In order to evaluate our formulas, we need a way to interpret the timed terms that we use as the alphabet. In line with classical formulations of first order Boolean logic [Smullyan, 1995], formulas are evaluated in the context of an interpretation structure , which is a pair where is a non-empty set that is used as the interpreting domain, and is an interpretation function that assigns to each an interpreting function , and to each an interpreting relation . These interpretations are naturally applied to closed terms by induction on the structure of terms as . Our logic proves judgments of the form that state that considering the finite word from the position of its -th letter, the formula is evaluated to the truth value under the interpretation . In other words, if we stand at the -th letter of and start evaluating , moving forward in one letter at a time as time progresses, and using to interpret the terms that appear in the word and in the formula, we end up getting the truth value . Note that in our judgments the same interpretation structure holds “eternally” constant for all instants, while only one letter of is occurring at each instant. This is modeling what happens during the testing of a stream processing system: the code that defines how the program reacts to its inputs is the same during the execution of the program—which is modeled by a constant interpretation structure—, while the inputs of the program and their corresponding output change with time —which is modeled by the sequence of letters that is the word. This is not able to model updates in the program code, but it is expressive enough to be used during unit and integration testing, where the program code is fixed. Note the predicate symbols used in the formula correspond to the assertions used in the tests [Torreborre, 2014], whose meaning is also constant during the test execution. Judgments are defined by the following rules, where only the first rule that fits should be applied, and we assume :
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
[TABLE]
We say iff . The intuition underlying these definitions is that, if the word is too short to check all the steps indicated by a temporal operator and neither or can be obtained before finishing the word, then is obtained. Otherwise, the formula is evaluated to either or just by checking the appropriate sub-word. Note the consume operator () is the only one that accesses the word directly, and that consume is equivalent to next applied to the corresponding formula at its body: for example . It is trivial to check that timeless formulas—i.e. without temporal connectives—are always evaluated to one of the usual binary truth values of , and that timeless formulas are evaluated to the same truth value irrespective of the word and the position considered, even for or . As a consequence, some temporal formulas are true even for words with a length smaller than the number of letters referred by the temporal connectives in the formula: for example, for any and we have —next inspects the second letter, but the formula is true for the empty word because the body is trivially true—, —this always refers to 10 letters, but it holds for a word with just 2 letters because the body is a tautology—, and similarly because .
The resulting logic gives some structure to letters and words, but it is not fully a first order logic because it does not provide neither existential or universal quantifiers for words. The consume operator is somewhat a universal quantifier for letters, but can also be understood as a construct for parameter passing, like the binding operator from TraceContract [Barringer and Havelund, 2011].
Let us consider some example judgments for simple formulas, to start tasting the flavor of this logic.
Example 2
Assume the set of constants , the set of variables , and an interpretation structure for the initial model where and . Then for the word u\equiv\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,0)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}} we can construct the following formulas:
- •
, since does not appear in the first four letters.
- •
, since we have consumed the word, did not appear in those letters but the timeout has not expired.
- •
, since the property holds until the word is consumed, but the user required more steps.
- •
, since appears in the third letter, but the user wanted to check just the first two letters.
- •
, since appears in the third letter and, before that, appeared in all the letters.
- •
, since appears in all the required letters.
- •
, since the formula holds in the first three letters (note that the fourth letter is required, since the formula involves the next operator).
- •
, since in the first letter we have but we do not have until the third letter.
- •
, since holds in the second letter (that is, holds in the third letter, which can be also understood as appears in the third and fourth letters).
- •
, since the first letter is and hence the equality is evaluated to .
By using functions with arity greater than [math], and predicate symbols, we can construct more complex formulas. For example given and an interpretation structure where , , , , then we have {\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(0,0)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(1,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(2,3)}}}\vDash^{\mathcal{A}}{\lozenge_{2}\ \lambda^{o_{1}}_{x}.\lambda^{o_{2}}_{y}.leq(5,plus(x,y)}:{\top}
For some examples in this paper we will assume the Spark interpretation structure , that captures the observable semantics of a Spark program, and where timestamps are interpreted as Unix timestamps as usual in Java. We will not provide a formalization of , but the idea is that the prototype we present in Section 3 is intended to implement a procedure to prove judgments under the Spark interpretation structure. This interpretation uses the set of Scala expressions as the domain , and assumes that letters are timed tuples of terms, and that each input or output DStream has an assigned tuple index, so that each element of the tuple represents the micro batch at that instant for the corresponding DStream. This is expressive enough to express any Spark Streaming program, because the set of DStreams is fixed during the lifetime of a Spark Streaming application. Let us see some simple formulas we can write with this logic and in our prototype.
Example 3
Assuming a Spark Streaming program with one input DStream and one output DStream, the formula below expresses the requirement that the output DStream will always contain numbers greater than 0, for 10 batches. As we have one input and one output, uses timed letters in for and the set of all Spark RDDs.
[TABLE]
This formula can be written in our prototype as follows:
always(nowTime[(RDD[Int], RDD[Int])]{ (letter, time) => letter._2 should foreachRecord { _ > 0} }) during 10 *
The formula below expresses that time always increases monotonically during 10 instants:
[TABLE]
which we can express in our prototype as:
always(nextTime[(RDD[Int], RDD[Int])]{ (letter, time) => nowTime[U]{ (nextLetter, nextTime) => time.millis <= nextTime.millis } }) during 9 *
Once the formal definition has been presented, we require a decision procedure for evaluating formulas. Next we present a formula evaluation algorithm inferred from the logic presented above.
Decision procedure for
Just like ScalaCheck [Nilsson, 2014] and any other testing tool of the QuickCheck family [Claessen and Hughes, 2011, Papadakis and Sagonas, 2011], this decision procedure does not try to be complete for proving the veritative value of formulae, but just to be complete for failures, i.e. judgments to the truth value . For this purpose we define an abstract rewriting system for reductions for in the same domain as above. We write when the interpretation is implied by the context. Given a letter , a word , a set of terms , a timeout , and formulas , we have the following rules:111Formulas built with propositional operators just evaluate the sub-formulas and apply the connectives as usual.
Rules for :
\begin{array}[]{lllll}1)&u\vDash^{\mathcal{A}}p(e_{1},\ldots,e_{n})&\leadsto&\top&\text{if~{}}([\![e_{1}]\!]^{\mathcal{A}},\ldots,[\![e_{n}]\!]^{\mathcal{A}})\subseteq{\mathit{I}}(p)\\ 2)&u\vDash^{\mathcal{A}}p(e_{1},\ldots,e_{n})&\leadsto&\bot&\textrm{otherwise}\end{array} 2. 2.
Rules for :
\begin{array}[]{llll}1)&u\vDash^{\mathcal{A}}e_{1}=e_{2}&\leadsto&[\![e_{1}]\!]^{\mathcal{A}}=[\![e_{2}]\!]^{\mathcal{A}}\\ \end{array} 3. 3.
Rules for :
\begin{array}[]{llll}1)&\epsilon\vDash\lambda^{o}_{x}.\varphi&\leadsto&?\\ 2)&(e,t)u\vDash\lambda^{o}_{x}.\varphi&\leadsto&u\vDash\varphi[x\mapsto e][o\mapsto t]\\ \end{array} 4. 4.
Rules for :
\begin{array}[]{llll}1)&\epsilon\vDash X\ \varphi&\leadsto&\epsilon\vDash\varphi\\ 2)&au\vDash X\ \varphi&\leadsto&u\vDash\varphi\\ \end{array} 5. 5.
Rules for :
\begin{array}[]{lllll}1)&\epsilon\vDash\lozenge_{t}\ \varphi&\leadsto&\epsilon\vDash\varphi&\\ 2)&u\vDash\lozenge_{0}\ \varphi&\leadsto&\bot&\\ 3)&u\vDash\lozenge_{t}\ \varphi&\leadsto&\top&\text{if }u\vDash\varphi\leadsto^{*}\top\\ 4)&au\vDash\lozenge_{t}\ \varphi&\leadsto&u\vDash\lozenge_{t-1}\ \varphi&\text{if }au\vDash\varphi\leadsto^{*}\bot\\ \end{array} 6. 6.
Rules for :
\begin{array}[]{lllll}1)&\epsilon\vDash\square_{t}\ \varphi&\leadsto&\epsilon\vDash\varphi&\\ 2)&u\vDash\square_{0}\ \varphi&\leadsto&\top&\\ 3)&u\vDash\square_{t}\ \varphi&\leadsto&\bot&\text{if }u\vDash\varphi\leadsto^{*}\bot\\ 4)&au\vDash\square_{t}\ \varphi&\leadsto&u\vDash\square_{t-1}\ \varphi&\text{if }au\vDash\varphi\leadsto^{*}\top\\ \end{array} 7. 7.
Rules for :
\begin{array}[]{lllll}1)&\epsilon\vDash\varphi_{1}~{}U_{t}~{}\varphi_{2}&\leadsto&\epsilon\vDash\varphi_{2}&\\ 2)&u\vDash\varphi_{1}~{}U_{0}~{}\varphi_{2}&\leadsto&\bot&\\ 3)&u\vDash\varphi_{1}~{}U_{t}~{}\varphi_{2}&\leadsto&\top&\text{if }u\vDash\varphi_{2}\leadsto^{*}\top\\ 4)&u\vDash\varphi_{1}~{}U_{t}~{}\varphi_{2}&\leadsto&\bot&\text{if }u\vDash\varphi_{1}\leadsto^{*}\bot\wedge u\vDash\varphi_{2}\leadsto^{*}\bot\\ 5)&au\vDash\varphi_{1}~{}U_{t}~{}\varphi_{2}&\leadsto&u\vDash\varphi_{1}~{}U_{t-1}~{}\varphi_{2}&\text{if }au\vDash\varphi_{1}\leadsto^{*}\top\wedge au\vDash\varphi_{2}\leadsto^{*}\bot\\ \end{array} 8. 8.
Rules for :
\begin{array}[]{lllll}1)&\epsilon\vDash\varphi_{1}~{}R_{t}~{}\varphi_{2}&\leadsto&\epsilon\vDash\varphi_{1}&\\ 2)&u\vDash\varphi_{1}~{}R_{0}~{}\varphi_{2}&\leadsto&\top\\ 3)&u\vDash\varphi_{1}~{}R_{t}~{}\varphi_{2}&\leadsto&\top&\text{if }u\vDash\varphi_{1}\leadsto^{*}\top\wedge u\vDash\varphi_{2}\leadsto^{*}\top\\ 4)&u\vDash\varphi_{1}~{}R_{t}~{}\varphi_{2}&\leadsto&\bot&\text{if }u\vDash\varphi_{2}\leadsto^{*}\bot\\ 5)&au\vDash\varphi_{1}~{}R_{t}~{}\varphi_{2}&\leadsto&u\vDash\varphi_{1}~{}R_{t-1}~{}\varphi_{2}&\text{if }au\vDash\varphi_{1}\leadsto^{*}\bot\wedge au\vDash\varphi_{2}\leadsto^{*}\top\\ \end{array}
for the empty word. These rules follow this schema: (i) an inconclusive value is returned when the empty word is found; (ii) the formula is appropriately evaluated when the timeout expires; (iii) it evaluates the subformulas to check whether a value can be obtained; it consumes the current letter and continues the evaluation; and (iv) inconclusive is returned if the subformulas are evaluated to inconclusive as well, and hence the previous rules cannot be applied. Hence, note that these rules have conditions that depend on the future. This happens in rules with a condition involving that inspects not only the first letter of the word, i.e., what is happening now, but also the subsequent letters, as illustrated by the following examples:
Example 4
We recall the word u\equiv\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,0)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}} from Example 2 and evaluate the following formulas:
- •
\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,0)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash\square_{2}(\lambda^{o}_{x}.x=b)\rightarrow(\lozenge_{2}~{}\lambda^{p}_{y}.y=a)\leadsto\bot, because first the in is bound to and hence the premise holds, but \framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,0)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash(\lozenge_{2}\lambda^{p}_{y}.y=a)\leadsto\\ \framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash(\lozenge_{1}~{}\lambda^{p}_{y}.y=a)\leadsto\\ \framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash(\lozenge_{0}\lambda^{p}_{y}.y=a)\leadsto\bot.
- •
\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,0)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash(\lambda^{o}_{x}.x=b)~{}U_{2}~{}X(\lambda^{p}_{y}.y=a\wedge X\lambda^{q}_{z}.z=a)\leadsto\\ \framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash(\lambda^{o}_{x}.x=b)~{}U_{1}~{}X(\lambda^{p}_{y}.y=a\wedge X\lambda^{q}_{z}.z=a), which requires to check the second and third letters to check that the second formula does not hold. Then we have \framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash(\lambda^{o}_{x}.x=b)~{}U_{1}~{}X(\lambda^{p}_{y}.y=a\wedge X\lambda^{q}_{z}.z=a)\leadsto\top after checking the third and fourth letters.
- •
\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,0)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash\lambda^{o}_{x}.\square_{o+6}{x=b}\leadsto\\ \framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash\square_{6}{\top}, just by binding the variables. Then we have \framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash\square_{6}{\top}\leadsto\\ \framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash\square_{5}{\top}\leadsto\\ \framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}\vDash\square_{4}{\top}\leadsto\varepsilon\vDash\square_{3}{\top}\leadsto\varepsilon\vDash\top\leadsto\top just by applying the rules for .
To use this procedure as the basis for our implementation, we would had to keep a list of suspended alternatives for each of the rules above, that are pending the resolution of the conditions that define each alternative, which will be solved in the future. For example if we apply rule 5 to an application of for a non empty word and then we get 2 alternatives for sub-rules 5.3 and 5.4, and those alternatives will depend on whether the nested formula is reduced to or using , which cannot be determined at the instant when rule 5 is applied. This is because, although we do have all the batches for a generated test case corresponding to an input stream, the batches for output streams generated by transforming the input will be only generated after waiting the corresponding number of instants, as our implementation runs the actual code that is the subject of the test in a local Spark cluster. This leads to a complex and potentially expensive computation, since many pending possible alternatives have to be kept open. Instead of using this approach, it would be much more convenient to define a stepwise method with transition rules that only inspect the first letter of the input word.
2.2 A transformation for stepwise evaluation
In order to define this stepwise evaluation, it is worth noting that all the properties are finite (that is, all of them can be proved or disproved after a finite number of steps). It is hence possible to express any formula only using the temporal operators next and consume, which leads us to the following definition.
Definition 2.1** (Next form)**
We say that a formula is in next form iff. it is built by using the following grammar:
[TABLE]
We can extend the transformation in [Riesco and Rodríguez-Hortalá, 2016b] for computing the next form of any formula :
Definition 2.2** (Explicit next transformation)**
Given a formula , the function computes another formula , such that is in next form and .
\begin{array}[]{llll}\mathit{nt}^{e}(\varphi)&=&\varphi&\textrm{ if }\varphi\in\{\top,\bot,p(e_{1},\ldots,e_{n}),e_{1}=e_{2}\}\\ \mathit{nt}^{e}(\mathit{op}\ \varphi)&=&\mathit{op}\ \mathit{nt}^{e}(\varphi)&\textrm{ if }\mathit{op}\in\{\neg,X,\lambda^{o}_{x}\}\\ \mathit{nt}^{e}(\varphi_{1}\ \mathit{op}\ \varphi_{2})&=&\mathit{nt}^{e}(\varphi_{1})\ \mathit{op}\ \mathit{nt}^{e}(\varphi_{2})&\textrm{ if }\mathit{op}\in\{\vee,\wedge,\rightarrow\}\\ \end{array}**
\begin{array}[]{lll}\mathit{nt}^{e}(\lozenge_{t}\varphi)&=&\mathit{nt}^{e}(\varphi)\vee X\mathit{nt}^{e}(\varphi)\vee\ldots\vee X^{t-1}\mathit{nt}^{e}(\varphi)\\ \mathit{nt}^{e}(\square_{t}\varphi)&=&\mathit{nt}^{e}(\varphi)\wedge X\mathit{nt}^{e}(\varphi)\wedge\ldots\wedge X^{t-1}\mathit{nt}^{e}(\varphi)\\ \mathit{nt}^{e}(\varphi_{1}~{}U_{t}~{}\varphi_{2})&=&\mathit{nt}^{e}(\varphi_{2})\vee(\mathit{nt}^{e}(\varphi_{1})\wedge X\mathit{nt}^{e}(\varphi_{2}))\vee\\ &&(\mathit{nt}^{e}(\varphi_{1})\wedge X\mathit{nt}^{e}(\varphi_{1})\wedge X^{2}\mathit{nt}^{e}(\varphi_{2}))\vee\ldots\vee\\ &&(\mathit{nt}^{e}(\varphi_{1})\wedge X\mathit{nt}^{e}(\varphi_{1})\wedge\ldots\wedge X^{t-2}\mathit{nt}^{e}(\varphi_{1})\wedge X^{t-1}\mathit{nt}^{e}(\varphi_{2}))\\ \mathit{nt}^{e}(\varphi_{1}~{}R_{t}~{}\varphi_{2})&=&(\mathit{nt}^{e}(\varphi_{2})\wedge X\mathit{nt}^{e}(\varphi_{2})\wedge\ldots\wedge X^{t-1}\mathit{nt}^{e}(\varphi_{2}))\vee\\ &&(\mathit{nt}^{e}(\varphi_{1})\wedge\mathit{nt}^{e}(\varphi_{2}))\vee(\mathit{nt}^{e}(\varphi_{2})\wedge X(\mathit{nt}^{e}(\varphi_{1})\wedge\mathit{nt}^{e}(\varphi_{2})))\vee\\ &&(\mathit{nt}^{e}(\varphi_{2})\wedge X\mathit{nt}^{e}(\varphi_{2})\wedge X^{2}(\mathit{nt}^{e}(\varphi_{1})\wedge\mathit{nt}^{e}(\varphi_{2})))\vee\ldots\vee\\ &&(\mathit{nt}^{e}(\varphi_{2})\wedge X\mathit{nt}^{e}(\varphi_{2})\wedge\ldots\wedge X^{t-2}\mathit{nt}^{e}(\varphi_{2})\wedge X^{t-1}(\mathit{nt}^{e}(\varphi_{1})\wedge\mathit{nt}^{e}(\varphi_{2}))\\ \end{array}* for , , , and .*
Note that (i) it is not always possible to compute the next form a priori, since the time in temporal operators might contain variables that need to be bound and (ii) the transformation might produce large formulas. For these reasons, it is worth transforming the formula following a lazy strategy, which only generates the subformulas required in the current and the next states. We present next a recursive function that allows us to compute the next form in a lazy way, which we use to improve the efficiency of our prototype, as we will see in Section 3.1.
Definition 2.3** (Recursive next transformation)**
Given a formula , the function computes another formula , such that is in next form and .
[TABLE]
for , , , and .
Next, we present some results about these transformations and an auxiliary lemma that indicates that, if two formulas are equivalent at time , then they keep being equivalent the rest of the execution:
Lemma 2.1
Given an alphabet and formulas , if then .
Theorem 1** (Transformation equivalence)**
Given a formula such that does not contain variables in temporal connectives, we have .
It is straightforward to see that the formula obtained by this transformation is in next form, since it only introduces formulas using the temporal operators next or consume. The equivalence between formulas is stated in Theorem 2:
Theorem 2
Given an alphabet , an interpretation , and formulas , such that , we have .
Both theorems are proved by induction in the structure of formulas and using Lemma 2.1. Detailed proofs are available in A.
The show next some examples of explicit transformation and the first step of the lazy transformation.
Example 5
We present here how to transform some of the formulas from Example 2. Note that the last one cannot be completely transformed a priori:
- •
**
- •
**
- •
**
- •
**
Example 6
We present the lazy next transformation for some formulas, where we just apply the first transformation. Note that in the last example it is not possible to compute the next form in an eager way:
- •
**
- •
**
Once the next form of a formula has been computed, it is possible to evaluate it for a given word just by traversing its letters. We just evaluate the atomic formulas in the present moment (that is, those properties that does not contain the next operator) and remove the next operator otherwise, so these properties will be evaluated for the next letter. This method is detailed as follows:
Definition 2.4** (Letter simplification)**
Given a formula in next form, a letter , where can be either , with , or the empty letter , and an interpretation , the function ( when is clear from the context) simplifies with s as follows:
\begin{array}[]{llll}\mathit{ls}(\varphi,s)&=&\varphi&\textrm{if }\varphi\in\{\top,\bot\}\\ \mathit{ls}^{\mathcal{A}}(p(e_{1},\ldots,e_{n}),s)&=&([\![e_{1}]\!]^{\mathcal{A}},\ldots,[\![e_{n}]\!]^{\mathcal{A}})\subseteq{\mathit{I}}(p)&\\ \mathit{ls}^{\mathcal{A}}(e_{1}=e_{2},s)&=&\mathit{synEq}([\![e_{1}]\!]^{\mathcal{A}},[\![e_{2}]\!]^{\mathcal{A}})&\\ \mathit{ls}(\psi_{1}\ \mathit{op}\ \psi_{2},s)&=&\mathit{ls}(\psi_{1},s)\ \mathit{op}\ \mathit{ls}(\psi_{2},s)&\textrm{if }\mathit{op}\in\{\vee,\wedge,\rightarrow\}\\ \mathit{ls}(X\psi,(e,t))&=&\psi&\\ \mathit{ls}(X\psi,\emptyset)&=&\mathit{ls}(\psi,\emptyset)&\\ \mathit{ls}(\lambda^{o}_{x}.\psi,(e,t))&=&\psi[x\mapsto e][o\mapsto t]&\\ \mathit{ls}(\lambda^{o}_{x}.\psi,\emptyset)&=&?&\\ \end{array}**
where stands for syntactic equality. Note that using the empty letter forces the complete evaluation of the formula. Using this function and applying propositional logic and the interpretation when definite values are found it is possible to evaluate formulas in a step-by-step fashion.222Note that the value ? is only reached when the word is consumed and this simplification cannot be applied. In this way, we can solve the formulas from the previous example as illustrated in the next example.
Example 7
We present here the lazy evaluation process for some formulas in Example 4 using the word u\equiv\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,0)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(b,2)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,3)}}\thickspace\framebox[30.1388pt][c]{\rule{0.0pt}{6.45831pt}\smash{(a,6)}}.
- •
* (from Example 6).*
- –
.
- –
.
- •
* (from Example 6).*
- –
**
- –
**
- –
**
- –
**
- –
**
- –
**
When no variables appear in the timeouts of temporal operators, the next transformation gives also the intuition that inconclusive values can be avoided if we use a word as long as the number of next/consume operators nested in the transformation.333Note that it might be possible to avoid an inconclusive value with shorter words, so this is a sufficient condition. We define this safe word length as follows:
Definition 2.5** (Safe word length)**
Given a formula without variables in any timeouts of the temporal operators that occur in it, its longest required check is the maximum word length of a word such that we have . It is defined as follows:
\begin{array}[]{llll}\mathit{swl}(\varphi)&=&0&\textrm{if }\varphi\in\{\top,\bot,p(e_{1},\ldots,e_{n}),\\ &&&e_{1}=e_{2}\}\\ \mathit{swl}(\neg\varphi)&=&\mathit{swl}(\varphi)&\\ \mathit{swl}(\varphi_{1}\ \mathit{op}\ \varphi_{2})&=&\mathit{max}(\mathit{swl}(\varphi_{1}),\mathit{swl}(\varphi_{2}))&\textrm{if }\mathit{op}\in\{\vee,\wedge,\rightarrow\}\\ \mathit{swl}(\mathit{op}\ \varphi)&=&\mathit{swl}(\varphi)+1&\textrm{if }\mathit{op}\in\{X,\lambda^{o}_{x}\}\\ \mathit{swl}(\mathit{op}_{t}\ \varphi)&=&\mathit{swl}(\varphi)+(t-1)&\textrm{if }\mathit{op}\in\{\lozenge,\square\}\\ \mathit{swl}(\varphi_{1}~{}U_{t}~{}\varphi_{2})&=&\mathit{max}(\mathit{swl}(\varphi_{1}),\mathit{swl}(\varphi_{2}))+(t-1)&\textrm{if }\mathit{op}\in\{U,R\}\\ \end{array}**
Example 8
We present here the safe word length for some of the formulas in Example 2:
- •
.
- •
.
On the other hand, we cannot define a safe word length for arbitrary formulas with variables in timeouts, because an application of the consume operator might bind those variables using a letter of the input word, so there is no way to determine the value of the timeout for all possible words.
2.3 Generating words
Besides stating properties, formulas can be used to generate words. In particular, we will generate sequences of terms from formulas; these sequences can then be extended by pairing each letter with a number generated by an arbitrary monotonically increasing function, hence obtaining words with timed terms as letters. The formulas used for generating terms have the following restrictions:
- •
Given a formula , we have . Since in this stage we do not generate times, they cannot be used.
- •
Formulas do not contain the negation operator or the false constant. The process tries to generate words that make the formula evaluate to true, so we would not generate any word for a contradiction. Besides, we do not support negation because that would imply maintaining a set of excluded words, and we wanted to define simple ScalaCheck generators in a straightforward way.
For describing how the generators compute the sequences we first need to introduce a constant that stands for an erroneous sequence. Moreover, we use the notation () for composing words, and extend the union on as:
[TABLE]
for and . Note that we assume that syntax for sets and unions is defined in . Using these ideas, we have:
Definition 2.6** (Random word generation)**
Given an interpretation , , , formulas , , and in next form, the function ( when is clear from the context) generates a finite word . If different equations can be applied for a given formula any of them can be chosen:
\begin{array}[]{llll}\mathit{gen}(\top)&=&\emptyset&\\ \mathit{gen}^{\mathcal{A}}(p(e_{1},\ldots,e_{n}))&=&\emptyset&\textrm{if ([![e_{1}]!]^{\mathcal{A}},\ldots,[![e_{n}]!]^{\mathcal{A}})\subseteq{\mathit{I}}(p)}\\ \mathit{gen}^{\mathcal{A}}(e_{1}=e_{2})&=&\emptyset&\textrm{if [![e_{1}]!]^{\mathcal{A}}=[![e_{2}]!]^{\mathcal{A}}}\\ \mathit{gen}(\psi_{1}\vee\psi_{2})&=&\mathit{gen}(\psi_{1})&\\ \mathit{gen}(\psi_{1}\vee\psi_{2})&=&\mathit{gen}(\psi_{2})&\\ \mathit{gen}(\psi_{1}\wedge\psi_{2})&=&\mathit{gen}(\psi_{1})\cup\mathit{gen}(\psi_{2})&\\ \mathit{gen}(\psi_{1}\rightarrow\psi_{2})&=&\mathit{gen}(\psi_{2})&\\ \mathit{gen}(X\psi)&=&\emptyset+\mathit{gen}(\psi)&\\ \mathit{gen}(\lambda^{o}_{x}.\psi)&=&\{e\}+\ \mathit{gen}(\psi)&\textrm{if x\not\in\mathit{fv}(\psi)e\in{\mathit{T}erm}}\\ &&&\textrm{s.t.\ \mathit{gen}(\psi[x\mapsto e])\neq\mathit{err}}\\ \mathit{gen}(\psi)&=&\mathit{err}&\mathrm{otherwise}\\ \end{array}**
where stands for an empty term and indicates that the batch can be empty.
Note that this definition interprets conjunctions as unions. Hence, the formula is interpreted as and generates a single batch containing and .
Example 9
We present here the generation process for a formula from Example 2.
- •
* (from Example 6).*
- •
\mathit{gen}((\lambda^{o}_{x}.x=b)\rightarrow(\lambda^{p}_{y}.y=a\vee(X\mathit{nt}(\lozenge_{1}\lambda^{p}_{y}.y=a)))\wedge X\mathit{nt}(\square_{1}(\lambda^{o}_{x}.x=b)\rightarrow(\lozenge_{2}\lambda^{p}_{y}.y=a)))=\\ \mathit{gen}((\lambda^{o}_{x}.x=b)\rightarrow(\lambda^{p}_{y}.y=a\vee(X\mathit{nt}(\lozenge_{1}\lambda^{p}_{y}.y=a))))\cup\\ \mathit{gen}(X\mathit{nt}(\square_{1}(\lambda^{o}_{x}.x=b)\rightarrow(\lozenge_{2}\lambda^{p}_{y}.y=a)))=\\ \framebox[17.22217pt][c]{\rule{0.0pt}{6.45831pt}\smash{a}}\cup\framebox[17.22217pt][c]{\rule{0.0pt}{6.45831pt}\smash{\emptyset}}\thickspace\framebox[17.22217pt][c]{\rule{0.0pt}{6.45831pt}\smash{a}}=\framebox[17.22217pt][c]{\rule{0.0pt}{6.45831pt}\smash{a}}\thickspace\framebox[17.22217pt][c]{\rule{0.0pt}{6.45831pt}\smash{a}}**
Since we have, for the first term of the union:
- •
\mathit{gen}((\lambda^{o}_{x}.x=b)\rightarrow(\lambda^{p}_{y}.y=a\vee(X\mathit{nt}(\lozenge_{1}\lambda^{p}_{y}.y=a))))=\\ \mathit{gen}(\lambda^{p}_{y}.y=a\vee(X\mathit{nt}(\lozenge_{1}\lambda^{p}_{y}.y=a)))=\\ \mathit{gen}(\lambda^{p}_{y}.y=a)=\\ \framebox[17.22217pt][c]{\rule{0.0pt}{6.45831pt}\smash{a}}**
Similarly we would generate the second term of the union. Note that in both cases we decided to generate values for the first term of the disjunction. A similar process can be followed to obtain different values.
3 sscheck: using for property-based testing
We have developed a prototype that allows for using the logic for property-based testing of Spark Streaming programs, as the Scala library sscheck [Riesco and Rodríguez-Hortalá, 2017b]. This library extends the PBT library ScalaCheck [Nilsson, 2014] with custom generators for Spark DStreams and with a property factory that allows developers to check a formula against the finite DStream prefixes generated by another formula.
3.1 Design overview
In order to write a temporal property in sscheck, the user extends the trait (the Scala version of an abstract class) DStreamTLProperty, and then implements some abstract methods to configure Spark Streaming (e.g. defining the batch interval or the Spark master). The method DStreamTLProperty.forAllDStream is used to define temporal ScalaCheck properties:
type SSeq[A] = Seq[Seq[A]] type SSGen[A] = Gen[SSeq[A]]
def forAllDStream[In:ClassTag,Out:ClassTag]( generator: SSGen[In])( transformation: (DStream[In]) => DStream[Out])( formula: Formula[(RDD[In], RDD[Out])])( implicit pp1: SSeq[In] => Pretty): Prop
The function forAllDStream takes a ScalaCheck generator of sequences of sequences of elements, which are interpreted as finite DStream prefixes, so each nested sequence is interpreted as an RDD. Our library defines a case class Batch[A] that extends Seq[A] to represent an RDD for a micro batch, and a case class PDStream[A] that extends Seq[Batch[A]] to represent a finite DStream prefix. For example Batch("scala", "spark") represents an RDD[String] with 2 elements, and PDStream(Batch("scala", "spark"), Batch(), Batch("spark")) represents a finite prefix of a DStream[String] consisting of a micro batch with 2 elements, followed by an empty micro batch, and finally a micro batch with a single element. The sscheck classes BatchGen and PDStreamGen and their companion objects can be used to define generators of Batch and PDStream objects using temporal operators, and the trait Formula is used to represent formulas. See Section 3.2 below for details about the user API to write properties with sscheck. Note the type parameter of Formula is (RDD[In], RDD[Out]), which means in formula the letter corresponding to each instant is a pair of RDDs, one for the input DStream and another for the output DStream. Finally the function transformation is the test subject which correctness is checked during the evaluation of the property.
In order to evaluate the resulting ScalaCheck Prop, first we apply a lazy variant of the transformation from Definition 2.3 (see Section 3.2 for details.) to formula, in order to get an equivalent formula in next form. Then the following process iterates until the specified number of test cases has passed, or until a failing test case—i.e. a counterexample—is found, whatever happens first. A test case of type SSeq[In] is generated using generator, which corresponds to a finite prefix for the input DStream, and a fresh Spark StreamingContext is created. The test case, the streaming context, and the transformation are used to create a TestCaseContext that encapsulates the execution of the test case. The program then blocks until the test case is executed completely by the Spark runtime, and then a result for the test case is returned by the test case context. Test case results can be inconclusive, which corresponds to the truth value in , in case the generated test case is too short for the formula. Internally the test case context defines an input DStream by parallelizing the test case —using the Spark-testing-base package [Holden Karau, 2015b]—, and applies the test subject transformation to it to define an output DStream. It also maintains variables for the number of remaining batches (initialized to the length of the test case), and the current value for the formula, and registers a foreachRDD Spark action that updates the number of remaining batches, and the current formula using the letter simplification procedure from Definition 2.4. This action also stops the Spark streaming context once the formula is solved or there are no remaining batches. Other variants of forAllDStream can be used for defining properties with more than one input DStream and one output DStream.
Therefore forAllDStream(gen)(transformation)(formula) is trying to refute for the Spark interpretation structure , formulas corresponding to gen and formula respectively, and where is a word which interpretation under corresponds to the result of applying transformation to the interpretation of under , and is the sequence of time stamps starting from the unix timestamp at the start of the execution of the property and moving milliseconds at a time for the configured batch interval. Here is the usual operator that combines two sequences element wise to produce a sequence of pairs of elements in the same position, truncating the longest of the two sequences to the length of the shortest. This way we add an additional external universal quantifier on the domain of finite words, as usual in PBT, but inside that scope we have a propositional formula, and we evaluate the whole formula with the usual sound but incomplete PBT evaluation procedure.
3.2 User manual
In order to check the behaviour of a test subject transformation the user defines a property using logic by invoking the method forAllDStream[In, Out] with the following arguments:
Generator gen: Gen[Seq[Seq[In]]].
It is a regular ScalaCheck generator that produces sequences of sequences of elements, where each nested sequence represents an RDD for a Spark Streaming micro batch, and where the top sequence represent a prefix of a DStream. We represent that with the classes Batch[A](points : A*) extends Seq[A] for the batches, and PDStream[A](batches : Batch[A]*) extends Seq[Batch[A]] for the DStream prefixes. The objects PDStreamGen and BatchGen define functions for a small combinator library for ScalaCheck generators using the temporal operators of . First of all, BatchGen.ofN[T](n: Int, g: Gen[T]): Gen[Batch[T]] can be used to define a batch generator of batches of size from the elements generated by the ScalaCheck generator . We can then use BatchGen.always[A](bg: Gen[Batch[A]], t: Timeout): Gen[PDStream[A]], and PDStreamGen.always[A](dsg:Gen[PDStream[A]],t: Timeout): Gen[PDStream[A]] to build more complex generators, using operators. We also include combinator functions next, eventually, until, and release, that map to operators in the obvious way. These combinators are also available as methods for the classes BatchGen and PDStreamGen, for defining generators easily with a fluent syntax.
We currently do not include combinators for the consume operator , and generators only cover the propositional version of from [Riesco and Rodríguez-Hortalá, 2016b]. Also, just like regular ScalaCheck, we do not include functions for non temporal operators like disjunction, intersection, or implication, and rely on ScalaCheck’s Gen.oneOf for implementing the disjunction. There are also other combinators to concatenate two PDStreamGen objects, both by concatenating the one PDStream after the other –combinator ++–, and by concatenating the PDStream objects batch by batch, in an zip operation–combinator +. Examples 1, D.8, and D.10 show the usage of these combinators.
Test subject transformation: (DStream[In]) => DStream[Out].
This function that transforms an input DStream into an output DStream is the part of the production code that we are testing with the property.
Assertion formula: (RDD[In], RDD[Out]).
While the generator defines how to build input DStream prefixes, the assertion formula defines the expected relation between the input DStream and the output DStream. It is a value of type Formula[(RDD[In], RDD[Out])], for Formula a sealed trait that is extended by a case class for each operator in , following the typical implementation of an algebraic data type in Scala. This hierarchy includes the case classes Not, Or, And, Implies, Next, Eventually, Always, Until, and Release, that map to operators in the obvious way. The consume operator is represented by case class BindNext[T](timedAtomsConsumer: TimedAtomsConsumer[T]), where the class TimedAtomsConsumer[T] just adds a bit on functionality on top of a given timedLetterConsumer: Time => T => Formula[T], which is a function that defines how to consume the current letter to produce a new formula for the following letter. In this context, T would be equal to (RDD[In], RDD[Out]), containing the value of the input and output micro batches for the current instant, as corresponds to the Spark interpretation structure . Also, case class Solved[T](status : Prop.Status) represents a solved formula with a value in as correspond to the status value. Prop.Status is a type defined in the ScalaCheck library, that also includes the undefined value, and that we use to connect sscheck with ScalaCheck. Similarly to what we did for PDStream, the Formula trait and its companion object contain functions and methods or, always, etc, that define a combinator library for formulas.
Regarding other basic formulas, like predicates and equalities, we can represent them as instances of BindNext, using constant timed atoms consumer functions. Note there is no problem with checking these formulas in the next instant, because timeless formulas have the same truth value at all instants. The combinator library offers a couple of ways to express those applications of BindNext in a nicer way that direct constructor applications, that in particular integrates with the Specs2 matcher assertions that programmers are familiar with.
- •
The first one, used in examples 1, D.6, D.8, D.10, and D.11, is based on the function Formula.at[T, A, R <% Result](proj: (T) => A)(assertion: A => R): Formula[T], which builds a formula by composing a projection function on the current letter, for example to extract the input batch, with a function that builds an Spec2 matcher with the result—using Specs2’s type Result—, and uses that to build a BindNext instance with a timed atom consumer function that ignores the time argument. In this setting matchers represent predicates and equalities, and regular Scala functions and methods represent functions, which again corresponds to the Spark interpretation structure .
- •
Another option is directly using the function Formula.now[T](letterToResult: T => Result): BindNext[T] that Formula.at uses under the hood, as seen in Example D.14. There is also Formula.nowTime[T](letterToResult: (T, Time) => Result): BindNext[T] for formulas with a time component.
- •
We also have Formula.next[T](letterToFormula: T => Formula[T]): Formula[T] that again builds a BindNext instance with nicer syntax, which is called “next” instead of “now” because we do not know if the result formula will be timeless, and so the result in the next instant would not necessarily be applicable to the current instant. See e.g. examples D.8, and D.14. There is also a version Formula.nextTime for using time. In Example 3 we see example usages of nowTime and nextTime.
- •
Finally, functions and methods or, always, etc have variants that accept timed atoms consumer functions, to save some “now” and “next” applications and write the formula more succinctly, see examples D.7, D.9, D.12, D.13, and D.14.
Pretty printer witness pp1.
This is just an artifact required by ScalaCheck for printing each generated test case while reporting property evaluation results. ScalaCheck already includes implicit values for most usual types, so passing an explicitly value for this argument is rarely required.
Once the generator and the formula are defined, all that is left is using them in a test class that extends Specs2’s Specification and sscheck’s DStreamTLProperty. A Specs2 test example can be defined using DStreamTLProperty.forAllDStream invoked as forAllDStream(gen)(transformation)(formula), which returns an object of ScalaCheck’s type Prop, that can be used to launch the property check.
3.3 Verifying AMP Camp’s Twitter tutorial
In this section we give a flavor of the performance of sscheck on a more complex example, adapted for Berkeley’s AMP Camp training on Spark,444http://ampcamp.berkeley.edu/3/exercises/realtime-processing-with-spark-streaming.html adding sscheck properties for the functions implemented in that tutorial. The code for these examples is reproduced in D and it is available for download at [Riesco and Rodríguez-Hortalá, 2017a], while detailed explanations are available in [Riesco and Rodríguez-Hortalá, 2018].
Our test subject will work on a stream of tweets. A tweet is a piece of text of up to 140 characters, together with some meta-information like an identifier for the author or the creation date. Those words in a tweet that start with the # character are called “hashtags” and are used by the tweet author to label the tweet, so other users that later search for tweets with a particular hashtag can locate those related tweets easily. If many tweets use the same hashtag it becomes “popular” (a so called trending topic) and can become a topic of discussion between users. For this reason, Tweeter provides the most popular trending topics in real time, so it is worth noting that popularity is not measured in absolute terms but in a temporal window (that is, it is more popular a hashtag that appeared 10 times the last minute than one that appeared 20 times yesterday). In these examples we check the AMP Camp versions of the functions required to compute trending topics. The generators required for checking these functions consist of a stream of random tweets containing hashtags from a certain set given as parameter; we will specify, for each property, the details of the generator. We check the following properties, each corresponding to an Specs2 [Torreborre, 2014] example test function.
Hashtags correctly extracted (getHashtagsOk).
We first check whether the hashtags are correctly computed. We use a simple generator that always generates tweets with hashtags in a predefined set. Since we know beforehand the hashtags in the tweets we check that always all the tweets have at least one hashtag, and the computed hashtags are in the set of hashtags indicated by the argument given to the generator.
Hashtags correctly counted (countHashtagsOk).
We also need to make sure that, for a given period (which does not refer to real but logical time, measured by the number of batches) our functions count all appearances of hashtags. In this case our generator first generates only one hashtag (#spark) and after some time only another hashtag (#scala), both of them generated with always. For this stream we check that (i) we reach the expected amount of #spark, (ii) the amount decreases in the given window until it reaches 0, and (iii) we reach the expected amount of #scala.
Trending topic correctly found (sparkTopUntilScalaTop).
We check now that our functions select as trending topic the hashtag that has appeared most often and that this trending topic is updated if another one becomes more popular. We use an until generator that produces first tweets with the hashtags #scalacheck and #spark, using more than twice the latter, and then it keeps generating tweets with #scalacheck and #scala, but in this case #scala appears more than three times for each #scalacheck. The corresponding property checks, also with until, that the trending topic is correctly computed.
There is always exactly one top hashtag (alwaysOnlyOneTopHashtag).
Next, we check that there is always just one top hashtag by generating a stream of random tweets and then checking that the output stream of top hashtags always has a single element at each instant in time. This is a simple case of a safety property of the form .
The count of all hashtags is eventually zero (alwaysEventuallyZeroCount).
We check that the count for all hashtags reaches eventually zero by using a generator that creates a stream of tweets that starts with different hashtags and finishes with tweets without hashtags; this process is repeated inside an always operator. Then, we check that it is always the case that eventually the count for all hashtags reaches zero. Note that this property has the form of a liveness property .
Periodic trending topic (alwaysPeakImpliesEventuallyTop).
We generate for a long period random hashtags and a particular hashtag, making sure the latter happens often. Then we check that, if we reach a peak (e.g. 20 appearances in the window) then it corresponds to the particular hashtag we are generating. Note that this property has the form of a liveness property .
On Table 1 we present the execution times for these properties, as well as the number of successful generated tests cases used when checking each property. The test suite was executed on an Intel Core i7-3517U dual core 1.9 GHz and 8 GB RAM, with Spark running in local mode. That is a reasonable time for an integration test, and could be used as an automated validation step in a continuous integration pipeline [Fowler and Foemmel, 2006]. sscheck local execution could be also used for local developing to fix a broken test, using a longer batch interval configuration and smaller number of passing test cases to adapt to an scenario with less computing resources. On the other hand, if a cluster is available, sscheck could be executed using Spark distributed mode —by setting the sparkMaster field appropriately—, using a shorter batch interval, higher default parallelism, and a higher number of passing tests. In the future we also plan to develop a new feature to allow several test cases for the same property to be execute in parallel. This is not trivial because Spark is limited to a single Spark context per Java virtual machine (JVM) —see https://issues.apache.org/jira/browse/SPARK-2243.
4 Related work
At first sight, the system presented in this paper can be considered an evolution of the data-flow approaches for the verification of reactive systems developed in the past decades, exemplified by systems like Lustre [Halbwachs, 1992] and Lutin [Raymond et al., 2008]. In fact, the idea underlying both stream processing systems and data-flow reactive systems is very similar: processing a potentially infinite input stream while generating an output stream. Moreover, they usually work with formulas considering both the current state and the previous ones, which are similar to the “forward” ones presented here. There are, however, some differences between these two approaches, being an important one that sscheck is executed in a parallel way using Spark.
Lustre is a programming language for reactive systems that is able to verify safety properties by generating random input streams. The random generation provided by sscheck is more refined, since it is possible to define some patterns in the stream in order to verify some behaviors that can be omitted by purely random generators. Moreover, Lustre specializes in the verification of critical systems and hence it has features for dealing with this kind of systems, but lacks other general features as complex data-structures, although new extensions are included in every new release. On the other hand, it is not possible to formally verify systems in sscheck; we focus in a lighter approach for day-to-day programs and, since it supports all Scala features, its expressive power is greater. Lutin is a specification language for reactive systems that combines constraints with temporal operators. Moreover, it is also possible to generate test cases that depend on the previous values that the system has generated. First, these constraints provide more expressive power than the atomic formulas presented here, and thus the properties stated in Lutin are more expressive than the ones in sscheck. Although supporting more expressive formulas would be an interesting subject of future work, in this work we have focused on providing a framework where the properties are “natural” even for engineers who are not trained in formal methods; once we have examined the success of this approach we will try to move into more complex properties. Second, our framework completely separates the input from the output, and hence it is not possible to share information between these streams. Although sharing this information is indeed very important for control systems, we consider that stream processing systems usually deal with external data and hence this relation is not so relevant for the present tool. Finally, note that an advantage of sscheck consists in using the same language for both programming and defining the properties.
In a similar note, we can consider runtime monitoring of synchronous systems like Lola [D’Angelo et al., 2005], a specification language that allows the user to define properties in both past and future LTL. Lola guarantees bounded memory for monitoring and allows the user to collect statistics at runtime. On the other hand, as indicated above, sscheck allows to implement both the programs and the test in the same language and provides PBT, which simplifies the testing phase, although actual programs cannot be traced.
TraceContract [Barringer and Havelund, 2011] is a Scala library that implements a logic for analyzing sequences of events (traces). That logic is a hybrid between state machines and temporal logic, that is able to express both past time and future time temporal logic formulas, and that supports a form of first order quantification over events. The logic is implemented as a shallow internal DSL, just as we do for in sscheck, and it also supports stepwise evaluation of traces so it can be used for online monitoring of a running system, besides evaluating recorded execution traces. On the other hand, TraceContract is not able to generate test cases, and it is not integrated with any standard testing library like Specs2.
Regarding testing tools for Spark, the most clear precedent is the unit test framework Spark Test Base [Holden Karau, 2015a], which also integrates ScalaCheck for Spark but only for Spark core. To the best of out knowledge, there is no previous library supporting property-based testing for Spark Streaming.
5 Conclusions and future work
In this paper we have presented sscheck, a property-based testing tool for Spark Streaming programs. sscheck allows the user to define generators and to state properties using , an extension of Linear Temporal Logic with timeouts in temporal operators and a special operator for binding the current batch and time. This logic allows us to define a stepwise transformation that only requires/generates the current batch; using this feature the Scala implementation of sscheck takes advantage of lazy functions to efficiently implement the tool. The benchmarks presented in the paper show that the approach works well in practice. With these features in mind, we hope sscheck will be accepted by the industry; we consider the presentation at Apache Europe [Riesco and Rodríguez-Hortalá, 2016a] and citations in books written by remarkable members of the Spark community [Karau and Warren, 2017] are important steps in this direction.
There are many open lines of future work. First, adding support for arbitrary nesting of ScalaCheck forall and exists quantifiers inside formula would be an interesting extension. Moreover, we also consider developing versions for other languages with Spark API, in particular Python, or supporting other SPS, like Apache Flink [Carbone et al., 2015b] or Apache Bean [Akidau et al., 2015]. This would require novel solutions, as these systems are not based on synchronous micro-batching but they process events one at a time, and also have interesting additional features like the capability for handling different event time characteristics for supporting out of order streams, and several types of windows [Akidau et al., 2015]. Besides, we plan to explore whether the execution of several test cases in parallel minimize the test suite execution time. We could also improve the sscheck library interface, employing advanced Scala DSL techniques like the Magnet Pattern [Typesafe Inc., 2012] to make formulas easier to write and read. Finally, we intend to explore other formalisms for expressing temporal and cyclic behaviors [Wolper, 1983].
Appendix A Proofs
We present in this sections the proofs for the theorems presented in the paper.
Theorem 1. Given a formula such that does not contain variables in temporal connectives, we have .
Proof A.3**.**
We prove it by induction on the structure of the formula. The base cases are the formulas for , , terms, atomic propositions, and equalities, that are not modified and hence the property holds.
Then, it is easy to see that the property holds for the formulas defining and, or, implication, next, and consume just by applying the induction hypothesis, since both functions apply the same transformation.
Finally, we need to apply induction on the time used in temporal connectives. We present the proof for the always connective; the rest of them follow the same schema. For the base case we have:
- •
.
- •
**
This case holds by induction hypothesis in the structure of the formula. Then, assuming , with , we need to prove .
[TABLE]
Lemma 2.1. * Given an alphabet and formulas , if then . *
Proof A.4**.**
Since , , we distinguish the cases and :
It is easy to see for all possible formulas that only ? can be obtained, so the property trivially holds.
Then we have and, since we know that , the property holds.
Theorem 2. Given an alphabet , an interpretation , and formulas , such that , we have .
Proof A.5**.**
We apply induction on formulas.
Base case. It is straightforward to see that the result holds for the constants and and for an atomic predicate .
Induction hypothesis. Given the formulas , such that and , we have , .
Inductive case. We distinguish the different formulas in :
- •
For the formulas , and is straightforward to see that the result holds, since the same operators are kept and the subformulas are equivalent by hypotheses.
- •
For the formula is straightforward to see that the result holds, since it remains unchanged.
- •
For the formula is also straightforward, since by hypothesis the subformula is equivalent and then the same variables are bound.
- •
Given the formula , we have to prove that . This expression can be transformed using the definition for the satisfaction for the next operator into , which holds by hypothesis and Lemma 2.1.
- •
Given the formula , , we have to prove that . We distinguish the possible values for :
- –
. In this case the property holds because there exists , such that . Hence, by hypothesis and the definition of the next operator (note that for we just have ).
- –
. In this case , so we have for and the transformation is also evaluated to .
- –
. In this case we have of length , , and . Hence, we have for and for . Hence, we have and the property holds.
- •
The analysis for is analogous to the one for .
- •
Given the formula , , we have to prove that . We distinguish the possible values for :
- –
. In this case we have from the definition that such that and . Hence, applying the induction hypothesis we have , and hence the property holds.
- –
.
Case a) . In this case we have , and hence the complete formula is evaluated to .
- *
Case b) , , and . In this case we have and by inductive hypothesis. Hence, all the conjunctions are evaluated to and the property holds.
- –
. In this case we have of length , , , and . Hence, the first conjunctions in the transformation are evaluated to by the induction hypothesis, while the rest are evaluated to ? by the definition of the next operator and the property holds.
- •
The analysis for is analogous to the one for , taking into account that formula also holds if always holds.
Appendix B Introduction to Spark and Spark Streaming
Spark [Zaharia et al., 2012] is a distributed processing engine that was designed as an alternative to Hadoop MapReduce [Marz and Warren, 2015], but with a focus on iterative processing—e.g. to implement distributed machine learning algorithms—and interactive low latency jobs—e.g. for ad hoc SQL queries on massive datasets. The key to achieving these goals is an extended memory hierarchy that allows for an increased performance in many situations, and a data model based on immutable collections inspired in functional programming that is the basis for its fault tolerance mechanism. The core of Spark is a batch computing framework [Zaharia et al., 2012] that is based on manipulating so called Resilient Distributed Datasets (RDDs), which provide a fault tolerant implementation of distributed collections. Computations are defined as transformations on RDDs, that should be deterministic and side-effect free, as the fault tolerance mechanism of Spark is based on its ability to recompute any fragment (partition) of an RDD when needed. Hence Spark programmers are encouraged to define RDD transformations that are pure functions from RDD to RDD, and the set of predefined RDD transformations includes typical higher-order functions like map, filter, etc., as well as aggregations by key and joins for RDDs of key-value pairs. We can also use Spark actions, which allow us to collect results into the driver program or store them into an external data store. The driver program is the local process that starts the connection to the Spark cluster, and issues the execution of Spark jobs, acting as a client of the Spark cluster. Spark actions are impure, so idempotent actions are recommended in order to ensure a deterministic behavior even in the presence of recomputations triggered by the fault tolerance or speculative task execution mechanisms [Apache Spark Team, 2016]. Spark is written in Scala and offers APIs for Scala, Java, Python, and R; in this work we focus on the Scala API. The example in Figure 2 uses the Scala Spark shell to implement a variant of the famous word count example that in this case computes the number of occurrences of each character in a sentence. For that we use parallelize, a feature of Spark that allows us to create an RDD from a local collection, which is useful for testing. We start with a set of chars distributed among partitions, we pair each char with a 1 by using map, and then group by first component in the pair and sum by the second by using reduceByKey and the addition function (+), thus obtaining a set of (char, frequency) pairs. We collect this set into an Array in the driver with collect.
Besides the core RDD API, the Spark release contains a set of high level libraries that accelerates the development of Big Data processing applications, and that are also one of the reasons for its growing popularity. This includes libraries for scalable machine learning, graph processing, a SQL engine, and Spark Streaming, which is the focus of this work. In Spark Streaming, the notions of transformations and actions are extended from RDDs to DStreams (Discretized Streams), which are series of RDDs corresponding to splitting an input data stream into fixed time windows, also called micro batches. Micro batches are generated at a fixed rate according to the configured batch interval. Spark Streaming is synchronous in the sense that given a collection of input and transformed DStreams, all the batches for each DStream are generated at the same time as the batch interval is met. Actions on DStreams are also periodic and are executed synchronously for each micro batch. The code in Figure 3 is the streaming version of the code in Figure 2. In this case we process a DStream of characters, where batches are obtained by splitting a String into pieces by making groups (RDDs) of consecutive characters. We use the testing utility class QueueInputDStream, which generates batches by picking RDDs from a queue, to generate the input DStream by parallelizing each substring into an RDD with partitions. The program is executed using the local master mode of Spark, which replaces slave nodes in a distributed cluster by local threads, which is useful for developing and testing.
Appendix C Overview of property-based testing and ScalaCheck
Classical unit testing with xUnit-like frameworks [Meszaros, 2007] is based on specifying input – expected output pairs, and then comparing the expected output with the actual output obtained by applying the test subject to the input. On the other hand, in property-based testing (PBT) a test is expressed as a property, which is a formula in a restricted version of first order logic that relates program input and output. The testing framework checks the property by evaluating it against a bunch of randomly generated inputs. If a counterexample for the property is found then the test fails, otherwise it passes. This allows developers to obtain quite a good test coverage of the production code with a fairly small investment on development time, specially when compared to xUnit frameworks. However xUnit frameworks are still useful for testing corner cases that would be difficult to cover with a PBT property. The following is a “hello world” ScalaCheck property that checks the commutativity of addition:555Here we use the integration of ScalaCheck with the Specs2 [Torreborre, 2014] testing library.
class HelloPBT extends Specification with ScalaCheck { def is = s2"""Hello world PBT spec, where int addition is commutative $intAdditionCommutative"""
def intAdditionCommutative = Prop.forAll("x" |: arbitrary[Int], "y" |: arbitrary[Int]) { (x, y) => x + y === y + x }.set(minTestsOk = 100) }
PBT is based on generators (the functions in charge of computing the inputs, which define the domain of discourse for a formula) and assertions (the atoms of a formula), which together with a quantifier form a property (the formula to be checked). In the example above the universal quantifier Prop.forAll is used to define a property that checks whether the assertion x + y === y + x holds for 100 values for x and y randomly generated by two instances of the integer generator arbitrary[Int]. Each of those pairs of values generated for x and y is called a test case, and a test case that refutes the assertions of a property is called a counterexample. Here arbitrary is a higher order generator that is able to generate random values for predefined and custom types. Besides universal quantifiers, ScalaCheck supports existential quantifiers—although these are not much used in practice [Nilsson, 2014, Venners, 2015]—, and logical operators to compose properties. PBT is a sound procedure to check the validity of the formulas implied by the properties, in the sense that any counterexample that is found can be used to build a definitive proof that the property is false. However, it is not complete, as there is no guarantee that the whole space of test cases is explored exhaustively, so if no counterexample is found then we cannot conclude that the property holds for all possible test cases that could had been generated: all failing properties are definitively false, but not all passing properties are definitively true. PBT is a lightweight approach that does not attempt to perform sophisticated automatic deductions, but it provides a very fast test execution that is suitable for the test-driven development (TDD) cycle, and empirical studies [Claessen and Hughes, 2011, Shamshiri et al., 2015] have shown that in practice random PBT obtains good results, with a quality comparable to more sophisticated techniques. This goes in the line of assuming that in general testing of non trivial systems is often incomplete, as the effort of completely modeling all the possible behaviors of the system under test with test cases is not cost effective in most software development projects, except for critical systems.
Appendix D Code for AMP Camp’s Twitter tutorial with sscheck
Now we will present a more complex example, adapted for Berkeley’s AMP Camp training on Spark,666http://ampcamp.berkeley.edu/3/exercises/realtime-processing-with-spark-streaming.html but adding sscheck properties for the functions implemented in that tutorial. The complete code for these examples is available at https://github.com/juanrh/sscheck-examples/releases/tag/0.0.4.
Our test subject will be an object TweetOps, which defines a series of operations on a stream of tweets. A tweet is a piece of text of up to 140 characters, together with some meta-information like an identifier for the author or the creation date. Those words in a tweet that start with the # character are called “hashtags”, and are used by the tweet author to label the tweet, so other users that later search for tweets with a particular hashtag might locate those related tweets easily. The operations below take a stream of tweets and, respectively, generate the stream for the set of hashtags in all the tweets; the stream of pairs (hashtags, number of occurrences) in a sliding time window with the specified size777See https://spark.apache.org/docs/1.6.2/streaming-programming-guide.html#window-operations for details on Spark Streaming window operators.; and the stream that contains a single element for the most popular hashtag, i.e. the hashtag with the highest number of occurrences, again for the specified time window.
object TweetOps { def getHashtags(tweets: DStream[Status]): DStream[String] def countHashtags(batchInterval: Duration, windowSize: Int) (tweets: DStream[Status]): DStream[(String, Int)] def getTopHashtag(batchInterval: Duration, windowSize: Int) (tweets: DStream[Status]): DStream[String] }
In this code, the class twitter4j.Status from the library Twitter4J [Yamamoto, 2010] is used to represent each particular tweet. In the original AMP Camp training, the class TwitterUtils888https://spark.apache.org/docs/1.6.0/api/java/org/apache/spark/streaming/twitter/TwitterUtils.html is used to define a DStream[Status] by repeatedly calling the Twitter public API to ask for new tweets. Instead, in this example we replace the Twitter API by an input DStream defined by using an sscheck generator, so we can control the shape of the tweets that will be used as the test inputs. To do that we employ the mocking [Mackinnon et al., 2001] library Mockito [Kaczanowski, 2012] for stubbing [Fowler, 2007] Status objects, i.e. to easily synthetize objects that impersonate a real Status object, and that provide predefined answers to some methods, in this case the method that returns the text for a tweet.
object TwitterGen { /** Generator of Status mocks with a getText method
- that returns texts of up to 140 characters
- @param noHashtags if true then no hashtags are generated in the
- tweet text
- / def tweet(noHashtags: Boolean = true): Gen[Status] /* Take a Status mocks generator and return a Status mocks
- generator that adds the specified hashtag to getText
- */ def addHashtag(hashtagGen: Gen[String]) (tweetGen: Gen[Status]): Gen[Status] def tweetWithHashtags(possibleHashTags: Seq[String]): Gen[Status] def hashtag(maxLen: Int): Gen[String] def tweetWithHashtagsOfMaxLen(maxHashtagLength: Int): Gen[Status] }
D.1 Extracting hashtags
Now we are ready to write our first property, which checks that getHashtags works correctly, that is, it computes the set of hashtags (words starting with #). In the property we generate tweets that use a predefined set of hashtags, and then we check that all hashtags produced in the output are contained in that set.
Example D.6**.**
def getHashtagsOk = { type U = (RDD[Status], RDD[String]) val hashtagBatch = (_ : U)._2
val numBatches = 5 val possibleHashTags = List("#spark", "#scala", "#scalacheck") val tweets = BatchGen.ofNtoM(5, 10, tweetWithHashtags(possibleHashTags) ) val gen = BatchGen.always(tweets, numBatches)
val formula = always { at(hashtagBatch){ hashtags => hashtags.count > 0 and ( hashtags should foreachRecord(possibleHashTags.contains(_)) ) } } during numBatches
forAllDStream( gen)( TweetOps.getHashtags)( formula) } *
In the next example we use the “reference implementation” PBT technique [Nilsson, 2014] to check the implementation of TweetOps.getHashtags, which is based on the Spark transformations flatMap and filter also using String.startsWith, against a regexp-based reference implementation. This gives us a more thorough test, because we use a different randomly generated set of hashtags for each batch of each test case, instead of a predefined set of hashtags for all the test cases.
Example D.7**.**
private val hashtagRe = """#\S+""".r private def getExpectedHashtagsForStatuses(statuses: RDD[Status]) : RDD[String] = statuses.flatMap { status => hashtagRe.findAllIn(status.getText)}
def getHashtagsReferenceImplementationOk = { type U = (RDD[Status], RDD[String]) val (numBatches, maxHashtagLength) = (5, 8)
val tweets = BatchGen.ofNtoM(5, 10, tweetWithHashtagsOfMaxLen(maxHashtagLength)) val gen = BatchGen.always(tweets, numBatches)
val formula = alwaysR[U] { case (statuses, hashtags) => val expectedHashtags = getExpectedHashtagsForStatuses(statuses).cache() hashtags must beEqualAsSetTo(expectedHashtags) } during numBatches
forAllDStream( gen)( TweetOps.getHashtags)( formula) } *
D.2 Counting hashtags
In order to check countHashtags, in the following property we setup a scenario where the hashtag #spark is generated for some period, and then the hashtag #scala is generated for another period, and we express the expected counting behaviour with several subformulas: we expect to get the expected count of hashtags for spark for the first period (laterAlwaysAllSparkCount); we expect to eventually get the expected count of hastags for scala (laterScalaCount); and we expect that after reaching the expected count for spark hashtags, we would then decrease the count as time passes and elements leave the sliding window (laterSparkCountUntilDownToZero).
Example D.8**.**
def countHashtagsOk = { type U = (RDD[Status], RDD[(String, Int)]) val countBatch = (_ : U)._2
val windowSize = 3 val (sparkTimeout, scalaTimeout) = (windowSize * 4, windowSize * 2) val sparkTweet = tweetWithHashtags(List("#spark")) val scalaTweet = tweetWithHashtags(List("#scala")) val (sparkBatchSize, scalaBatchSize) = (2, 1) val gen = BatchGen.always(BatchGen.ofN(sparkBatchSize, sparkTweet), sparkTimeout) ++ BatchGen.always(BatchGen.ofN(scalaBatchSize, scalaTweet), scalaTimeout)
def countNHashtags(hashtag : String)(n : Int) = at(countBatch)(_ should existsRecord(_ == (hashtag, n : Int))) val countNSparks = countNHashtags("#spark") _ val countNScalas = countNHashtags("#scala") _ val laterAlwaysAllSparkCount = later { always { countNSparks(sparkBatchSize * windowSize) } during (sparkTimeout -2) } on (windowSize + 1) val laterScalaCount = later { countNScalas(scalaBatchSize * windowSize) } on (sparkTimeout + windowSize + 1) val laterSparkCountUntilDownToZero = later { { countNSparks(sparkBatchSize * windowSize) } until { countNSparks(sparkBatchSize * (windowSize - 1)) and next(countNSparks(sparkBatchSize * (windowSize - 2))) and next(next(countNSparks(sparkBatchSize * (windowSize - 3)))) } on (sparkTimeout -2) } on (windowSize + 1) val formula = laterAlwaysAllSparkCount and laterScalaCount and laterSparkCountUntilDownToZero
forAllDStream( gen)( TweetOps.countHashtags(batchInterval, windowSize)(_))( formula) } *
Then we check the safety of countHashtags by asserting that any arbitrary generated hashtag is never skipped in the count. Here we again exploit the reference implementation technique to extract the expected hashtags, and join this with the output counts, so we can assert that all and only all expected hastags are counted, and that those countings are never zero at the time the hashtag is generated.
Example D.9**.**
def hashtagsAreAlwasysCounted = { type U = (RDD[Status], RDD[(String, Int)]) val windowSize = 3 val (numBatches, maxHashtagLength) = (windowSize * 6, 8)
val tweets = BatchGen.ofNtoM(5, 10, tweetWithHashtagsOfMaxLen(maxHashtagLength)) val gen = BatchGen.always(tweets, numBatches)
val alwaysCounted = alwaysR[U] { case (statuses, counts) => val expectedHashtags = getExpectedHashtagsForStatuses(statuses).cache() val expectedHashtagsWithActualCount = expectedHashtags .map((, ())) .join(counts) .map{case (hashtag, (, count)) => (hashtag, count)} .cache() val countedHashtags = expectedHashtagsWithActualCount.map{_.1} val countings = expectedHashtagsWithActualCount.map{._2}
// all hashtags have been counted
countedHashtags must beEqualAsSetTo(expectedHashtags) and
// no count is zero
(countings should foreachRecord { _ > 0 })
} during numBatches
forAllDStream( gen)( TweetOps.countHashtags(batchInterval, windowSize)(_))( alwaysCounted)
} *
D.2.1 Getting the most popular hashtag
Now we check the correctness of getTopHashtag, that extracts the most “popular” hashtag, i.e. the hashtag with the highest number of occurrences at each time window. For that we use the following property where we define a scenario in which we start with the hashtag #spark as the most popular (generator sparkPopular), and after that the hashtag #scala becomes the most popular (generator scalaPopular), and asserting on the output DStream that #spark is the most popular hashtag until #scala is the most popular.
Example D.10**.**
def sparkTopUntilScalaTop = { type U = (RDD[Status], RDD[String])
val windowSize = 1 val topHashtagBatch = (_ : U)._2 val scalaTimeout = 6 val sparkPopular = BatchGen.ofN(5, tweetWithHashtags(List("#spark"))) + BatchGen.ofN(2, tweetWithHashtags(List("#scalacheck"))) val scalaPopular = BatchGen.ofN(7, tweetWithHashtags(List("#scala"))) + BatchGen.ofN(2, tweetWithHashtags(List("#scalacheck"))) val gen = BatchGen.until(sparkPopular, scalaPopular, scalaTimeout)
val formula = { at(topHashtagBatch)(_ should foreachRecord(_ == "#spark" )) } until { at(topHashtagBatch)(_ should foreachRecord(_ == "#scala" )) } on (scalaTimeout)
forAllDStream( gen)( TweetOps.getTopHashtag(batchInterval, windowSize)(_))( formula) } *
Finally, we state the safety of getTopHastag by checking that there is always one top hashtag.
Example D.11**.**
def alwaysOnlyOneTopHashtag = { type U = (RDD[Status], RDD[String]) val topHashtagBatch = (_ : U)._2
val (numBatches, maxHashtagLength) = (5, 8) val tweets = BatchGen.ofNtoM(5, 10, tweetWithHashtagsOfMaxLen(maxHashtagLength))
val gen = BatchGen.always(tweets, numBatches) val formula = always { at(topHashtagBatch){ hashtags => hashtags.count === 1 } } during numBatches
forAllDStream(gen)( TweetOps.getTopHashtag(batchInterval, 2)(_))( formula) } *
D.2.2 Defining liveness properties with the consume operator
So far we have basically defined two types of properties: properties where we simulate a particular scenario, and safety properties where we assert that we will never reach a particular “bad” state. It would be also nice to be able to write liveness properties in sscheck, which is another class of properties typically used with temporal logic, where we express that something good keeps happening with a formula of the shape of . In this kind of formulas it would be useful to define the conclusion formula that should happen later, based on the value of the word that happened when the premise formula was evaluated. This was our motivation for adding to the logic the consume operator , that can be used in liveness formulas of the shape or . One example of the former is the following liveness property for countHashtags, that checks that always each hashtag eventually gets a count of 0, if we generate empty batches at the end of the test case so all hashtags end up getting out of the counting window.
Example D.12**.**
def alwaysEventuallyZeroCount = { type U = (RDD[Status], RDD[(String, Int)]) val windowSize = 4 val (numBatches, maxHashtagLength) = (windowSize * 4, 8)
// repeat hashtags a bit so counts are bigger than 1 val tweets = for { hashtags <- Gen.listOfN(6, hashtag(maxHashtagLength)) tweets <- BatchGen.ofNtoM(5, 10, addHashtag(Gen.oneOf(hashtags))(tweet(noHashtags=true))) } yield tweets val emptyTweetBatch = Batch.empty[Status] val gen = BatchGen.always(tweets, numBatches) ++ BatchGen.always(emptyTweetBatch, windowSize*2)
val alwaysEventuallyZeroCount = alwaysF[U] { case (statuses, ) => val hashtags = getExpectedHashtagsForStatuses(statuses) laterR[U] { case (, counts) => val countsForStatuses = hashtags .map((, ())) .join(counts) .map{case (hashtag, (, count)) => count} countsForStatuses should foreachRecord { _ == 0} } on windowSize*3 } during numBatches
forAllDStream(gen)( TweetOps.countHashtags(batchInterval, windowSize)(_))( alwaysEventuallyZeroCount) } *
One example of the second kind of liveness properties, that use an implication in the body of an always, is the following property for getTopHashtag, that checks that if we superpose two generators, one for a random noise of hashtags that have a small number of occurrences (generator tweets), and another for a periodic peak of a random hashtag that suddenly has a big number of occurrences (generator tweetsSpike), then each time a peak happens then the corresponding hashtag eventually becomes the top hashtag.
Example D.13**.**
def alwaysPeakImpliesEventuallyTop = { type U = (RDD[Status], RDD[String]) val windowSize = 2 val sidesLen = windowSize * 2 val numBatches = sidesLen + 1 + sidesLen val maxHashtagLength = 8 val peakSize = 20
val emptyTweetBatch = Batch.empty[Status] val tweets = BatchGen.always( BatchGen.ofNtoM(5, 10, tweetWithHashtagsOfMaxLen(maxHashtagLength)), numBatches) val popularTweetBatch = for { hashtag <- hashtag(maxHashtagLength) batch <- BatchGen.ofN(peakSize, tweetWithHashtags(List(hashtag))) } yield batch val tweetsSpike = BatchGen.always(emptyTweetBatch, sidesLen) ++ BatchGen.always(popularTweetBatch, 1) ++ BatchGen.always(emptyTweetBatch, sidesLen) // repeat 6 times the superposition of random tweets // with a sudden spike for a random hastag val gen = Gen.listOfN(6, tweets + tweetsSpike).map{.reduce(++_)}
val alwaysAPeakImpliesEventuallyTop = alwaysF[U] { case (statuses, ) => val hashtags = getExpectedHashtagsForStatuses(statuses) val peakHashtags = hashtags.map{(,1)}.reduceByKey{+} ΨΨΨ .filter{_.2 >= peakSize}.keys.cache() val isPeak = Solved[U] { ! peakHashtags.isEmpty } val eventuallyTop = laterR[U] { case (, topHashtag) => topHashtag must beEqualAsSetTo(peakHashtags) } on numBatches
isPeak ==> eventuallyTop
} during numBatches * 3
forAllDStream( gen)( TweetOps.getTopHashtag(batchInterval, windowSize)(_))( alwaysAPeakImpliesEventuallyTop) } *
The consume operator is also useful to define other types of properties like the following, that only uses consume and next as temporal operators, but that is able to express the basic condition for counting correctly and on time. It states that for any number of repetitions less or equal to the counting window size, and for any random word prefix, if we repeat the word prefix times then after the instants we will have a count of at least (to account for hashtags randomly generated twice) for all the hashtags in the first batch. Here we use def next[T](times: Int)(phi: Formula[T]) that returns the result of applying next times times on the given formula.
Example D.14**.**
def forallNumRepetitionsLaterCountNumRepetitions = { type U = (RDD[Status], RDD[(String, Int)]) val windowSize = 5 val (numBatches, maxHashtagLength) = (windowSize * 6, 8)
// numRepetitions should be <= windowSize, as in the worst case each // hashtag is generated once per batch before being repeated using // Prop.forAllNoShrink because sscheck currently does not support shrinking Prop.forAllNoShrink(Gen.choose(1, windowSize)) { numRepetitions => val tweets = BatchGen.ofNtoM(5, 10, tweetWithHashtagsOfMaxLen(maxHashtagLength)) val gen = for { tweets <- BatchGen.always(tweets, numBatches) // using tweets as a constant generator, to repeat each generated // stream numRepetitions times delayedTweets <- PDStreamGen.always(tweets, numRepetitions) } yield delayedTweets
val laterCountNumRepetitions = nextF[U] { case (statuses, _) =>
val hashtagsInFirstBatch = getExpectedHashtagsForStatuses(statuses)
// -2 because we have already consumed 1 batch in the outer nextF, and
// we will consume 1 batch in the internal now
next(max(numRepetitions-2, 0))(now { case (_, counts) =>
val countsForHashtagsInFirstBatch =
hashtagsInFirstBatch
.map((_, ()))
.join(counts)
.map{case (hashtag, (_, count)) => count}
countsForHashtagsInFirstBatch should foreachRecord { _ >= numRepetitions }
})
}
forAllDStream(
gen)(
TweetOps.countHashtags(batchInterval, windowSize)(_))(
laterCountNumRepetitions)
} } *
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1Akidau et al., 2013 Akidau, T., Balikov, A., Bekiroğlu, K., Chernyak, S., Haberman, J., Lax, R., Mc Veety, S., Mills, D., Nordstrom, P., and Whittle, S. (2013). Mill Wheel: fault-tolerant stream processing at internet scale. Proceedings of the VLDB Endowment , 6(11):1033–1044.
- 2Akidau et al., 2015 Akidau, T., Bradshaw, R., Chambers, C., Chernyak, S., Fernández-Moctezuma, R. J., Lax, R., Mc Veety, S., Mills, D., Perry, F., Schmidt, E., et al. (2015). The dataflow model: a practical approach to balancing correctness, latency, and cost in massive-scale, unbounded, out-of-order data processing. Proceedings of the VLDB Endowment , 8(12):1792–1803.
- 3Alur and Henzinger, 1994 Alur, R. and Henzinger, T. A. (1994). A really temporal logic. J. ACM , 41(1):181–204.
- 4Apache Spark Team, 2016 Apache Spark Team (2016). Spark programming guide. https://spark.apache.org/docs/latest/programming-guide.html .
- 5Barringer and Havelund, 2011 Barringer, H. and Havelund, K. (2011). Tracecontract: A scala DSL for trace analysis. In Butler, M. J. and Schulte, W., editors, Proceedings of the 17th International Symposium on Formal Methods, FM 2011 , volume 6664 of Lecture Notes in Computer Science , pages 57–72. Springer.
- 6Bauer et al., 2006 Bauer, A., Leucker, M., and Schallhart, C. (2006). Monitoring of real-time properties. In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science , pages 260–272. Springer.
- 7Beck, 2003 Beck, K. (2003). Test-driven development: by example . Addison-Wesley Professional.
- 8Blackburn et al., 2006 Blackburn, P., van Benthem, J., and Wolter, F., editors (2006). Handbook of Modal Logic . Elsevier.