Bernhard K Aichernig
email: aichernig@ist.tugraz.at

Christian Burghard
email: burghard@ist.tugraz.at

Giving a Model-based Testing Language a Formal Semantics via Partial MAX-SAT

Keywords: Partial Moore Machines, Model Transformation, Consistency Checking, Formal Semantics, Frame Problem, Partial MAX-SAT

are widely used in modelbased testing to make the benefits of modeling available to test engineers while avoiding the problem of excessive learning effort. Complex DSLs benefit from a formal definition of their semantics for model processing as well as consistency checking. A formal semantics can be established by mapping the model domain to a well-known formalism. In this paper, we present an industrial use case which includes a mapping from domainspecific models to Moore Machines, based on a Partial MAX-SAT problem, encoding a predicative semantics for the model-to-model mapping. We show how Partial MAX-SAT solves the frame problem for a nontrivial DSL in which the non-effect on variables cannot be determined statically. We evaluated the performance of our model-transformation algorithm based on models from our industrial use case.

Introduction

Model-based Testing (MBT) has emerged as a widely adopted practice for the verification of industrial systems [START_REF] Peleska | Industrial-strength model-based testing -state of the art and current challenges[END_REF][START_REF] Sarma | Model-based testing in industry: a case study with two MBT tools[END_REF][START_REF] Utting | A taxonomy of model-based testing approaches[END_REF]. Following this development, the AVL List GmbH is testing its portfolio of automotive measurement devices via an MBT approach based on a textual domain-specific modeling language called MDML. In our previous work [START_REF] Burghard | Model-based Testing of Measurement Devices Using a Domainspecific Modelling Language[END_REF][START_REF] Burghard | Introducing MDML -a domain-specific modelling language for automotive measurement devices[END_REF], we designed the MDML language and modeling environment to provide our test engineers with an intuitively understandable model-based testing tool.

In a more recent development stage, we incorporated a model transformation from MDML models to Partial Moore Machines as the initial step of our modelbased testing toolchain. This transformation to a well-defined formalism provides MDML with an operational semantics. In the current version of our toolchain, it is largely based on a Partial MAX-SAT (PMSAT) problem, encoding predicative semantics. We chose a SAT-based implementation for our model transformation to cope with the potentially complex interplay of specialized language features. Before giving formal definitions, we briefly describe the syntax and semantics of MDML informally by the example model in Listing 1.1, which we will use for explanatory purposes throughout this work. Each MDML model starts with the definition of one or more state variables (Lines 1-2), including their name, value domain, initial value and a public or private classifier which indicates if the value of this variable is visible to an outside observer. This is followed by the definition of at least one input channel (Line 3), defining one or more input symbols through which the system can be controlled from the outside. The rest of the model consists of a hierarchy of rules, defining changes to state variables dependent on the current state variable values and the received input.

Beyond this basic structure, MDML incorporates several specialized language features which facilitate the modeling of specific behaviors or allow for a very concise model representation, e.g. last-transitions (Listing 1.1, Line 10), secondary actions (Line 13) or fallback blocks (Lines 14-16), all of which will be explained over the course of this work. These special features complicate the semantic evaluation of MDML models and, as our model-based testing toolchain evolved, the need for a more explicit model representation arose. A graph-based representation of the modeled state machine -e.g. in the form of a Moore Machine, would have a beneficial impact on further stages of our MBT toolchain, e.g test case generation [START_REF] Schlick | Fault-based generation of test cases from UMLmodels -approach and some experiences[END_REF], visualization [START_REF] Burghard | Visualizing multi-dimensional state spaces using selective abstraction[END_REF] and tracing. A Partial Moore Machine generated from the MDML model in Listing 1.1 can be seen in Figure 1.

The semantics of MDML state machine models as collections of state variables makes them subject to the frame problem -i.e. the problem of reasoning about system variables which are implicitly assumed to remain unchanged during an operation. The use of PMSAT is dictated by specific MDML language constructs -the aforementioned secondary actions -which significantly complicate a purely SAT-based solution of the frame problem. Lines 9 and 10 in Listing 1.1, for example, each specify a transition from Mode = Measure to Mode = Standby. However, the secondary action in Line 13 states that, whenever the Mode changes to Standby, the Timer must change to Off. This is a condition on the post-state of a transition, depending on another property of the post-state. In Figure 1, the result can be seen as the two transitions labeled STBY which are not loops. To the best of our knowledge, we are the first to provide a formal semantics to a domain-specific language via Partial MAX-SAT. Especially our treatment of the frame problem seems to be novel. We also contribute some experiences on the industrial use of a PMSAT-based model transformation. Defining an operational semantics for a front-end modeling language also has the effect of closely relating model transformation to consistency checking. We show how, through a small alteration, our model transformation setup can be used to uncover semantic inconsistencies within MDML models.

The rest of this paper is structured as follows: Section 2 introduces some necessary preliminaries, Section 3 outlines the syntax of the MDML language and Section 4 defines a formal semantics based on those syntax elements. Sections 5 and 6 explain how a model transformation and a consistency check can be implemented using this formal semantics. Section 7 presents the results of a runtime evaluation as well as our experience with the implementation. Finally, Section 8 discusses related work and Section 9 concludes the paper.

Preliminaries

Measurement Device Modeling Language

The Measurement Device Modeling Language (MDML) was developed in close cooperation with AVL's test engineers to efficiently model the firmware state machines of measurement devices. The taxonomy of Utting et al. [START_REF] Utting | A taxonomy of model-based testing approaches[END_REF] classifies MDML as a state-based notation, which means that it specifies a system as a collection of variables, representing a snapshot of the internal state of the system, plus some operations that modify those variables through pre-and postconditions. The syntax of MDML allows for many degrees of freedom in the encoding of a specific state machine behavior and each engineer is able to develop a modeling style that suits his or her individual needs. After the test models have been established, we automatically generate test cases from them using various mutation-based, structural and random coverage metrics [START_REF] Burghard | Model-based Testing of Measurement Devices Using a Domainspecific Modelling Language[END_REF]. These test cases are then converted to C# code and deployed to our test automation system. However, the aforementioned syntactic freedom of MDML is paid for by an increased difficulty in model processing. Although MDML is an effective input language, it would benefit from a more explicit model representation for all further uses in the model-based testing toolchain.

SAT, MAX-SAT and Partial MAX-SAT

A Boolean satisfiability (SAT) problem inquires, if a given Boolean formula can be fulfilled. While SAT problems are NP-complete, a series of algorithms and implementations ("SAT solvers") have been developed which can solve such problems in a (relatively) efficient and highly scalable manner [START_REF] Berre | The Sat4j library, release 2.2[END_REF]. When run on a Boolean formula f (b 1 , . . . , b n ) on the variables b 1 to b n , a SAT solver either returns a solution S : [1, n] → B, or the message UNSAT if f is not satisfiable. SAT solvers usually require formulas to be given in conjunctive normal form (CNF), i.e. as a conjunction of clauses, each consisting of a disjunctions of Boolean literals. However, any Boolean formula can be rewritten to CNF. The MAX-SAT problem is related to SAT. Here, the solver tries to maximize the number of satisfied clauses in a given CNF-formula. A further variant of the MAX-SAT problem is called Partial MAX-SAT (PMSAT) [START_REF] Fu | On solving the partial MAX-SAT problem[END_REF]. Here, the clauses are partitioned into a set of hard clauses (Φ H SAT ), which must be satisfied in any case, and a set of soft clauses (Φ S SAT ), of which a maximum number must be satisfied. Both MAX-SAT and PMSAT can be viewed as optimization problems with a cost function equal to the number of unfulfilled (soft) clauses.

Moore Machines

Definition 1 (Moore Machine). A Moore Machine is a tuple Q, q 0 , I, O, δ, λ with a finite set of states Q, an initial state q 0 ∈ Q, a set of input symbols I, a set of output symbols O, a transition function δ :

Q × I → Q and an output function λ : Q → O.
Definition 2 (Partial Moore Machine). A Partial Moore Machine (PMM) is a generalization of a Moore Machine with a partial function δ : Q × I Q.

Frame Problem

The frame problem is a rather old problem that was first formulated by Mc-Carthy and Hayes in a discussion of philosophical aspects of AI [START_REF] Mccarthy | Some philosophical problems from the standpoint of artificial intelligence[END_REF]. It is the problem of expressing the assumption in First-Order-Logic, that all system variables, which are not explicitly stated to be changed during an operation, remain unchanged. In classical specification methods, such as Z [START_REF] Spivey | Understanding Z : A specification language and its formal semantics[END_REF], VDM [START_REF] Jones | Systematic software development using VDM[END_REF] and B [START_REF] Abrial | The B-book -assigning programs to meanings[END_REF], the set of changed variables for a given operation is known at the time of specification. Such a partial variable assignment can easily be transformed into a total assignment by assigning all remaining variables their current value. In this way, the frame problem can be solved on a syntactic level. The Unified Theory of Programming (UTP) [START_REF] Aichernig | Refinement and test case generation in UTP[END_REF][START_REF] Hoare | Unifying theories of programming[END_REF] makes this transformation from partial to total assignments explicit. Separation Logic [21] leverages this a-priori knowledge in order to reason about programs with a high number of state-defining variables.

MDML Syntax

The syntax of MDML is given by the following production rules:

M odel ::=V + S C + Root M Root ? F V S ::=(public | private) statevar ID v {D v } = ι v ; D v ::=x (, x) * x ::=ID ι v ::=x C ::=input ID c {I c }; I c ::=x (, x) * Root M ::=N ode + N ode ::=G | W | T G ::=given Rule G (and Rule G ) * (N ode|{N ode + }) Rule G ::=ID v (( = | != ) x | not ? in {x (, x) * }
Rule T ::=ID v -> x | ID v -> last | DoNothing Root F ::=fallback {N ode + }
In the above grammar, ID maps to an identifier terminal and INT to an integer terminal. In the rest of this paper, we will re-use some of the non-terminal symbols to denote the set of all their instantiations within a given syntactically correct MDML model -i.e. the set of all state variables V S , the set of all input channels C, the set of all given statements G, the set of all when statements W , the set of all then statements T and the set Node for the union of the latter three. In contrast, we use D v as the set of domain values and ι v as the initial value for a given state variable v, as well as I c as the set of input values for a given input channel c. Let I τ be the set of all instantiations of τ and let RNode = Node ∪{Root M , Root F }. With P signifying the powerset, we define the function children : RNode → P(Node) which maps a non-terminal instantiation to the set of all instantiations of Node on the right side of its production rule. We also define parent : Node → RNode as the inverse of children and ancestors : Node → P(RNode) as the transitive closure of parent. We illustrate all three functions on Lines 14-16 of Listing 1.1: children(when Action = any then DoNothing;) = {(then DoNothing;)} parent(when Action = any then DoNothing;) = Root F ancestors(then DoNothing) = {Root F , (when Action = any . . . )} Using these functions, we formulate the additional syntactic rule that for each then statement t ∈ T , ancestors(t) must contain exactly one when statement from W . There are also some type restrictions to be considered. For a given state variable v ∈ V S , ι v must be an element of D v and for each occurrence of ID v on the right side of a production rule together with an x, x must be an element of D v . We also define all different D v to be disjoint sets of state variable values, even if shared value IDs occur. For each input channel c ∈ C, each occurrence of ID c together with an x on the right side of a production rule, x must be a member of I c . All I c are pairwise disjoint the same way as all D v .

MDML Semantics

With a clearly defined syntax in place, we now define a formal semantics for MDML. By mapping MDML models to Partial Moore Machines (PMMs), we first establish an operational semantics. This mapping, in turn, relies upon a Boolean predicative semantics.

Operational Semantics

Let V = {v 1 , . . . , v n } be the set of all model variables, including but not limited to V S . Further, let

D × = D v1 × • • • × D vn and D ∪ = D v1 ∪ • • • ∪ D vn .
Let public : V → B be true, iff the argument is an element of V S and declared public. Let V P = {v P 1 , . . . , v P m } = {v ∈ V S | public(v)} and let D P × be defined analogous to D × , on V P , instead of V S . We define the semantics of MDML models by mapping them to PMMs in the following way:

Q ⊆ D × (1)
q 0 = df [ι v1 , . . . , ι vn ] (2)
I = df I τ ∪ c∈C I c (3)
O ⊆ D P × (4) λ(q) = df [eval(q, v P 1 ), . . . , eval(q, v P m )] (5)
Other than externally triggered transitions, MDML also supports time-triggered transitions (see Listing 1.1, Line 10). Rather than giving MDML a full-fledged Timed-Automata semantics, we simply treat time triggers (I τ ) in the same way as external inputs, in the sense of "the external controller lets time pass" (see Equation 3). This abstraction is not without its shortcomings but it is sufficient for our MBT purposes. As shown by Equation 1, the state space of the PMM is a subset of the space of possible valuations for the variables in V. We define eval : D × × V → D ∪ to retrieve the value of a given variable in a given state. Finally, we define the transition function δ, based on the predicate transition :

D × × I × D × → B: ∀q ∈ Q, i ∈ I, q ∈ D × : δ(q, i) = q ∧ q ∈ Q ⇔ transition(q, i, q ) (6)
The remainder of this section will be dedicated to defining transition(q, i, q ) based on the contents of a given MDML model. We first break it down into its individual semantic components and finally relate them to the syntactic elements of MDML.

Predicative Semantics

The transition predicate is dependent on the primary action predicate pa, the secondary action predicate sa, the history predicate hist and the framing predicate fra:

transition (q, i, q ) ⇔ pa(q, i, q ) ∧ sa(q, i, q ) ∧ hist (q, q ) ∧ fra(q, i, q )

For all Boolean predicates introduced in this and the next section, we assume an implicit dependence on q, i, and q . In these definitions, we use v and v as a shorthand for the assignment of v ∈ V in q and q , respectively. Primary Action. A primary action is the immediate response of the state machine to an external input or a time-trigger (see Action I and τ in the grammar definition, as well as Lines 6, 9, 10, 12 and 15 in Listing 1.1), encoded in the rule hierarchy of the MDML model. This hierarchy is composed of given statements, encoding conditions on q, when statements, encoding conditions on i and then statements, encoding conditions on q . A then statement is enabled if the conditions of all its superordinate given statements evaluate to true and it is triggered if the condition of its superordinate when statement evaluates to true. A predicative definition of "enabled" and "triggered" will follow in Section 4.3. Let T P ⊆ T be the set of then statements which are both enabled and triggered. In a well-formed MDML model, the set of primary actions T P has either zero or one elements. In the case of zero elements, the MDML model does not specify a transition for the specific pair of pre-state and input. In this case, we define transition(q, i, q ) = df false and δ(q, i) remains undefined. If T P contains more than one element, the MDML model is malformed and an inconsistency error is reported. For all further considerations, we assume T P = {t P }. pa(q, i, q ) = df upd(t P )

The update predicate upd : T → B encodes the effect of a then statement on q and will also be defined in Section 4.3.

Secondary Action. A secondary action is a value change of a variable v which is conditioned on a value change of a different variable v w , as exemplified by Listing 1.1, Line 13. The effect is akin to that of a change-trigger in UML [START_REF]Object Management Group: OMG Unified Modelling Language[END_REF]. Secondary actions are encoded as when statements with a trigger rule of the form Action S ::= ID vw -> x w . Let T S ⊆ T × Action S be the set of pairs of all enabled then statements and rules of their superordinate when statements of the form Action S . We also restrict T S to those pairs which share the same root node as t P . The secondary action predicate is given as:

sa(q, i, q ) = df (IDv w ->xw),t ∈T S v w = x w ∧ v w = x w → upd(t) (9)
As can be seen from the above definition, the updates of each then statement t are performed if v w simultaneously changes from a value other than x w to x w .

History Variable Maintenance. MDML offers a language construct called lasttransition (see Listing 1.1, Line 10), where a state variable is reset to its most recent previous value. This cannot be accomplished without adding additional model variables on a semantic level. Let V H ⊆ V S be the set of all state variables v for which a then rule Rule T ::= ID v -> last exists. We define a new set of state variables called history variables H, which are bijectively associated with the variables in V H . For each v ∈ V H , we have an associated

h v ∈ H with D v = D hv and ι v = ι hv .
We can now complete the definition of the set of model variables as V = V S ∪ H. The variables in H will be used to store the previous value of their counterparts in V H . This is accomplished by the history maintenance predicate:

hist (q, q ) = df v∈V H v = v → h v = h v ∧ v = v → h v = v (10)
Framing. The predicates defined above clearly define v for some v ∈ V S and leave it undefined for others. If the v is not defined by either the primary or the secondary action, it shall remain unchanged:

fra(q, i, q ) = df v∈V S ¬def(v) → v = v (11) def(v) = df ∃x ∈ D v : pa(q, i, q ) ∧ sa(q, i, q ) v = x (12)
The helper predicate def : V S → B evaluates to true iff a unique value for v can be formally deduced (expressed by the symbol ) from the primary and/or secondary action predicates. The effect of the framing predicate can be observed in Listing 1.1, Lines 5-7, where transitions from states with Mode = Standby to Mode = Measure are specified. These transitions exist regardless of the value of Timer and trigger no secondary actions. Therefore, the framing predicate will cause Timer = Timer for each resulting transition. This results in the two transitions in Figure 1 which are labeled SMES and are not self-transitions.

Rule Hierarchy

As previously stated, we express the semantics of given and when statements via the predicates en ("enables") and tr ("triggers"), which are defined on the syntactic elements of the rule hierarchy:

en(Root M ) ⇔ df true en(G) ⇔ df en(parent(G)) ∧ en(Rule G1 ) ∧ • • • ∧ en(Rule Gk ) en(ID v = x) ⇔ df v = x en(ID v != x) ⇔ df v = x en(ID v in {x 1 , . . . , x k }) ⇔ df v ∈ {x 1 . . . , x k } en(ID v not in {x 1 , . . . , x k }) ⇔ df v / ∈ {x 1 . . . , x k } en(W ) ⇔ df en(parent(W )) en(T ) ⇔ df en(parent(T )) en(Root F ) ⇔ df t ∈ T P : Root M ∈ ancestors(t)
The main root of the rule hierarchy (Root M ) is enabled by default. Each given statement inherits the enabledness of its parent and imposes its own conditions (Rule G ) on q in the form of equality, inequality and set exclusion and inclusion of state variable values v in q. Both when and then statements inherit enabledness from their parent statements. The when statements in Lines 12 and 13 of Listing 1.1, for example, are direct children of Root M and always enabled while those in Lines 6, 9 and 10 are conditioned upon the value of the state variable Mode in q.

We complete the definition of en by examining the semantics of the fallback root Root F , which is enabled when the main rule hierarchy specifies no primary action. The fallback mechanism was designed to provide the users of MDML with an easy way to incorporate "exception handling" in their models or make their models input-complete. Secondary actions (Action S ) do not rely upon this predicate and evaluate to false. The semantics of when statements is encoded in the predicate tr:

tr(Root M ) ⇔ df false tr(Root F ) ⇔ df false tr(G) ⇔ df tr(parent(G)) tr(W ) ⇔ df tr(Rule W 1 ) ∨ • • • ∨ tr(Rule W k ) tr(ID c = x) ⇔ df i = x tr(ID c != x) ⇔ df i ∈ I c \ {x} tr(ID c in {x 1 , . . . , x n }) ⇔ df i ∈ {x 1 , . . . , x k } tr(ID c not in {x 1 , . . . , x n }) ⇔ df i ∈ I c \ {x 1 , . . . , x k } tr(ID c = any) ⇔ df i ∈ I c tr(τ ) ⇔ df i = τ tr(Action S ) ⇔ df false tr(T ) ⇔ df tr(parent(T ))
Unlike the value of en, tr starts out as false on both roots. If the current input i satisfies a trigger rule Rule W of a when statement, the statement gets triggered.

Here, Rule W can again be based on equality or inequality, as well as set inclusion and exclusion relative to the input alphabet I c of a given input channel c. However, since i is not guaranteed to be an element of I c , the conditions are formulated in a type-safe manner. Alternatively, primary actions can be triggered by time triggers τ . Analogous to en, given and then statements inherit the tr value of their parent node. The effect of a then statement on q is encoded by the update predicate upd:

upd(T ) ⇔ df upd(Rule T 1 ) ∧ • • • ∧ upd(Rule T k ) upd(ID v -> x) ⇔ df v = x upd(ID v -> last) ⇔ df v = h v upd(DoNothing) ⇔ df v∈V S v = v
The most common case of Rule T is the assignment of v to a specific value x. Alternatively, the rule DoNothing encodes a self-transition (δ(q, i) = q) and ID v -> last causes v to assume the value that was held prior to v.

Model Transformation

To transform a given MDML model into a PMM, we first obtain I and q 0 directly from the model. We then perform a closure on Q under δ for all i ∈ I. To do that, we state the transformation problem as obtaining a post-state q for a given pre-state q and input i according to Equation 6. The transformation problem is a Constraint Satisfaction Problem (CSP), which we encode as a PMSAT problem and solve with an appropriate solver. We do, however perform a prefiltering step by computing T P and T S via imperative algorithms and therefore exclude all irrelevant model elements from the CSP. This was done to further both performance and ease of implementation.

PMSAT-Encoding of the Transformation Problem

The assignments of the MDML model variables in both pre-and post-state become the variables of the CSP:

V CSP = v∈V {v, v } (13)
There are multiple ways to encode a CSP into SAT. For the transformation problem, we follow the direct encoding method described by Walsh [START_REF] Walsh | SAT v CSP[END_REF]. The encoding of CSP variables with multi-value domains into Boolean SAT variables is accomplished by:

V SAT = b vx ∈ B | v ∈ V CSP ∧ x ∈ D v ∧ b vx = true ⇔ v = x (14)
Although there are more concise encodings, the direct encoding was again chosen to ease implementation. The MDML model in Listing 1.1, for example, would produce eight Boolean variables, for Mode=Standby, Mode=Measure, Timer=On and Timer=Off in both q and q . This encoding requires additional clauses to ensure that each CSP variable is assigned exactly one value. The valuation in the pre-state q is known a-priori and be directly evaluated as x = eval(q, v) and all Boolean variables encoding q can be set to a fixed value:

pre(q) = v∈V   v = x ∧ x∈Dv\{x} v = x  (15)
The valuation in the post-state q is as of yet unknown and only restricted by the known variable domains.

post(q ) = v∈V   x∈Dv v = x ∧ x1∈Dv,x2∈Dv\{x1} (v = x 1 → v = x 2 )   (16)
Leaving the conversion to CNF implicit, the full set of hard clauses for the PMSAT problem emerges as:

Φ H SAT = pa(q, i, q ) ∧ sa(q, i, q ) ∧ hist (q, q ) ∧ pre(q) ∧ post(q )

Up to this point, fra(q, i, q ) has not been represented in terms of a firstorder logic formula. In CSP problems, framing axioms explicitly ensure that every variable change has a defined cause [START_REF] Kaufmann | Global state checker: Towards SAT-based reachability analysis of communicating state machines[END_REF]. However, this would require us to establish an explicit cause-and-effect relationship between variable changes to ensure that each secondary action is directly or indirectly caused by the primary action. Otherwise, the solution might contain groups of secondary actions which are causing each other -i.e. forming causal loops. Instead of using framing axioms, we decided to formulate the transformation problem in PMSAT and model fra(q, i, q ) by means of soft clauses:

Φ S SAT = v∈V S v = v (18)
Theorem 1. If the SAT problem Φ H SAT has a solution, 3 the solution to the PM-SAT problem Φ H SAT , Φ S SAT satisfies transition (q, i, q ).

Proof. The structure of the proof is as follows: First, we find a solution which minimizes the cost function of the PMSAT problem. Then, we confirm that this solution fulfills the framing predicate and is a valid solution to the SAT problem. Let V d ⊆ V S be the set of all state variables which are uniquely defined, i.e. are assigned the same value in all solutions of the pure SAT problem. Let V f = V S \ V d be the set of all state variables which are not uniquely defined. Following Equation 18, the cost function of the PMSAT problem can be reformulated in the following way, intuitively showing the global minimum:

E(q ) = c + v∈V f 0 iff v = v 1 otherwise (19)
Here, c is a constant value caused by the variables in V d . The post-state q min with ∀v ∈ V f : v = v yields the minimum cost value E(q min ) = c. We now examine the fulfillment of each predicate in Equations 7 and 17: Primary action: The primary action predicate references q solely via the predicate upd, which either does not reference any given v or restricts it to a single value. Therefore, all variables referenced by the primary action must be element of V d and q min cannot falsify this predicate.

Secondary action: The secondary action predicate references q via the update predicate, as well as in the left-hand side of an implication. If a variable from V d triggers a secondary action, all variables referenced by upd will be uniquely determined (see proof for primary action) and, in turn, be part of V d . The valuation of V f in q min , cannot trigger any secondary actions since v = v for all v ∈ V f . In other words, all variables in V f trivially fulfill the predicate for q min .

History: We assume that the assignment of all h ∈ H in q min satisfies the history predicate. All variables in V S are either not referenced or referenced in the left-hand side of an implication and therefore cannot falsify the predicate.

Pre-State: The pre-state predicate does not reference q .

Post-State: The post-state predicate establishes the domain for all v but does not restrict them any further.

Framing:

Let V dp = {v ∈ V S | def(v)} and V fp = V S \V dp .
From the definition of def and V d , it follows that V dp ⊆ V d and, consequently, V f ⊆ V fp . From the above proofs, it is evident that, if a given v is not uniquely determined by the primary or secondary action, it also cannot be further determined by any other predicates. Therefore we get V fp ⊆ V f and, consequently, V fp = V f . In q min , we have v = v for all variables in V f , fulfilling the framing predicate.

With exception of the framing predicate, all other predicates are (either generally or specifically for q min ) independent of all variables in V f . Therefore q min must be a valid solution to the SAT problem.

Consistency Check

In order to be transformed into a Partial Moore Machine (PMM), an MDML model needs to be well-formed. To define the notion of well-formedness, we ex-ploit an important duality between model transformation and consistency checking: An MDML model is well-formed, iff the transformation into a PMM succeeds. Or in other words, each failure mode of the transformation corresponds to a possible type of model error. To avoid redundancies in our implementation, we directly check the consistency of MDML models by attempting a model transformation. in the MDML model may take one of the following forms: q ∈ D × : transition (q, i, q ). They will be the focus of this Section. Contradictions can be as obvious as then Mode -> Standby and Mode-> Measure, but also more subtle due to the involvement of secondary actions.

-Remaining gaps in the semantics definition -e.g. multiple time-triggered then statements enabled in the same pre-state -must be explicitly disallowed and prevented via dedicated consistency checking methods.

Inconsistency Detection via PMSAT

Assuming the transformation problem has no solution, despite having a unique primary action, we define the checking problem as detecting a set of model elements which causes the contradiction. The checking problem could be solved by computing an unsatisfiability core and removing any axiomatic clauses, e.g. from pre(q), post(q ) or hist (q, q ). To avoid a further increase of requirements to the solver's capabilities, we instead formulate the checking problem again as a PMSAT problem. If a contradiction in the model prevents a solution of the transformation problem (Eq. 17), it is due to the presence of inconsistent upd predicates which only occur as part of pa and sa. To identify these contradictory predicates, we set up the checking problem ΦH SAT , ΦS SAT as a modified version of the transformation problem with pa and sa moved to the set of soft clauses: ΦH SAT = hist (q, q ) ∧ pre(q) ∧ post(q ) (20) ΦS SAT = pa(q, i, q ) ∧ sa(q, i, q )

In this way, the solver will remove the minimum number of clauses from pa and sa to produce a solution for q . Each one of these unfulfilled clauses contains an update predicate (or part thereof) which contributes to the contradiction. By iterating through all solutions with the optimal cost value and backtracking the unfulfilled clauses of each solution to their syntactic element of origin, we obtain a set of update rules (Rule T ) which make the model inconsistent. These model elements are then marked as erroneous. Hence, we use PMSAT for debugging.

Warnings against Dead Code and Redundancy

For the consistency checking of MDML models, we define an error as an aspect of the model which makes it unsuitable for further processing -e.g. test case generation. All other issues which do not fall under this category are classified as warnings. As such, we regard aspects of the MDML model which we believe may not reflect the intentions of the user, e.g. unreachable or redundant MDML statements. To identify such model elements, we relate the PMM, which was obtained through the model transformation, back to the original MDML model. The set of unreachable statements -i.e. dead code -can be obtained as Node U = {n ∈ Node| q ∈ Q : en(q, n)} while the set of redundant given statements is obtained as G R = {g ∈ G | q ∈ Q : en(q, parent(g)) ∧ ¬en(q, g)}.

Evaluation

We have implemented the previously described model transformation and consistency checking mechanism as part of our MDML IDE, using the SAT4J solver [START_REF] Berre | The Sat4j library, release 2.2[END_REF]. We have analyzed the runtime of the model transformation on 87 MDML models, taking the median of 10 repetitions for each model. Figure 2 displays the runtime measurements with respect to the number of states (|Q|), as well as the number of transitions (|δ|) of the individual MDML models. The runtime is polynomial with respect to both the number of states and transitions, as indicated by the linear-shaped distributions in both doubly-logarithmic plots.

Related Work

Our solution to the frame problem is similar to that of Answer Set Programming (ASP) [START_REF] Lifschitz | What is answer set programming?[END_REF]. The frame rule in ASP states that, if a property holds in the prestate and it cannot be derived that the property does not hold in the post-state, then it is assumed that the property holds in the post-state.

Mapping a DSL to a Moore Machine-based semantics has been done before [START_REF] Alenljung | Sensor graphs for discrete event modeling applied to formal verification of PLCs[END_REF][START_REF] Beyak | SAGA: A DSL for story management[END_REF][START_REF] Schuts | Reverse engineering of legacy software interfaces to a model-based approach[END_REF]. However, to the best of our knowledge, we are the first to define a predicative semantics of a DSL based on PMSAT. Biere et al. [START_REF] Biere | Bounded model checking[END_REF] have mapped the Bounded Model Checking problem to SAT. However, their technique is concerned with verifying temporal properties while we aim to check model consistency, unreachability, and redundancy. Hwong et al. [START_REF] Hwong | Formalising and analysing the control software of the compact muon solenoid experiment at the large hadron collider[END_REF] have designed and implemented a mapping from the textual State Machine Language to a process algebraic language called mCRL2 in order to verify the highly complex control software of one of the experiments at CERN. They then use Bounded Model Checking to detect live-locks and ensure strong connectedness. Löding and Peleska [START_REF] Löding | Timed moore automata: Test data generation and model checking[END_REF] present an operational semantics for their Timed Moore Automata formalism, which they use for livelock detection and SAT-based test case generation. Mechtaev et al. have devised a tool called DirectFix [START_REF] Mechtaev | Directfix: Looking for simple program repairs[END_REF] for program repairs based on PMSAT or, more specifically, Partial MAX-SMT. Similarly to our approach, Tien et al. [START_REF] Tien | Modeling and debugging numerical constraints of cyber-physical systems design[END_REF] use PMSAT to find contradictory constraints in SysML models.

Conclusion

We have defined a formal semantics for the pre-existing domain-specific modeling language MDML. We split the definition into an operational semantics, relating MDML models to Partial Moore Machines, and a predicative semantics, defining the relation between pre-and post-states of each transition. We have designed and implemented a model transformation from MDML models to PMMs, based on a Partial MAX-SAT problem. To the best of our knowledge, we are the first to show how PMSAT can be used to solve the frame problem when an approach based on pure SAT would significantly complicate the solution. However, we kept parts of the implementation imperative wherever the cost of a SAT-based implementation outweighed the benefits. We prioritized ease of implementation over performance, since the test models in our domain are rather small. In theory, we would be able to eliminate the need for PMSAT by excluding Secondary Actions from the language design. However, they considerably simplify the implementation of certain behaviors, resulting in shorter models. We have further established a duality between model transformation and consistency checking for MDML models, enabling us to turn the transformation into a consistency check with little effort. Our future work may encompass the automatic repair of contradictory MDML models, perhaps in a similar manner as DirectFix [START_REF] Mechtaev | Directfix: Looking for simple program repairs[END_REF].

1

  public statevar Mode { Standby , Measure } = Standby ; 2 private statevar Timer { Off , On } = Off ; 3 input Action { STBY , SMES , STIM }; STBY then Mode -> Standby ; 10 given Timer = On when 15 sec elapsed then Mode -> last ; 11 } 12 when Action = STIM then Timer -> On ; 13 when Mode -> Standby then Timer -> Off ; 14 fallback { 15 when Action = any then DoNothing ; 16 } Listing 1.1: Example MDML model

Fig. 1 :

 1 Fig. 1: Partial Moore Machine representation of the system represented in Listing 1.1. The values of private state variables, which are not part of the output, are displayed in brackets.

  ) W ::=when Rule W (or Rule W ) * (N ode|{N ode + }) Rule W ::=Action I | τ | Action S Action I ::=ID c (( = | != ) x | = any | not ? in {x (, x) * }) τ ::=INT (ms | sec | min) elapsed Action S ::=ID v -> x T ::=then Rule T (and Rule T ) * ;

-

  Syntax errors are handled directly by the textual editor. -Domain errors, e.g. when c = x with x / ∈ I c are also handled by the editor. -Explicit transformation errors, e.g. |T P | > 1 are handled as software exceptions, thrown within the transformation algorithm. -Contradictions within an MDML model can be discovered if |T P | = 1 but

Fig. 2 :

 2 Fig. 2: Runtime evaluation of the model transformation with respect to the number of states |Q| (left) and the number of transitions |δ| (right)

Note that the reverse implication is trivially fulfilled, since PMSAT can only pick the optimum from all possible solutions of the underlying SAT problem.

Acknowledgements. Research herein was partially funded by the Austrian Research Promotion Agency (FFG), program "ICT of the Future", project number 867535 Hybrid Domain-specific Language User eXperience (HybriDLUX).


Andrea Pferscher
email: apfersch@ist.tugraz.at

Bernhard K Aichernig
email: aichernig@ist.tugraz.at

Learning Abstracted Non-Deterministic Finite State Machines

Keywords: Active automata learning, Model inference, Non-deterministic finite state machines, MQTT

Active automata learning gains increasing interest since it gives an insight into the behavior of a black-box system. A crucial drawback of the frequently used learning algorithms based on Angluin's L * is that they become impractical if systems with a large input/output alphabet are learned. Previous work suggested to circumvent this problem by abstracting the input alphabet and the observed outputs. However, abstraction could introduce non-deterministic behavior. Already existing active automata learning algorithms for observable non-deterministic systems learn larger models if outputs are only observable after certain input/output sequences. In this paper, we introduce an abstraction scheme that merges akin states. Hence, we learn a more generic behavioral model of a black-box system. Furthermore, we evaluate our algorithm in a practical case study. In this case study, we learn the behavior of five different Message Queuing Telemetry Transport (MQTT) brokers interacting with multiple clients.

Introduction

The origin of automata learning dates back to the seventies and eighties, when Gold [START_REF] Gold | System identification via state characterization[END_REF] and Angluin [4] introduced algorithms to learn behavioral models of black-box systems. Later, in the seminal work of Peled et al. [START_REF] Peled | Black box checking[END_REF], automata learning proofed itself as a valuable tool to test black-box systems. Today automata learning reveals security vulnerabilities in TLS [START_REF] De Ruiter | Protocol state fuzzing of TLS implementations[END_REF] or DTLS [START_REF] Fiterau-Brostean | Analysis of DTLS implementations using protocol state fuzzing[END_REF].

The applicability of automata learning, however, suffers from two main problems: (1) automata learning becomes infeasible for systems with a large input and output alphabet and (2) many systems behave non-deterministically, e.g. due to timed behavior or stochastic decisions. One promising solution for the first problem was proposed by Aarts et al. [2]. They presented an abstraction technique that introduces a more generic view on the system by creating an abstract and, therefore, smaller input and output alphabet. However, a too coarse view on the system creates non-determinism, which leads back to the second problem. In the literature, several work on learning-based testing [START_REF] Tappler | Model-based testing IoT communication via active automata learning[END_REF][START_REF] Fiterau-Brostean | Analysis of DTLS implementations using protocol state fuzzing[END_REF][START_REF] Aichernig | Learning-based testing of an industrial measurement device[END_REF] stress the problem of observing non-deterministic behavior during learning. However, we already find learning algorithms [START_REF] El-Fakih | Learning finite state models of observable nondeterministic systems in a testing context[END_REF][START_REF] Pacharoen | Active learning of nondeterministic finite state machines[END_REF][START_REF] Khalili | Learning nondeterministic mealy machines[END_REF] for observable non-deterministic reactive systems. To make them applicable, we have to provide an input and output alphabet that establishes observable non-determinism, i.e. systems where an input may lead to different states, but we can observe which state has been chosen.

In this paper, we propose an active learning algorithm for observable nondeterministic finite state machines (ONFSMs) that addresses both problems of active automata learning. The first problem is solved via a mapper that provides a more generic view on the system under test (SUT) via an abstract input/output alphabet. The non-deterministic behavior is handled by our learning algorithm for ONFSMs. We show that an abstracted input/output alphabet does not necessarily decrease the state space of a non-deterministic systems sufficiently. To overcome the state-space problem, we introduce a new abstraction technique that defines equivalence classes for outputs and merges akin states of the model.

We evaluated our proposed learning algorithm on the MQTT protocol, which is a publish/subscribe protocol that is frequently used in the Internet of Things (IoT). This protocol defines the communication between clients and a broker, where the broker manages the messages of the clients. Tappler et al. [START_REF] Tappler | Model-based testing IoT communication via active automata learning[END_REF] showed that automata learning is an effective method to test the behavior of different MQTT brokers. However, in their work they only considered an interaction with one or two clients to keep the learning feasible. Furthermore, they stress that the non-deterministic behavior hampered the learning procedure. In this paper, we show that our algorithm for observable non-deterministic systems makes learning-based testing of the MQTT protocol in a multi-client setup feasible.

Our contribution comprises four aspects. [START_REF] Aarts | Automata learning through counterexample guided abstraction refinement[END_REF] We analyze the challenges of learning an abstracted system that behaves non-deterministically. (2) We propose a new abstraction technique that manages these challenges. [START_REF] Aichernig | Learning-based testing of an industrial measurement device[END_REF] We introduce a new active learning algorithm that integrates our proposed abstraction technique and, therefore, learns a more abstract model of a non-deterministic system. (4) We show the applicability of our algorithm in a case study and compare it to existing algorithms for deterministic finite state machines (FSMs).

Structure. Section 2 explains the modeling formalism and active automata learning. In Sect. 3, we introduce our learning algorithm including our novel abstraction technique. Our case study on five different MQTT brokers is presented in Sect. 4. Section 5 discusses related work. Finally, Sect. 6 concludes the paper.

Preliminaries

Finite State Machines

An observable non-deterministic finite state machine (ONFSM) is a 5-tuple M = Σ I , Σ O , Q, q 0 , h where Σ I is the finite set of input symbols, Σ O is the finite set of output symbols, Q is the finite set of states, q 0 is the initial state, and

h ⊆ Q × Σ I × Σ O × Q is the transition relation.
We denote a transition in the ONFSM by q i/o --→ q , where (q, i, o, q ) ∈ h. The assumed ONFSMs are input enabled, i.e., there exists for every pair (q, i), where q ∈ Q and input i ∈ Σ I , at least one output o ∈ Σ O and successor state q ∈ Q. Further, we call the finite state machine observable if there exists for any triple (q, i, o) at most one q such that (q, i, o, q ) belongs to h. Hence, in fact, we have a state transition function δ : Q × I × O → Q, that maps a triplet (q, i, o) to a unique state q . Note that learning algorithms, like the ones used in the tool LearnLib [START_REF] Isberner | The open-source LearnLib -A framework for active automata learning[END_REF], commonly require deterministic systems. We define an FSM as deterministic if there exists for each input at most one output and succeeding state. In the literature, deterministic FSM are also known as Mealy machines.

Let s ∈ (Σ I × Σ O ) * be an input/outputs sequence, with the corresponding input projection s I ∈ Σ * I and output projection s O ∈ Σ * O . We write for the empty sequence and s • s for the concatenation of two sequences, where s, s ∈ (Σ I × Σ O ) * . We also define a single input/output pair (i, o) ∈ (Σ I × Σ O ) as a sequence and, therefore, s • (i, o) is also defined. The function pre(s) returns the prefixes of s, including the sequence s.

Let s + ∈ (Σ I × Σ O ) + , s + I ∈ Σ + I , s + O ∈ Σ + O
denote non-empty sequences. For convenience, we write s • (s + I , s + O ), defining a sequence s that is concatenated with a sequence of input/output pairs.

Active Automata Learning

In active automata learning, we gain understanding about a system by actively questioning the SUT. Many active automata learning algorithms build on the seminal work of Angluin [4]. Her proposed algorithm (L * ) learns a deterministic finite automaton (DFA) that accepts a regular language. The learning procedure is based on the minimally adequate teacher (MAT) framework, which comprises a teacher and a learner component. The learner asks the teacher either a membership query or an equivalence query. The former one answers if a word is part of the language, whereas the second one checks if a hypothesis, i.e. a proposed DFA, represents the regular language. The equivalence query is either answered with yes or with a counterexample that shows an evidence to the non-conformance of the proposed hypothesis and the SUT. All the answers from the queries are saved in an observation table, which is then used to construct a hypothesis.

Angluin's L * has been extended for different types of systems, including algorithms for Mealy machines [START_REF] Margaria | Efficient test-based model generation for legacy reactive systems[END_REF][START_REF] Niese | An integrated approach to testing complex systems[END_REF][START_REF] Shahbaz | Inferring mealy machines[END_REF]. In these algorithms for learning Mealy machines, membership queries are replaced by output queries. There, instead of asking whether a word is in the language, an input string is provided. The teacher executes this input string on the SUT and responds the observed output string. The observed outputs are then saved in the observation table.

The previously mentioned learning algorithms can only handle deterministic SUTs. Tackling the problem that systems behave non-deterministic due to various reasons, e.g. ignoring timed behavior, L * -based learning algorithms [START_REF] El-Fakih | Learning finite state models of observable nondeterministic systems in a testing context[END_REF][START_REF] Pacharoen | Active learning of nondeterministic finite state machines[END_REF][START_REF] Khalili | Learning nondeterministic mealy machines[END_REF] for ONFSMs were proposed. The algorithms for ONFSMs follow the idea of the Mealy machine learning algorithms, but instead of considering just one possible output for an input, all possible outputs are saved in the observation table.

One major drawback of the Angluin style algorithms is that they do not scale for a large input/output alphabet, since the number of required queries significantly grows with the increasing size of the used alphabet. To overcome this problem, Aarts et al. [2] proposed an abstraction technique that reduces the size of the used input/output alphabet of the learning algorithm. This abstraction technique introduces a mapper component that translates the communication between the learner and the SUT in both directions.

A mapper is an 8-tuple A = Σ I , Σ O , R, r 0 , Σ A I , Σ A O , ∆, ∇ , where Σ I and Σ O are the disjoint sets of concrete inputs and outputs, R is the set of mapper states, r 0 ∈ R is the initial state, Σ A I and Σ A O are the finite disjoint sets of abstract inputs and outputs, ∆ : R × (Σ I ∪ Σ O ) → R is the state transition function, and

∇ : (R × Σ I → Σ A I ) ∪ (R × Σ O → Σ A O )
is the abstraction function. The mapper takes abstract inputs and translates them to concrete inputs, which can then be executed on the SUT. In return, the mapper observes concrete outputs from the SUT and returns the corresponding abstracted outputs to the learner. On each received input/output pair, the mapper updates its internal state.

A large input/output alphabet is not the only challenge that limits the feasibility of active automata learning. Berg et al. [START_REF] Berg | On the correspondence between conformance testing and regular inference[END_REF] state that the real bottleneck of active automata learning is the equivalence oracle since the presence of such an oracle is highly improbable. To make active learning practically applicable, tools like LearnLib [START_REF] Isberner | The open-source LearnLib -A framework for active automata learning[END_REF] substitute the equivalence oracle by conformance testing. In this section, we describe our active learning algorithm for abstracted ONFSMs. Firstly, we introduce our basic learning setup. Secondly, we explain the two different levels of abstraction and, thirdly, we discuss the application of our abstraction mechanism on the learning algorithm.

Learning Setup

Our proposed learning algorithm for ONFSMs is based on an Angluin-style active learning setup. For this, we define a learner that queries a teacher. Figure 1 shows the components of our learning algorithm. The teacher comprises three components: (1) conformance testing, (2) a mapper and (3) the SUT. (1) The aim of conformance testing is to make the equivalence check feasible. For this, we assume that the learned model conforms to the SUT if a finite set of test cases passes. (2) The mapper is based on the idea of Aarts et al. [2], where the mapper translates a (possibly infinite) alphabet to a finite alphabet that is used by the learning algorithm to create an abstracted model. The difference to Aarts' proposed mapping concept is that we do not require an abstracted alphabet that assures that the learned model behaves deterministically. This gives us the possibility to create an even more abstract view on the SUT. (3) The SUT represents an interface, where concrete inputs can be executed and the corresponding concrete outputs can be observed by the mapper. This allows a black-box view on the SUT.

The difference to other active learning setups is that the learner uses an additional abstraction mechanism for the observation table. To avoid confusion between the abstraction done by the mapper and the abstraction of the observation table, we distinguish two levels of abstraction. We denote the abstraction by the mapper as first level abstraction and the abstraction of the observation table is denoted as second level abstraction. The first level abstraction comprises the mapper component of the teacher that translates abstract inputs to concrete inputs and concrete outputs to abstract outputs. The aim of mapping is to decrease the size of the alphabet to make the learning algorithm feasible. However, Aarts et al.

First Level Abstraction

[2] stress that a too abstract alphabet creates non-determinism, which is not suitable for many learning algorithms. We circumvent the problem of creating a deterministic alphabet by using a learning algorithm for non-deterministic systems. Still, the abstracted alphabet must not violate the assumption of observable non-deterministic outputs. If the abstraction is too coarse, we have to refine the abstracted outputs by introducing new outputs that make the model of the SUT observable non-deterministic.

Example 1 (Multi-Client Connection Mapper). Our goal is to learn a model of an MQTT broker that interacts with several clients. For simplicity, here we only consider the connection procedure of the protocol. The clients can send a connection request to the broker. A client gets disconnected if the client is already connected. The concrete inputs are Σ I = {Connect(id )|id ∈ N} and the concrete outputs Σ O = {Ack(id ), Closed(id )|id ∈ N}, where id ∈ N uniquely identifies a client by an integer. Therefore, the set of concrete inputs and outputs is infinite. To build a finite model of this connection protocol for multiple-clients, we have to define a mapper that abstracts the input/output alphabet. The mapper for this example has the abstracted inputs Σ A I = {Connect} and abstracted outputs Σ A O = {Ack, Closed}. The abstracted non-deterministic model is depicted in Fig. 2. We distinguish the states where no client (q 0 ) or more than one client (q 1 ) is connected. In the state where more than one client is connected, further clients can connect or disconnect. Since the Mealy machine in Fig. 2 is not observable non-deterministic, we have to refine the abstracted outputs to make the states distinguishable. For this, we add another abstract output Closed All, capturing the observation when the last client gets disconnected, to Σ A O which makes the automaton observable non-deterministic. The refined model is depicted in Fig. 3.

Second Level Abstraction

The first level abstraction enables an abstracted view and supports the feasibility of the learning algorithm. However, due to the iterative state exploration of L * , In our learning algorithm, the learner maintains an extended observation table. The classic observation table T is defined as a triplet Γ, E, T , where Γ ⊂ (Σ A I × Σ A O ) * contains sequences of inputs and outputs, E ⊂ Σ A + I is a suffixed closed set of input sequences, and T is a mapping

Γ × E → 2 Σ A O + containing first level abstract outputs of the power set of Σ A O + . The extension of the classi- cal observation table T A is a 5-tuple Γ, E, T, T A , µ where T A is a mapping Γ × E → 2 Σ A O +
to the second level abstracted outputs and µ :

Σ A O → Σ A
O is the second level abstraction function. ). Table 1 shows an intermediate observation table in the learning procedure of the system depicted in Fig. 3. Table 1 is then abstracted with the equivalence classes defined in Example 2. The abstracted observation table is presented in Table 2.

Example 3 (Multi-Client Connection Observation Table

Learning Algorithm

In the following, we introduce our learning algorithm for ONFSMs. Especially, we explain the integration of the second level abstraction in the L * -based learning setup and how this abstraction technique generates a more generic hypothesis.

Algorithm 1 Learning algorithm using an abstracted observation table

Input: input alphabet Σ A I , equivalence class map- ping µ, teacher Π Output: ONFSM H 1: Γ, E, T ← InitTable(Σ A I ) 2: cex ← 3: do 4: Γ, E, T ← FillTable( Γ, E, T , Π)

5:

T A ← AbstractTable( Γ, E, T , µ)

6:

while ¬IsClosedConsistentComplete(T A ) do 7:

Γ ← MakeClosed(T A ) 8:
Γ, E, T ← FillTable( Γ, E, T , Π) 9:

T A ← AbstractTable( Γ, E, T , µ) 10: Γ ← CompleteQueries(T A )

11:

Γ, E, T ← FillTable( Γ, E, T , Π)

12:

T A ← AbstractTable( Γ, E, T , µ)

13:

E ← MakeConsistent(T A )

14:

Γ, E, T ← FillTable( Γ, E, T , Π) 15:

T A ← AbstractTable( Γ, E, T , µ)
16:

H ← ConstructHypothesis(T A ) 17: cex ← ConformanceTest(H) 18: if cex = then 19: Γ, E, T ← AddCex(cex, Π)
20: while cex = 21: return H Algorithm 1 describes the procedure performed by the learner to learn an ONFSM. For this, the learner requires the abstract input alphabet Σ A I of the SUT, the second level abstraction mapping µ, and the teacher Π which provides access to the mapper and SUT. In Line 1 and 2 we start with the initialization of the observation table and the counterexample (cex). Remember that the classic observation table is a triplet T = Γ, E, T . Γ is a prefixed-closed set of sequences, which can be written as Γ = Γ S ∪ Γ P where Γ S ∩ Γ P = ∅. Γ S contains the sequences that identify the states of the ONFSM and Γ P = Γ P S ∪ Γ P , where

Γ P S ⊆ Γ S • (Σ A I × Σ A O ), Γ P ⊂ Γ • (Σ A I × Σ A O )
and Γ P S ∩ Γ P = ∅. We initialize T by adding the empty sequence to Γ S and the input alphabet Σ A I to E. After the initialization we fill the observation table T (Line 4) by performing output queries to the teacher Π. The mapper translates the first level abstracted inputs of Σ A I to concrete inputs of Σ I and the observed concrete outputs of Σ O to first level abstracted outputs Σ A O . Every time we fill the table with the query outputs we extend the observation table T = Γ, E, T to the abstract observation table T A = Γ, E, T, T A , µ by translating observed outputs with µ as explained in Sect. 3.3. Note that the second level abstraction only changes the mapping T A ; Γ , E and T stay unchanged.

After the abstraction in Line 5 we check in Line 6 if the abstracted observation table T A is closed, consistent and complete. To the best of our knowledge, this part is different to other learning algorithms.

Closedness First, we check if the abstracted table T A is closed. This check is similar to the closed check proposed by El-Fakih et al. [START_REF] El-Fakih | Learning finite state models of observable nondeterministic systems in a testing context[END_REF], however, instead of checking the values in the mapping T , we check if the second level abstracted outputs in T A are equal. For this, we denote that two rows γ, γ ∈ Γ in the abstracted table are equal, i.e. γ ∼ =A γ , iff ∀e ∈ E, T A (γ, e) = T A (γ , e). The abstract observation table T A is not closed if there exists a γ ∈ Γ P such that no γ ∈ Γ S fulfills γ ∼ =A γ .

Consistency Unlike the other learning algorithms for ONFSMs, we have to check if our abstract observation table T A is consistent. The consistency check is necessary due to queries that are added through the abstraction mechanism and due to the counterexample processing which we discuss later in this section. Our check is based on the consistency check for Mealy machines introduced by Niese [START_REF] Niese | An integrated approach to testing complex systems[END_REF]. We define that T A is consistent if for every γ, γ ∈ Γ , where γ ∼ =A γ holds, no input/output pair (i, o)

∈ (Σ A I ×Σ A O ) exists where γ •(i, o) A γ •(i, o).
Completeness The completeness check is different to other active learning algorithms. Here we check, if we have added all necessary sequences to construct a hypothesis. Since the final hypothesis contains the first level abstracted outputs, but is constructed based on the second level abstraction outputs, it may be necessary to add additional sequences to Γ . These sequences are required to identify the target state of all observed input/output pairs. For this, we define that two rows γ, γ ∈ Γ in the classic observation table are equal, denoted by γ ∼ = γ , iff ∀e ∈ E, T (γ, e) = T (γ , e). For each γ ∈ Γ S we select each γ ∈ Γ P where γ ∼ =A γ but γ γ holds. We then check if Γ contains all sequences pre(γ • (e, s + O )) where e ∈ E and T (γ, e) = T (γ , e), and s + O ∈ T (γ , e). If no such sequence is required or all required sequences already exist, T A is complete.

If either the abstracted table T A is not closed or not consistent or not complete, we continue our procedure in Line 7. Here, we make T A closed if necessary. To make T A closed, we move every row γ ∈ Γ P to Γ S , where ∀γ ∈ Γ S : γ A γ holds. Informally, we move every row from Γ P to Γ S where the set of abstracted outputs for all e ∈ E is unique. This introduces a new state in our hypothesis. If we have found such a γ ∈ Γ P , we have to add all observed outputs in the mapping T from the row γ to Γ P S . For this, we concatenate γ with each observed input/output pair in that row, i.e. for each i ∈ Σ A I we add for each observed output sequence o ∈ T (γ , i) the concatenation γ • (i, o) to Γ P S . Afterwards, we fill the table T according to the updated Γ in Line 8 and in the next line we construct again T A .

Example 4 (Closed Abstracted Observation Table ). Table 3 shows the observation table after the first output queries. We abstract the table using the mapping function µ introduced in Example 2. The result of the abstraction is shown in Table 4. According to Algorithm 1 we then check if the abstracted table is closed. Since the row (Connect, Ack) is in Γ P and the produced outputs are not in Γ S , Table 4 is not closed. To make the table closed, we move (Connect, Ack) to Γ S and add the corresponding sequences of the observed outputs to Γ P . The result including the additionally performed output queries is shown in Table 1. We then again abstract this table -shown in After making the abstract table closed and performing the required queries to fill the table, we add in Line 10 all necessary queries to make the table complete. For this, we select for all γ ∈ Γ S every γ ∈ Γ P where γ ∼ =A γ . If then γ γ , we select the input sequence e ∈ E where T (γ, e) = T (γ , e) and the output sequence where the observed outputs are different, i.e. s + O ∈ T (γ , e) \ T (γ, e). (Table 5). After making Table 5 complete, we abstract the table (Table 6). Table 6 is now closed and complete.

If the table is closed and complete, we make in Line 13 the abstracted observation table consistent. For each two rows γ, γ ∈ Γ where γ ∼ =A γ and an input/output pair (i, o)

∈ (Σ A I × Σ A O ) where γ • (i, o) A γ • (i, o) exists, we add i • e to E, where e ∈ E and T (γ • (i, o), e) = T (γ • (i, o), e).
When the table is closed, complete and consistent, we construct a hypothesis from our abstract observation table in Line 16 of Algorithm 1. Since we consider two different levels of abstraction in our observation table, we have to modify the classical construction approach from El-Fakih et al. [START_REF] El-Fakih | Learning finite state models of observable nondeterministic systems in a testing context[END_REF]. Algorithm 2 describes the process of generating an ONFSM M from the abstract observation table T A . The initialization process in Line 2 and 3 of Algorithm 2 is equal to other L * -style algorithms. For this, the empty sequence indicates the initial state q 0 of M. In addition, the states are defined by the rows of Γ S . However, due to the second level abstraction, not all observed outputs are represented in the row γ S ∈ Γ S . To consider these outputs in the hypothesis, we have to check

Algorithm 2 Hypothesis construction

Input: abstract obs. table

T A = Γ = Γ S ∪ Γ P , E, T, T A , µ , input alphabet Σ A I Output: ONFSM M = Σ A I , Σ A O , Q, q0, h 1: function ConstructHypothesis 2: q0 ← ∈ Γ S 3: Q ← Γ S

4:

for all γ S ∈ Γ S do 5:

Qγ S ← {γ|γ ∈ Γ ∧ γ ∼ = A γ S }

6:

for all γ ∈ Qγ S do

7:

for all i ∈ Σ A I do

8:

for all o ∈ T (γ, i) do 9:

γ ← γ • (i, o) 10: if γ ∈ Γ then 11: h ← h ∪ (γ S , i, o, γ S ) where γ S ∈ Γ S ∧ γ S ∼ = A γ return M
also the observations in the mapping T . For this, we filter in Line 5 the equal rows of γ S in Γ according to the second level abstraction and then add all transitions with the corresponding observations in the Lines 6 to 11. In Line 9 we concatenate the currently considered sequence γ with the observed input/output pair. If this sequence is part of Γ , we have to find the correct destination state of the transition. For this, we select the equal state according to the second level abstraction in Γ S . In Line 11, we add the new transition to the transitions h. Example 6 (Hypothesis Construction). Table 5 and Table 6 are used to construct a hypothesis of Example 1. The closed, complete and consistent Table 6 identifies the states and Table 5 contains all observed outputs. Γ S includes two states {q 0 , q 1 }. From the initial state q 0 we create one transition q 0 Connect/Ack -------→ q 1 . In the second state we consider three different outputs, {Ack, Closed, Closed All}, where Closed and Closed All belong to the equivalence class Closed. Therefore, we create three different edges q 1 Connect/Closed All -----------→ q 0 , q 1 Connect/Closed ---------→ q 1 and q 1

Connect/Ack -------→ q 1 . The hypothesis is equal to the ONFSM shown in Fig. 3. Conformance Testing After the construction of the hypothesis (Algorithm 1, Line 16), we have to check in Line 17 whether our constructed hypothesis conforms to the SUT. Usually, in automata learning we assume that two systems are equal if the behavior of the learned hypothesis and the SUT are equal. For an ONFSM we could say that two systems are equal if all observable traces are equal. However, due to our second level abstraction, the learned model has a more generic behavior than the SUT. Therefore, the trace equivalence assumption does not hold. Instead we have to check trace inclusion, i.e., every trace produced by the SUT must also be observable in our learned hypothesis. Let I be our SUT and H the learned hypothesis. Further we define the function Traces(M) that returns all observable traces, starting at the initial state q 0 of an ONFSM M. The generated traces contain input and output symbols on the first level abstraction. Formally, we can define the conformance relation as follows:

Traces(I) ⊆ Traces(H). (1)
This relations implies that the more generic the hypothesis the better the conformance. However, a completely generic model would not be useful, e.g. for further testing purposes. The learning of a too generic hypothesis is prevented by the mere consideration of observed outputs from the observation table. Therefore, the hypothesis only includes outputs that can be observed on the SUT. According to the framework depicted in Fig. 1, the teacher either responds yes if the conformance relation in Eq. 1 is fulfilled or reports a counterexample. The counterexample is a trace that contains an output that is not included in our hypothesis H. Note that since the model is input-enabled only outputs may lead to the violation of trace inclusion. We replace the conformance oracle by conformance testing to make the conformance check feasible. For this, a finite number of test cases is generated and then executed on the SUT. Since the test cases contain inputs and outputs on the first level abstraction, we again need a mapper that abstracts and concretizes inputs and outputs for the execution on the SUT. A test case passes if the trace generated by the SUT is also observable in the hypothesis, otherwise the test case fails. Therefore, the teacher answers with yes, if all traces pass, otherwise a failing trace is returned. In Algorithm 1 Line 17 the return of an empty sequence is equal to the answer yes. A practical implementation of the conformance testing approach is discussed in Sect. 4.

If no counterexample is found our algorithm terminates and returns the current hypothesis in Line 21, otherwise we add the counterexample to the observation table in Line 19. Note that every returned counterexample is cut off after the first non-conforming input/output pair.

The adding of a counterexample in Line 19 distinguishes two different types of counterexamples. The first type reveals an unobserved output in a state of the hypothesis where an output of the same equivalence class is also observable. To check if the counterexample belongs to this type, we execute all input/output pairs except the last one of the sequence on H. This leads us to the failing state prior to the wrong observation. We then check if executing the remaining input generates an output of the same equivalence class. If the output is in the same equivalence class, we want to add the missing input/output transition to the state. In this case, we add any not already existing prefix of the found counterexample to Γ P . The second type of a counterexample reveals an input/output pair, where no equivalent output is observable in the failing state. In this case, we perform the counterexample processing as proposed by El-Fakih et al. [START_REF] El-Fakih | Learning finite state models of observable nondeterministic systems in a testing context[END_REF], since we want to introduce a new state in our hypothesis. This is done by firstly removing the longest matching prefix γ ∈ Γ of the counterexample and secondly adding the suffixes of the remaining input sequence of the found counterexample to E. In both cases, we then jump back to Line 3 and continue to fill the observation table by asking membership queries. This procedure is repeated until no counterexample can be found.

Case Study

We evaluated the Message Queuing Telemetry Transport (MQTT) protocol. MQTT defines a publish/subscribe protocol, where clients can subscribe to topics and publish messages to a topic. Tappler et al. [START_REF] Tappler | Model-based testing IoT communication via active automata learning[END_REF] already presented work on model-based testing of the MQTT protocol via active automata learning. However, in their work they only consider one or two clients interacting with the broker. Due to the proposed abstraction technique used in our learning algorithm for ONFSMs, we can deal with a multi-client setup. In this section, we first discuss technical aspects of the implementation of our learning algorithm and then present the results of the case study on five different MQTT brokers.

We weaken the all-weather assumption [START_REF] Milner | A Calculus of Communicating Systems[END_REF] for the observation of outputs, and assume like other learning algorithms for non-deterministic systems [START_REF] Pacharoen | Active learning of nondeterministic finite state machines[END_REF][START_REF] Khalili | Learning nondeterministic mealy machines[END_REF][START_REF] Volpato | Approximate active learning of nondeterministic input output transition systems[END_REF] that all outputs are observable after performing a query n times. Regarding the challenge that not all outputs are observable at once, we discuss three technical aspects of our implementation: (1) repeated execution of output queries, (2) stopping criterion for output queries, and (3) shrinking of the observation table.

(1) We need to repeat an output query since the abstraction done by the mapper introduces non-determinism. The mapper takes an abstract input and randomly chooses an input from a set of corresponding concrete inputs. Therefore, the observed outputs may differ. The number of repetitions n q ∈ N depends on the SUT, e.g. for the multi-client setup on MQTT we executed each query at least as often as the number of used clients.

(2) Repeating every output query each time the table is filled leads to a vast amount of queries. In practice, performing queries on the SUT can be expensive, e.g. due to the latency of the response. Thus, we want to reduce the number of performed queries. In our implementation, we extended each cell of the observation table by a score s ∈ R ≥0 that indicates how often the outputs in the cell change. The value of s is between 0.0 and 1.0, and each time we perform the output queries and no new output is observed, s increases by a value s i ∈ R ≥0 . If at least one new output is observed, the score decreases by s d ∈ R ≥0 . Note that s cannot increase above 1.0 and decrease below 0.0. If s = 1.0, we do not perform the output query again. The initial value of s and the values of s i and s d depend on the SUT and how often output queries are repeated in general.

(3) The size of the observation table significantly influences the runtime of the learning algorithm. Our abstraction techniques keep the size of the observation table small. However, due to the assumed non-determinism, it may happen that rows become equal after repeating output queries. For this, we remove equal rows in Γ S and the corresponding suffixes in Γ P . The shrinking of the table is performed before the closedness, consistency and completeness check.

In Sect. 3.4, we explained that the equivalence oracle is replaced by conformance testing. Due to our conformance relation defined in Eq. 1, we cannot check if the outputs of all traces are equivalent, since our hypothesis is more generic than the SUT. We generate input sequences by randomly walking through the hypothesis model. The random walk selects outgoing transitions from the current state uniformly at random and append the input of the transition to the input sequence. This input sequence is then executed once on the SUT to generate an input/output sequence. We then check if the generated sequence is observable on our hypothesis. When we execute the input sequence on the SUT, we use the mapper to translate the abstracted inputs to concrete inputs. Since the number of possible concrete inputs is extremely large and executing all possible inputs would be infeasible, we limit the number of executed test cases to a finite number n test ∈ N. Due to the assumption of non-deterministic behavior, we may observe different sequences if we repeat the execution on the SUT. Instead of repeating each input sequence several times, we assume that the generation via random walk reflects the non-deterministic behavior sufficiently.

In this case study, we learned the ONFSMs of MQTT brokers. In the MQTT protocol, a client can connect to a broker. A connected client can subscribe to a topic and/or publish a message on a topic, which is then forwarded by the broker to the subscribed clients. The task of the MQTT broker is to handle the connection/disconnection of the clients and to forward publish-messages to subscribed clients. The five learned MQTT brokers are listed in Table 7. All of them implement the current MQTT standard version 5.0 [14]. To communicate with the different brokers, we used our own client implementation. We used an akin learning setup for all five MQTT brokers. The goal was to learn the behavior of the MQTT broker that interacts with multiple clients.

In our experiments, we used five clients. We defined the abstract input alphabet by Σ A I = {Connect, Disconnect, Subscribe, Unsubscribe, Publish}. The mapper translates each abstract input to a concrete input for one of the five clients. Furthermore, the clients can subscribe to one topic and publish a message to this topic. For the second level abstraction we defined the following mapping µ for the equivalence classes {Closed, Closed all, Closed Unsuback all} → Closed, {Unsuback, Unsuback all} → Unsuback, and all other outputs map to an equally named singleton equivalence class. To make the approach feasible for a large number of clients, our mapper saves translations from the abstract sequences in Γ to sequences with concrete input/output values, i.e., we cache concrete input/output sequences of the sequences in Γ . For each of these saved translations, we repeat the output query times the number of clients. Using this querying technique, we assume that we do not frequently observe new outputs when we repeat the output queries. Therefore, we set the change indicator s = 0.9, s i = 0.2 and s d = 0.1. Furthermore, we assume that 2 000 input/output sequences sufficiently represent this system. Thus, we set n test = 2 000.

Figure 5 represents the learned ONFSM of an MQTT broker interacting with multiple clients. The symbol "+" represents a wildcard for several inputs or outputs that are not critical for the behavior system and, therefore, are skipped to keep the model clear. The three states of the MQTT model distinguish between the state where no client is connected (q 0 ), at least one client is connected, but no client is subscribed (q 1 ) and at least one client is connected and subscribed (q 2 ). Note that Fig. 5 represents a valid model for all setups where more than two clients interact with the MQTT broker.

Table 7 shows the learning setup and the results of our case study. The first three rows of the table define the MQTT broker, the tested version and the required timeout on responses. The timeout defines the duration how long (in milliseconds) the socket listens for incoming messages. An equal behavior of the five brokers could only be achieved by the adaption of the timeouts. Selecting a too low timeout, we may not receive all messages in time. Our proposed learning algorithm can deal with such a non-deterministic behavior. For example, when we learn the HiveMQ broker with a timeout of 50, we receive messages from old sessions or some messages are not delivered in time. Therefore, we set the timeout for the brokers individually. The last three rows of Table 7 represent the learning results which state the number of performed output queries and equivalence queries, and the required time to learn the MQTT broker. The timeout directly affects the runtime of the learning algorithm, which can be seen in the experiments for ejabberd and HiveMQ. The experiments were conducted with a MacBook Pro 2019 with an Intel Quad-Core i5 operating at 2.4 GHz and with 8 GB RAM. All learned models correspond to the ONFSM presented in Fig. 5. Furthermore, we compared our algorithm with a deterministic learning algorithm. For this, we learn a deterministic model of the MQTT broker that interacts with five clients. The experiment was performed with the tool Learn-Lib [START_REF] Isberner | The open-source LearnLib -A framework for active automata learning[END_REF] using the improved version of L * proposed by Rivest and Schapire [START_REF] Rivest | Inference of finite automata using homing sequences[END_REF]. We only learned the model for the Mosquitto broker with a timeout of 50, all other brokers of Table 7 showed non-deterministic behavior during learning. The learning of the Mosquitto broker for five clients took more than two days (58.29 h). The final model had 243 states and 6 075 transitions. The model size shows that even if we learn a small part of a rather simple system the complexity of the system increases significantly in a multi-client setup. To learn the deterministic model, 151 900 output queries and one equivalence query were required. These results stress that our algorithm enables a faster learning-based testing technique and provides a simpler model of a large system.

Related Work

Our proposed learning algorithm for ONFSM is based on Angluin's L * [4]. In the literature, the majority of learning algorithms for non-deterministic systems [START_REF] Bollig | Angluin-style learning of NFA[END_REF][START_REF] El-Fakih | Learning finite state models of observable nondeterministic systems in a testing context[END_REF][START_REF] Pacharoen | Active learning of nondeterministic finite state machines[END_REF][START_REF] Khalili | Learning nondeterministic mealy machines[END_REF][START_REF] Volpato | Active learning of nondeterministic systems from an ioco perspective[END_REF][START_REF] Volpato | Approximate active learning of nondeterministic input output transition systems[END_REF]] also follows the same principle. Bollig et al. [START_REF] Bollig | Angluin-style learning of NFA[END_REF] introduced a learning algorithm for residual finite-state automata, which are a subclass of nondeterministic finite automata. Using this modeling formalism, they can represent a deterministic finite-state automaton by a more succinct non-deterministic automaton. However, they assume that the SUT behaves deterministically.

All Angluin-based algorithms for ONFSMs [START_REF] El-Fakih | Learning finite state models of observable nondeterministic systems in a testing context[END_REF][START_REF] Pacharoen | Active learning of nondeterministic finite state machines[END_REF][START_REF] Khalili | Learning nondeterministic mealy machines[END_REF] basically follow the approach that was first proposed by El-Fakih et al. [START_REF] El-Fakih | Learning finite state models of observable nondeterministic systems in a testing context[END_REF]. Their algorithm is based on the all-weather assumption, i.e. all possible outputs are observable at once. Pacharoen et al. [START_REF] Pacharoen | Active learning of nondeterministic finite state machines[END_REF] revise this assumption by assuming that all outputs are observed, after executing a query n ∈ N times. Kahlili and Tacchella [START_REF] Khalili | Learning nondeterministic mealy machines[END_REF] also considered more practical aspects and learned the non-deterministic model of TFTP server. However, as explained in Sect. 3 these algorithms might not scale well when an alphabet is abstracted by a mapper component.

Volpato and Tretmans [START_REF] Volpato | Active learning of nondeterministic systems from an ioco perspective[END_REF][START_REF] Volpato | Approximate active learning of nondeterministic input output transition systems[END_REF] introduced two learning algorithms for nondeterministic input/output labelled transition systems. In their first work [START_REF] Volpato | Active learning of nondeterministic systems from an ioco perspective[END_REF], they posed the all-weather assumption on the observation of outputs and assume an Angluin-style equivalence oracle. In their second work [START_REF] Volpato | Approximate active learning of nondeterministic input output transition systems[END_REF], they weakened these assumptions and proposed a conformance relation based on the iocotheory [START_REF] Tretmans | Test generation with inputs, outputs and repetitive quiescence[END_REF] for an over-and under-approximation of the SUT. In contrast to our algorithm, they try to improve the observation table by increasing it, which leads to more states like in the previously mentioned algorithms for ONFSMs.

Petrenko and Avellaneda [START_REF] Petrenko | Learning and adaptive testing of nondeterministic state machines[END_REF] proposed an algorithm for ONFSM that is not based on Angluin's MAT framework. Instead of a teacher they create a hypothesis using a SAT solver. However, the algorithm is based on the assumption that the final number of states of the ONFSM must be known in advance.

Tappler et al. [START_REF] Tappler | L * -based learning of Markov decision processes[END_REF] presented an L * -based learning algorithm for Markov decision processes. For this, they also considered the observed frequencies of stochastic events in their models. Their algorithm rather learns the stochastic behavior instead of the non-deterministic behavior like our algorithm.

Conclusion

We presented an active automata learning algorithm for observable non-deterministic finite state machines. Unlike previous work on L * -based algorithms for ONFSMs, our algorithm learns a more abstract model of the SUT by merging akin states. For this, we defined two levels of abstraction and explained how to combine them. Firstly, we showed how the mapper component proposed by Aarts et al. [2] can be used in an active learning setup for ONFSMs. Secondly, to further improve the scalability of our learning algorithm, we introduced a new abstraction scheme for the observation table based on equivalence classes for outputs. This abstraction technique made it possible to learn a more abstract model of a system that has a large input/output alphabet. We showed the applicability of our implementation by learning the ONFSMs of different MQTT brokers that interact with multiple clients.

Our proposed learning algorithm offers a more feasible technique to apply learning-based testing in a broader field of applications. For future work, it would be interesting to show a more elaborated case study, e.g. considering more features of the MQTT protocol, so that our abstract model can reveal unexpected behavior of the SUT. Currently, the abstraction refinement relies on expert knowledge, but we assume that an automatic abstraction is possible. Aarts et al. [START_REF] Aarts | Automata learning through counterexample guided abstraction refinement[END_REF] proposed an automatic abstraction refinement for the abstracted input/output alphabet that ensures deterministic learning. Following a similar idea, we could refine the outputs for the first level-abstraction to ensure observable non-determinism. Regarding the second level abstraction, an equivalence measurement for states could support the definition of equivalence classes.

Fig. 3 .

 3 Fig. 2. Abstracted nondeterministic Mealy machine of the MQTT connection protocol

Fig. 4 .

 4 Fig. 4. Learned model of Example 1 without second level abstraction, which has n + 1 states for n clients.

Table 1 .

 1 Observation table of the multiclient connection protocol of Example 1.

	Γ \E	Connect
		Ack
	(Connect, Ack)	Ack, Closed All
	(Connect, Ack)(Connect, Ack)	Ack, Closed
	(Connect, Ack)(Connect, Closed All)	Ack

Table 2 .

 2 Abstracted observation table of

Table 1 .

 1 Ack)(Connect, Closed All) Ack the first level abstraction might not be enough to keep the number of states low. To overcome this problem, we introduce a second level abstraction. The aim of this abstraction level is to decrease the state space by defining equivalent outputs. This is done by the definition of equivalence classes for outputs, which then replace the observations saved in the observation table. The mapping of the equivalence classes is a surjective function µ :Σ A O → Σ A O thatmaps an abstracted output of Σ AO to an equivalence class of Σ A O . Example 2 (Multi-Client Connection Equivalence Classes). Even though we abstracted the alphabet in Example 1, learning algorithms for ONFSMs, e.g. L N[START_REF] El-Fakih | Learning finite state models of observable nondeterministic systems in a testing context[END_REF], would learn a model similar to the one shown in Fig.4. The problem is that these algorithms count the number of clients, and create a new state for each client. To avoid a large model, we want to merge akin states. For this, we define for the outputs Σ A

	Γ \E	Connect
		Ack
	(Connect, Ack)	Ack, Closed
	(Connect, Ack)(Connect, Ack)	Ack, Closed
	(Connect,

O = {Ack, Closed, Closed All} the following equivalence classes Σ A O = {Ack, Closed}. The function µ for the second level abstraction of this example is defined as follows µ : {Ack} → Ack, {Closed, Closed All} → Closed.

Table 3 .

 3 Observation table of Example 1 after the first output queries.

	Γ \E	Connect
		Ack
	(Connect, Ack) Ack, Closed All

Table 4 .

 4 Abstraction of Table 3 using the mapping defined in Example 2

	Γ \E	Connect
		Ack
	(Connect, Ack) Ack, Closed

Table 2 -

 2 and check if the abstracted table is closed. Our closed check on Table 2 is now satisfied. Note that we do not bother that Table 1 is not closed.

Table 5 .

 5 Final observation table of the connection protocol of Example 1. The input Connect is abbreviated by Conn.

	Γ \E	Conn
		Ack
	(Conn, Ack)	Ack, Closed All
	(Conn, Ack)(Conn, Ack)	Ack, Closed
	(Conn, Ack)(Conn, Closed All)	Ack
	(Conn, Ack)(Conn, Ack)(Conn, Closed) Ack, Closed All

Table 6 .

 6 Final abstracted observation table generated from Table 5 The input Connect is abbreviated by Conn. The sequences pre(γ • (e, s + O )) are added to Γ P , if the sequence is not already part of Γ . Therefore, Γ P only contains sequences that are added to fulfill the completeness of the abstracted observation table. Example 5 (Complete Abstracted Observation Table). We continue the learning procedure of Example 4 by checking if the observation table is complete. For this, we consider Table 1 and the abstracted Table 2. We see that the row (Connect, Ack) is equal to (Connect, Ack), (Connect, Ack) in the abstracted table. However, in Table 1 we see that the outputs Closed All and Closed are different. Hence, we add the sequence (Connect, Ack), (Connect, Ack), (Connect, Closed) to the classic observation table

	Γ \E	Conn
		Ack
	(Conn, Ack)	Ack, Closed
	(Conn, Ack)(Conn, Ack)	Ack, Closed
	(Conn, Ack)(Conn, Closed All)	Ack
	(Conn, Ack)(Conn, Ack)(Conn, Closed) Ack, Closed

Table 7 .

 7 Learning setup and results of our case study on MQTT brokersBroker ejabberd 1 EMQ X 2 HiveMq 3 Mosquitto 4 VerneMQ 5

	Version	20.3	v4.0.0	2020.2	1.6.8	1.10.0
	Timeout	100	50	100	50	50
	# Output Queries	18 315	18 375	15 950	13 975	14 800
	# Equivalence Checks	1	1	1	1	1
	Runtime (h)	11.28	5.48	9.04	3.98	4.30

  Fig. 5. The ONFSM of an MQTT broker that interacts with multiple-clients.

		Connect/Closed all Disconnect/Closed all
		Connect/Connack	Publish/Puback Publish
		Connect/Connack	Publish/Puback Subscribe/Suback	Subscribe/Suback
	q0	q1		q2
		Connect/Closed all	Unsubscribe/Unsuback all	+/+
	+/Closed all	Disconnect/Closed all +/Closed, Unsub all	Unsubscribe/Unsuback
			Conclosed/Closed Unsuback all

https://www.ejabberd.im/

https://www.emqx.io/

https://www.hivemq.com/

https://mosquitto.org/

https://vernemq.com/

Acknowledgment. This work is supported by the TU Graz LEAD project "Dependable Internet of Things in Adverse Environments". We would like to thank student Jorrit Stramer for the implementation of the MQTT client.