Schema-guided testing of message-oriented systems

Schema-guided Testing of Message-Oriented Systems André Santos1,2 a, Alcino Cunha2 b and Nuno Macedo3 c 1VORTEX CoLab, Vila Nova de Gaia, Portugal 2High-Assurance Software Laboratory, INESC TEC and University of Minho, Braga, Portugal 3High-Assurance Software Laboratory, INESC TEC and University of Porto, Porto, Portugal [email protected], [email protected], [email protected] Keywords: Software Testing, Formal Specifications, Specification-based Testing, Property-based Testing. Abstract: Effective testing of message-oriented software requires describing the expected behaviour of the system and the causality relations between messages. This is often achieved with formal specifications based on temporal logics that require both first-order and metric temporal constructs – to specify constraints over data and real time. This paper proposes a technique to automatically generate tests for metric first-order temporal specifications that match well-understood specification patterns. Our approach takes in properties in a high-level specification language and identifies test schemas (strategies) that are likely to falsify the property. Schemas correspond to abstract classes of execution traces, that can be refined by introducing assumptions about the system. At the low level, concrete traces are successively produced for each schema using property-based testing principles. We instantiate this approach for a popular robotic middleware, ROS, and evaluate it on two systems, showing that schema-based test generation is effective for message-oriented software. 1 INTRODUCTION As the complexity of software systems increases, so does the necessity to properly verify that safe behaviour will be observed. Testing is an essential, and often the only, strategy deployed for that purpose, but the complexity of modern systems renders the manual encoding of test cases impractical. As a consequence, several automated approaches to test generation have emerged, such as model-based (MBT), property-based (PBT), and specification-based testing (SBT). These challenges are exacerbated when targeting distributed systems where components communicate asynchronously through message-passing, such as those complying to the OMG’s DDS standard (OMG, 2015). These systems are typically heterogeneous and built from third-party components, so system-level testing should act at the message-passing level, treating components as black-boxes. In this context, the behaviour to be analysed is of a dynamic nature, and testing procedures must take into consideration full traces of messages as inputs and outputs. This limits the feasibility of using unit tests beyond specific corahttps://orcid.org/0000-0002-1985-8264 bhttps://orcid.org/0000-0002-2714-8027 chttps://orcid.org/0000-0002-4817-948X ner cases. PBT approaches are also ill-suited since they either focus on execution safety properties (such as null references or buffer overflows) or require the expected behaviour to be specified operationally. MBT approaches require modelling the system behaviour, which is often infeasible in systems of this nature. SBT approaches can be used to tackle these issues. Here, the user is only expected to provide a single artefact, a high-level declarative specification of the expected behaviour of the system. In a dynamic context, these take the shape of temporal specifications, allowing the encoding of functional safety properties. Relevant trace inputs are automatically generated by inspecting the specifications, while validity is automatically tested by evaluating the specification against the output traces. However, previously proposed techniques of this nature are still affected by some issues. First, they are often based on logics with abstract time, such as linear temporal logic (LTL) (Tan et al., 2004; Michlmayr et al., 2006; Arcaini et al., 2013; Bloem et al., 2019; Narizzano et al., 2020), but most systems are expected to be tested for some timing constraints. Moreover, they often fail to provide a proper high-level interface that spares the developer from having to understand the underlying formalisms. Lastly, due to the extent of the search-space for timed trace test cases, such techniques must provide some kind Figure 1: Overview of the proposed approach. of mechanisms to guide the input generation. Some techniques have been proposed in PBT, such as targetoriented (Löscher and Sagonas, 2017) and coverageguided (Padhye et al., 2019) approaches, but they are ill-suited for heterogeneous and distributed systems. In this paper we propose a novel SBT approach, depicted in Figure 1, based on trace schemas for messageoriented systems whose expected behaviour is specified in a high-level specification language. The users are only required to specify the architecture and the expected behaviour of the system under test (SUT), from which the input generator and the property monitors are derived. The language is based on well-known specification patterns (Dwyer et al., 1999), so that knowledge about the underlying formalisms or the implementation details of the SUT is not required. A trace schema is a sequence of message-passing conditions that are expanded by the trace generators into concrete message traces, which are automatically derived from the specified properties based on the used pattern. To restrict the search-space of the trace generator, the developer can specify additional properties over the communication channels using the same specification language, which the testing procedure uses to refine the schemas derived from the specification. We evaluated our technique by implementing it over the most popular robotic middleware, the Robot Operating System (ROS) (Quigley et al., 2009). ROS provides a communication layer that allows robotic systems to be built from components communicating through a publisher-subscriber paradigm. This instantiation comprised the implementation of the specification language for ROS messages, a test generator for trace schemas, and the deployment of runtime monitors. It was integrated into HAROS (Santos et al., 2016; Santos et al., 2021), a framework for the development of high-assurance ROS software, which automates several tasks required for analysis and reporting. Evaluation shows that schemas automatically derived from specifications are effective in finding bugs related to message interleaving, and that providing additional assumptions further improves the results. The rest of this paper is organized as follows. Section 2 presents an overview of the proposed approach. Section 3 presents the proposed property specificaFigure 2: ROS system with open subscribers. tion language, followed by the formalization of trace schemas, their derivation and associated trace generator in Section 4. Section 5 and Section 6 present the instantiation of the approach for ROS and the evaluation results. Section 7 presents and discusses related work. Lastly, Section 8 concludes the paper. 2 SCHEMA-GUIDED TESTING To provide an overview of the proposed framework, consider its instantiation for ROS (Section 5), used for evaluation in Section 6. ROS is a collection of libraries, tools and components for the development of robotic applications. In ROS, software is organised in packages, the basic build and release units. A large number of packages is open source and over 4 000 are indexed in official collections, called distributions. At runtime, a ROS system is typically distributed, with various independent nodes consuming, processing and producing data. Nodes often communicate via structured messages sent through topics – typed message-passing channels implementing a publisher-subscriber model. Consider the system in Figure 2 as an example. It contains two nodes: /planner , which subscribes /position messages and publishes /plan messages, and /control , which given /plan and /laser , publishes velocity messages at /vel with some degree of safety. Let us say that we want to check whether a simple safety property holds in this system: that when the laser detects an obstacle closer than 40cm, a zero velocity message will be published within a certain threshold (say, 500ms), so that the robot avoids hitting the obstacle. Using the proposed specification language (Section 3), this could be easily specified as 1globally:/laser { dist < 40} causes 2/ vel { linear .x = 0} within 500 ms How can such a property be tested? Since nodes are considered to be black boxes, one must act at the message-passing level, publishing and listening to messages being passed by the middleware. However, not all available channels should be exercised by the testing procedure: we must identify the channels that represent the inputs of the system under test. An open subscribed channel is any channel that the system subscribes but for which there are no publishers. They are the intended interfaces to integrate the system with the environment, since there is no other purpose for subscribers that lack their respective publishers. In the example, /position and /laser are open subscriptions. Even though closed channels are technically usable by external components, we treat them as internal communication channels and do not tamper with them by publishing additional messages, because the system is likely not designed to expect the additional publishers. To test specific portions of the system, our approach also allows the testing of a projection of the architecture. For instance, in the example the user could wish to focus on testing the /control node, in which case /plan would become an open subscribed channel and /position rendered irrelevant. Once the input channels are selected, the testing procedure must decide the channels, order and delay between the messages that will be published. Our approach is based on PBT and SBT principles. We use the former to automatically explore the input space and test the SUT with a variety of valid inputs. We use the latter to convert formal properties into specialized test strategies, in order to nudge the input generators in a direction that is more likely to reveal counterexamples. We call these test strategies input trace schemas, an abstraction for a certain category of input traces. They describe a general sequence of events using abstract messages and durations, annotated with their respective constraints. For instance, for the property just presented, only input traces that publish /laser messages with values below 40cm are relevant, otherwise the property will never be falsified. This could be specified with the following simple trace schema. 1forbid /laser { dist < 40} 2+0..: publish /laser { dist < 40} Our system derives automatically an input trace schema for each property (Section 4.2). The notation is simple: a schema is interpreted line by line, each statement representing general constraints over channels ( forbid ) or mandatory events of interest ( publish ). The syntax follows the one used in our specification language, i.e., it expects a channel name, followed by predicates over the message’s fields. The forbid statement imposes restrictions over the (zero or more) random messages an input trace is allowed to instantiate within a segment of the trace, applied from the instant immediately following the previous mandatory event (or the start of the trace) until (but not including) the next mandatory event (or until the end of the trace). In the example, the first line states that there should be no /laser detecting obstacles until it is forced to be published later in the trace. There is no restriction on /position , so any number of /position messages – regardless of their content – and /laser messages with value ≥40 may be published in this interval. A publish statement is composed of an interval and of constraints over a channel. It denotes a single mandatory message whose timestamp must be contained in the specified interval, relative to the previous event. In the example the derived schema does not impose any time interval, so the interval is left unbounded (0 or more milliseconds after the initial instant). After forced publication no further constraints are imposed, so any arbitrary /position and /laser messages may be published until the end of the trace. An input trace is a finite sequence of messages with concrete values in data fields, annotated with timestamps generated from the schemas, that the test driver should replay on open subscribed channels to stimulate the SUT. Input traces are, thus, instances of a schema. Note that this is distinct from the observed trace, the actual sequence of events that makes a particular run of the SUT, including messages published by the nodes under test. For instance, the following input trace is an instance of the previous schema. 1@40ms /laser { dist : 50.0} 2@50ms /position {x: 0.0 , y: 0.0} 3@60ms /laser { dist : 30.0} 4@70ms /position {x: 2.5 , y: 0.5} 5@80ms /laser { dist : -20.0} 6@90ms /position {x: 3.0 , y: 1.0} We can see how this trace is an instance of the previous schema: a /laser message with value <40 is published after 60 milliseconds and there is no such message before it. Besides the restrictions imposed by the schema statements, the trace generator will generate arbitrary messages to build a complete input trace. However, we should also notice that it is allowing messages that are invalid in a real environment: sensors do not publish negative /laser messages. To address this, the user can introduce additional assumptions following the same specification language. For the example, this could specified as: 1globally:no /laser { dist < 0} Properties that only refer to open subscriptions, called axioms, are considered global constraints over the input trace schemas and are used to refine them. They are used to ignore tests whose actual input traces are nonconforming. Our example schema, now refined, would be: 1forbid /laser { dist < 40} 2+0..: publish /laser {0 <= dist < 40} 3forbid /laser { dist < 0} The previously shown (invalid) input trace would no longer be generated from this schema. Bugs often occur from specific message combinations, so the tighter the allowed message values, the higher the probability relevant input traces are generated. For instance, bugs may be triggered by the rapid publication of /laser messages near the 40cm boundary value. By being able to generate any positive float it would still be very unlikely to generate such a trace. Guided by specific knowledge of the SUT, the developer may introduce additional, finer axioms to force the trace generator to focus on particular classes of input traces. In our example, the developer could have imposed a very specific of range of /laser values, knowing that – in principle – the system would not behave differently for other values: 1globally:no /laser { dist < 0 or dist > 100} Such axioms should be used with care: they rule out test cases that are theoretically valid, even though they might be unexpected for a particular application. 3 SPECIFICATION LANGUAGE The property specification language we propose is based solely on the messages that components exchange with one another in a message-oriented system. The SUT is treated as a black box, as is custom in SBT. The language is built on top of the well-known property specification patterns proposed by (Dwyer et al., 1999). We focus on the Absence (a certain type of message, a behaviour, must not be observed), Existence (a certain type of message, a behaviour, must be observed at least once), Precedence (observing a certain type of message, a behaviour, implies that another type of message, a stimulus, must have been observed prior) and Response (observing a certain type of message, a stimulus, implies that another type of message, abehaviour, must be observed in the future) patterns. We also add a new Prevention pattern (a certain type of message, a stimulus, implies that another type of message, a behaviour, must not be observed in the future). In addition, properties specify a scope, delimiting the times during which the pattern must hold. A scope may be Global (the pattern should always hold), After (the pattern should hold indefinitely, after a certain message, the activator, is observed for the first time), Until (the pattern should hold up to the point when a certain message, the terminator, is observed for the first time), or After-until (the pattern should hold after a certain message, the activator, is observed, up to the point when another message, the terminator, is observed), the last being possibly re-entrant. 3.1 Syntax The following grammar defines the language’s syntax. hpropertyi::= hscopei‘:’hpatterni hscopei::= ‘globally’ | hafter-untili|huntili hafter-untili::= ‘after’heventi[huntili] huntili::= ‘until’heventi hpatterni::= ‘no’heventi[htime-boundi] | ‘some’heventi[htime-boundi] |heventi‘requires’heventi[htime-boundi] |heventi‘causes’heventi[htime-boundi] |heventi‘forbids’heventi[htime-boundi] htime-boundi::= ‘within’htimei htimei::= hnatural-zeroi‘ms’ heventi::= hros-namei[haliasi] [hpredicatei] haliasi::= ‘as’hidi hpredicatei::= ‘{’hconditioni‘}’ hconditioni::= hvaluei hbinary-rel-operatori hvaluei | ‘(’hconditioni‘)’ | ‘not’hconditioni | ‘forall’hidi‘in’hmsg-fieldi‘:’hconditioni |hconditioni hbinary-connectivei hconditioni hbinary-rel-operatori::= ‘=’|‘<’ hbinary-connectivei::= ‘or’|‘and’ hvaluei::= hbooleani|hnumeric-expri|hstringi hvariablei::= ‘$’hidi hmsg-fieldi::= hfield-namei{‘.’hfield-namei} |halias-ref i‘.’hfield-namei{‘.’hfield-namei} halias-ref i::= ‘@’ (hnatural-zeroi|hidi) hfield-namei::= hidi[hindexi] hindexi::= ‘[’ (hnatural-zeroi|hvariablei) ‘]’ We present only a small set of logical connectives and relational operators, but we can assume common syntactic sugar such as the relational operator ‘>’. The forall quantifier provides a basic means of iterating over all valid indices of array fields. The syntax ‘ forall iin array ’ is roughly equivalent to the Python ‘ for iin range(len(array)) ’. The grammar also captures references to quantified variables ( ‘$var’ ) and to message fields. Message fields can be: (i) simple identifiers ( ‘field’ ) to refer to a field of the message; (ii) multiple identifiers separated by dots ( ‘parent.child’ ) to refer to nested fields of composed messages; or (iii) indexed (‘parent.array[1]’) to access array positions. Every message in a property has an implicit associated index, to enable cross-references with ‘@’ . Messages are numbered, starting at 1 with the activator event, if any, and then following up with the pattern events. Since numeric references can become confusing, we introduce event aliases to allow humanreadable names instead. For instance, a predicate can refer to fields of an activator ‘ /bumper as Bumper ’ as ‘@Bumper.field’ rather than ‘@1.field’ . Crossreferences are only possible if the referenced message (unambiguously) happens before the current message; e.g., pattern events can refer to the scope activator. 3.2 Semantics The original specification patterns (Dwyer et al., 1999) are intended for propositional temporal logics, such as LTL, but our specification language adds first-order predicates over data and real-time constraints. Thus, we use Metric First-Order Temporal Logic (Chomicki, 1995) (MFOTL), whose syntax and semantics are similar to other commonplace logics, such as LTL, except that temporal operators in MFOTL can be annotated with metric time intervals. A temporal formula is only satisfied if it is satisfied within the bounds given by the time interval of the temporal operator, which is always relative to a timestamp. Let ∆ be the set of non-empty intervals over N0 , such that an interval δ∈∆ is written [δ1,δ2) with δ1∈ N0 , δ2∈N∪{∞} , and δ1<δ2 . A signature S is a tuple (C,P,a) , where C is a finite set of constant symbols, P is a finite set of predicates disjoint from C , and the function a:P7→ N provides the arity of each predicate. Also, let V denote a countably infinite set of variables, where we assume that V∩(C∪P) = / 0. Definition 1. The formulae over S are inductively defined: (i) For x,y∈V∪C , x=y is a formula. (ii) For p∈P , n=a(p) and x1,...,xn∈V∪C , p(x1,...,xn) is a formula. (iii) For x∈V , if ϕ and ψ are formulae, then (¬ϕ) , (ϕ∧ψ) and (∃x:ϕ) are formulae. (iv) For δ∈∆ , if ϕ and ψ are formulae, then (t δϕ) , (d δϕ) , (ϕSδψ), and (ϕUδψ)are formulae. Here t is read previous, d next, S since and U until. Other common operators can be defined in terms of the core set, namely  (historically),  (globally),  (once), ♦ (finally), W (weak-until), B (back-to) and Z(weak-previous). Afirst-order structure D over S consists of a domain |D| 6=/ 0 and interpretations cD∈ |D| and pD⊆ |D|a(p) , for each c∈C and p∈P . A temporal first-order structure over S is a pair (D,τ) , where D= (D0,D1, . . .) is a sequence of structures over S and τ= (τ0,τ1, . . .) is a sequence of natural numbers (timestamps), where τ is monotonically increasing ( ∀i≥0 : τi≤τi+1 ) and makes progress ( ∃j>i:τj> τi ); D has constant domains ( ∀i≥0 : |Di|=|Di+1| ); and each constant symbol c∈C has a rigid interpretation ( ∀i≥0 : cDi=cDi+1 ). A valuation is a mapping v:V7→ |D| . We abuse notation by applying valuations also to constant symbols c∈C , with v(c) = cD . Additionally, we denote v[x7→ d] as the valuation where (D,τ,v,i)x=yiff v(x) = v(y) (D,τ,v,i)x<yiff v(x)<v(y) (D,τ,v,i)p(x1,...,xa(p)) iff (v(x1),...,v(xa(p))) ∈pDi (D,τ,v,i)(¬ϕ)iff (D,τ,v,i)2ϕ (D,τ,v,i)(ϕ∧ψ)iff (D,τ,v,i)ϕ and (D,τ,v,i)ψ (D,τ,v,i)(∃x:ϕ)iff (D,τ,v[x7→ d],i)ϕ, for some d∈ |D| (D,τ,v,i)(t δϕ)iff i>0,τi−τi−1∈δ and (D,τ,v,i−1)ϕ (D,τ,v,i)(d δϕ)iff τi+1−τi∈δ and (D,τ,v,i+1)ϕ (D,τ,v,i)(ϕSδψ)iff (D,τ,v,j)ψ and (D,τ,v,k)ϕ for some j≤i,τi−τj∈δand all k∈[j+1,i] (D,τ,v,i)(ϕUδψ)iff (D,τ,v,j)ψ and (D,τ,v,k)ϕ for some j≥i,τj−τi∈δand all k∈[i,j) Figure 3: Metric First-Order Temporal Logic semantics. every mapping is unaltered, when compared to v , save for x∈V, which should map to d∈ |D|. Definition 2. Let (D,τ) be a temporal structure over S , with D= (D0,D1, . . .) and τ= (τ0,τ1, . . .) , ϕ and ψ formulae over S , v a valuation, and i∈N0 . The temporal structure satisfies a formula ϕ , written (D,τ)ϕ , if and only if (D,τ,v,0)ϕ, as shown in Figure 3. In the interpretation of the proposed language, the first-order structures Di over S consist of a domain |D| containing all numbers, Boolean values, strings, and messages (consisting of a unique identifier). Also, for all message channels /ch there is a predicate ch ∈P such that ch(m) is true if and only if a message m can be observed on /ch . The relation of messages to data fields is given by predicates field(m,x)∈P such that field(m,x) holds if and only if a message m carries the value (or message) x in a field named field . To simplify quantification over the indices of an array, we redefine field(m,k) to hold for all indices of the array rather than values. That is, for k∈N0 , field(m,k) holds if k is an index of an array named field . In addition, we define a predicate fieldk(m,x) that holds if the field field[k] carries the value x , i.e., if field(m,k) holds and the array contains x at index k . We address composed messages, f.g , with the composition of predicates fand g, such that g◦f(m,x)≡(∃m0:f(m,m0)∧g(m0,x)) Definition 3. Let (D,τ) be a temporal structure over S , with D= (D0,D1, . . .) and τ= (τ0,τ1, . . .) . Let v be a valuation, i∈N0 and Φ a property over S . We define JΦK , the interpretation of Φ , as a function that translates Φ to its equivalent MFOTL formula. Thus, Scopes Jglobally:ΨK,JΨK/ 0 ⊥ Juntil q:ΨK,JΨK/ 0 q Jafter p:ΨK, (∀x:(JpKx∧Z((@y:JpKy))) →JΨKx ⊥) Jafter puntil q:ΨK, (∀x:(JpKx∧(@y:JqKy)∧Z((@y:JpKy)B(∃y:JqKy))) →JΨKx q) Patterns Jno bwithin tmsKx q,(@y:JbKx,y)W[0,t)(∃y:JqKy) Jsome bwithin tmsKx q,(@y:JqKy)U[0,t)((∃y:JbKx,y)∧(@y:JqKy)) Jacauses bwithin tmsKx q,(∀y:JaKx,y→Jsome bwithin tmsKx,y q)W(∃y:JqKy) Jaforbids bwithin tmsKx q,(∀y:JaKx,y→Jno bwithin tmsKx,y q)W(∃y:JqKy) Jbrequires awithin tmsKx q,∀y:(¬JbKx,yW(∃z:JaKx,y,z∨JqKz)) ∧((JbKx,y→[0,t)(∃z:JaKx,y,z)) W(∃z:JqKz)) Events J/ch Kx,J/ch {>}Kx J/ch {ϕ}Kx1,...,xn,ch(xn)∧JϕKx1,...,xn / 0 Predicates J>Kx γ,> J⊥Kx γ,⊥ J(ϕ)Kx γ,(JϕKx γ) Jnot ϕKx γ,¬JϕKx γ Jϕand ψKx γ,JϕKx γ∧JψKx γ Jϕor ψKx γ,JϕKx γ∨JψKx γ Ja∼bKx γ,∃y,z:yJaKx γ∧zJbKx γ∧y∼z for ∼∈ {=, <, ≤, >, ≥} Jforallvar in f:ϕKx γ,∀y:yJfKx γ→JϕKx γ[var7→y] Jforallvar in @k.f:ϕKx γ,∀y:[email protected] γ→JϕKx γ[var7→y] Values and Expressions yJcKx γ,y=cfor cconstant yJ$varKx γ,y=γ(var) yJfKx1,...,xn γ,JfKγ(xn,y) [email protected],...,xn γ,JfKγ(xk,y)if 1 ≤k≤n yJ(a)Kx γ,(yJaKx γ) yJa⊕bKx γ,∃z,w:zJaKx γ∧wJbKx γ∧y= (z⊕w) for ⊕ ∈ {+,−,×,÷} Field Predicates JfieldKγ,field Jfield[k]Kγ,fieldk Jfield[$var]Kγ,fieldγ(var) Jf1.f2Kγ,Jf2Kγ◦Jf1Kγ Figure 4: Specification language semantics. we define (D,τ,v,i)Φ as (D,τ,v,i)JΦK , and JΦK is defined as shown in Figure 4. To shorten some formulae and improve readability, we assume that all interpreted properties Φ are typechecked prior to their semantic interpretation JΦK. Scopes. globally and until start, by definition, at the initial instant of the trace and, thus, require the inner formula to hold at that instant. On the other hand, after and after-until start when an activator is been observed – hence the (activator →Ψ) type of formula. The translation of a pattern Ψ is denoted by JΨKx q and is passed a vector of quantified messages x=x1,...,xn – initially the activator, if any – and the terminator event q, if any. Patterns. We present only the timed variants of each pattern, since untimed variants are particular cases where δ=∞ . Unary patterns, no and some , are already close to a MFOTL formula, requiring the translation of event predicates, denoted by JaKx for an event a given quantified messages x . The binary patterns causes and forbids are translated via composition with the unary ones. The most complex pattern, requires , is defined with two conjuncts: behaviour b should not happen before its stimulus a or the scope terminator q ; and if b happens before q , then a must have happened within the previous δtime instants. Predicates. The translation of a predicate ϕ is mostly direct to logic values or connectives, and is denoted by JϕKx γ for quantified messages x and a mapping γ for syntactic replacements arising from quantifications (given a variable name as written in the property, its occurrences are replaced with a quantified variable in |D| ). When translating an expression a , yJaKx γ denotes a predicate that tests whether the value of the variable yis one of the values for the expression a. Values and Expressions. Message fields translate to their homonymous predicates, and field composition to predicate composition, as previously explained. References to other messages, e.g., @k.f , convert the human-readable aliases to the message index, referring to the k -th message of the superscript vector, xk , rather than the current message, xn . Lastly, arithmetic expressions bind quantified variables to domain values. 4 TRACE SCHEMAS This section formalizes the core notion of the proposed approach, that of input trace schemas. Then it shows how they integrate the approach by presenting how schemas are derived from patterns, and then concrete input traces generated from schemas. 4.1 Formalization A trace schema is a sequence of restrictions on a sequence of messages, forcing messages with certain properties to be published and forbidding certain other kinds of messages between such publications. Definition 4. An input trace schema Γ is a set of formulae over a signature S , written as a sequence of statements according to the following grammar. hschemai::= hstatementi* hstatementi::= ‘forbid’heventi |hboundsi‘:’ ‘publish’heventi hboundsi::= ‘+’hnatural-zeroi‘..’ [hnatural-zeroi] To convert schemas into MFOTL formulae, let us start by defining an atomic variable e0 for the initial instant of the trace and atomic variables ei for each of the kpublish events in a schema. Each atomic variable ei is true only at the instant when the ith publish event happens. Given statements of the form +mi..ni:publish /ch {ϕi} for all i∈N , we have that: (ei→d (¬ei)) , i.e., once ei happens, it will not happen again; and also (ei→(∃x:ch(x)∧ϕi)) , i.e., at the instant ei happens, there is a message on /ch such that ϕi . Then, we must schedule all mandatory events. For all i≤k we must observe (ei−1→♦[mi,ni)ei) . Then, the constraints given by forbid statements must be considered. Given a statement forbid /ch {ϕ} placed between events ei and ei+1 , it follows that: (ei→ d ((¬∃x:ch(x)∧ϕ)Wei+1)) . The d and W operators ensure that the constraints do not apply at the logical instants ei and ei+1 . If the schema ends with a forbid statement, the W operator will impose the constraints indefinitely, as ek+1≡ ⊥. hglobally:Ψi,hΨi huntil q:Ψi,hΨi hafter p:Ψi hafter puntil q:Ψi, forbid p +0..: publish p hΨi hno bwithin tmsi,ε hsome bwithin tmsi,ε hbrequires awithin tmsi,ε hacauses bwithin tmsi haforbids bwithin tmsi,forbid a +0..: publish a Figure 5: Translation from specifications to schemas. 4.2 Generating Input Traces From Patterns to Schemas. For each pattern of the property language we specify how a base schema is derived. These schemas represent a set of traces with minimal constraints such that every counterexample to the property is necessarily in them (i.e., they are complete). These schemas essentially take into consideration the activators and stimuli of the properties, without which no counterexample can be found. This translation between properties and base schemas is shown in Figure 5, and is mostly selfexplanatory, denoted by hΦi for a property Φ . For example, consider the base schema for acauses b : a stimulus is forced to be published, otherwise the property cannot be falsified. Refining Schemas. Axioms play an important role in establishing valid data and valid trace structure. In some cases, they can be embedded into the base schemas, so that generated traces are mostly correct by construction. The refinement of a schema Γ by an axiom Φ is denoted by bΓcΦ . We support refinements for two types of properties, specifically: 1globally:no /c {ϕ} 2globally:/c forbids /c within tms If an axiom Φ is of the first shape, constraints are added to the data a message can carry. For /c 6=/d:     Γ1 δ:publish /d {ψ} Γ2    Φ , Γ1 forbid /c {ϕ} δ:publish /d {ψ} forbid /c {ϕ} Γ2 Publish statements on the same channel /c also have their predicates restricted:     Γ1 δ:publish /c {ψ} Γ2    Φ , Γ1 forbid /c {ϕ} δ:publish /c {ψand not φ} forbid /c {ϕ} Γ2 Axioms Φ of the second shape impose additional temporal constraints. For two consecutive publish statements on channel /c , we shift the lower-bound of the second interval, if t<n:          Γ1 δ:publish /c {ψ} Γ2 m..n: publish /c {ψ0} Γ3         Φ , Γ1 δ:publish /c {ψ} Γ2 t..n: publish /c {ψ0} Γ3 If t≥n, the specification is a contradiction. From Schemas to Traces. The last step is to generate traces that conform to the schemas. Definition 5. Let S be a signature, v a valuation and Γ an input trace schema over S . A temporal first-order structure (D,τ) over S is said to be an instance of Γ if and only if, for all ϕ∈Γ , it is true that (D,τ,v,0)ϕ . This definition determines whether a temporal firstorder structure (an infinite trace) is an instance of a schema, but we can only generate finite input traces. Thus, we need to validate finite traces against schemas. Definition 6. An input trace of length k is a k -prefix of a temporal structure over S, for some k ∈N0. Definition 7. Let S be a signature, v be a valuation and Γ be an input trace schema over S . Let k∈N0 and (D[0,k),τ[0,k)) be a k -prefix of a temporal structure over S . The k -prefix (D[0,k),τ[0,k)) is said to be an instance of Γ if and only if, for all (D0,τ0) temporal structures over S , (D[0,k),τ[0,k)) is a k -prefix of (D0,τ0) , and it is true that (D0,τ0,v,0)ϕ, for all ϕ∈Γ. The previous definition, in essence, states that, for a finite trace to be an instance of a schema, any of its possible (infinite) extensions must also be instances of the same schema, as is standard in bounded temporal semantics. With this, we are now equipped to produce traces that comply with a set of constraints. The algorithm for trace generation is simple. An initial pass allocates all timestamps and messages associated with publish events. A second pass iterates over all intervals before and after the mandatory events, and, evaluating the applicable forbid statements for each interval, builds a set of all usable channels. From this set, it then produces a random number of messages, and intersperses the messages randomly along the interval. The result is a sorted list of (timestamp, channel, message) tuples; a finite trace. 5 TOOL SUPPORT FOR ROS Given a system specification, composed of behavioural properties following the syntax shown in Section 3 and a description of the inputs and outputs of the SUT, the proposed schema-based testing approach automatically generates property-based tests that try to falsify the specification. Our implementation is compositional, tackling one problem at a time, namely: property parsing 1 , runtime monitor generation 2 and data generation for trace schemas 3 . To obtain the necessary architecture model of the SUT, we implemented the test generator as a plug-in for the HAROS framework, which is already capable of extracting models from source code (Santos et al., 2019). This eases workflow automation, from model extraction to test generation, execution and reporting. From a high-level perspective, the tool starts by filtering the provided properties. Each property is assigned one category of axiom,testable or non-testable. Although in theory all properties can be tested, our current implementation for ROS only considers a property testable if we have complete control of its scope and stimulus events. That is, its scope activator, scope terminator and stimulus event (if applicable) must be open subscribed topics (inputs), while its behaviour event must be a published topic (output). Furthermore, predicates over input messages must not contain arithmetic or quantified expressions. These limitations help ensure that tests are feasible and reproducible. Predicates over input messages are embedded into the message generators on a best-effort basis, which still requires a subsequent runtime validation step. Quantifiers and arithmetic expressions make constraints over data significantly more complex, meaning that more input candidates have to generated until one is valid. Limiting outputs only to behaviour events grants the test driver control over the pace of the test; the input trace schema dictates when scopes should start and when behaviours should be triggered. For each testable property, the tool identifies the property’s pattern and produces the corresponding base schemas, as presented in Section 4. Axioms are considered next, if applicable, to refine all starting schemas. Refinement is a best-effort attempt at generating correct data by construction. Again, it does not capture all given constraints and must be validated at runtime. Following the schema generation and refinement steps, the tool applies meta-programming Jinja 4 templates for all properties, to produce source code blocks 1https://github.com/git-afsantos/hpl-specs 2https://github.com/git-afsantos/hpl-rv-gen 3https://github.com/git-afsantos/haros-plugin-pbt-gen 4https://palletsprojects.com/p/jinja/ for the runtime monitors, trace generators and the overall test case structure. Each property pattern has its corresponding code template, meaning that we can produce optimized monitors and data generators for our limited catalogue of options. The trace generators are implemented as data generators for Hypothesis (MacIver et al., 2019), a well-established PBT library. At the end, all pieces are weaved into a single test script, which is responsible for successively producing traces using Hypothesis, according to a given schema, launching the SUT using tools of the ROS infrastructure, deploying runtime monitors, replaying the input trace and then observing the results. The test script is itself a ROS node, allowing runtime monitors to subscribe directly to all topics in the system, and, thus, observe messages as they are published. 6 EVALUATION The ROS-based implementation of the proposed schema-based approach for PBT has been applied to two concrete robotics applications. Note that the SUT are treated as black boxes with a publisher-subscriber interface, which makes the actual number of ROS nodes in the network irrelevant. Thus, for both case studies, we tested both individual nodes and fully integrated systems. We present now our case studies, the methodology behind our evaluation of the approach and, lastly, the observed results. 6.1 Case Studies The iClebo Kobuki 5 is our first test subject and one of the most iconic ROS robots. It is a low-cost, personal robot kit with open-source software whose main purpose is to provide an entry-level platform for roboticists to build applications with. Kobuki provides for an interesting case study, since its source code has been relatively well maintained and there is online documentation easily available – which makes it easier to understand the expected behaviour of the system. AgRob V16 6 is a modular robotic platform for hillside agriculture, adapted to steep slope vineyards. There are a few appealing factors in AgRob V16 as a case study, namely that it is an industrial robot, more complex than Kobuki, and that a large part of its software comes from integrated third-party packages. For this evaluation, and for both robots, we consider a configuration with three components: a Trajectory Controller node, that provides velocity commands 5http://kobuki.yujinrobot.com/about2/ 6http://agrob.inesctec.pt/ to the robot; a Safety Controller node, responsible for reacting to dangerous sensor readings; and a Supervisor node, that selects which commands to pass down to the hardware, based on the current safety state and the priority of the command source. 6.2 Methodology One of the characteristics of PBT is that it can only find discrepancies between implementation and specification (Hughes, 2016). Whether such discrepancies are an error in the system or in the specification is left to the user to decide. We have spent months studying the implementations of our target systems. Judging from the available documentation, we assume that they are relatively stable, with correct functional behaviour for the most part. This is a crucial assumption, as we write specifications mostly based on the actual (and expected) behaviour of the implementation. Given that PBT focuses on discrepancies, our evaluation process involves two types of testing: Positive Testing is the act of testing properties that we know to be true. The goal is to confirm that the tool does not introduce false positives – i.e., that it does not report an error if there is none to report. Negative Testing is the act of testing properties that we know to be false. The tool should be able to find at least one counterexample, athough this may require tuning how many examples are tested. We follow a systematic method to write specifications that include both true and false properties. We start by writing a catalogue of true properties and axioms for each system. Then, we apply specification mutation (Budd and Gopal, 1985; Ammann and Black, 1999; Black et al., 2000; Trab et al., 2012) to construct mutants (i.e., variants) of the initial set. Mutations are often small changes, such as changing a single operator or a variable. If the initial properties are as precise as we can write them, any small mutation should end up generating a false property. In practice, a validation step is still required to discard duplicates, trivial properties and equivalent mutants (mutants that are still true properties). Mutant validation is done manually, since it is an undecidable problem (Trab et al., 2012). The existing literature provides many operators to mutate specifications. We adapt and reuse those that are applicable to our specification language, such as: replacing an operand in an expression with another valid operand of the same type (e.g., 1with 0); negating an expression; replacing a logical operator (e.g., and with or ); replacing a relational operator (e.g., < with > ); removing a predicate from an event (e.g., /p {ϕ} becomes /p ); widening or shortening time constraints; replacing a message channel with another of