The de nition of a formal speci cation is a fundamental step in the design of safety-critical systems. The speci cation de nes the behaviors and constraints that the system under development is required to satisfy. Depending on the system dimension, the speci cation can be used to verify its correctness or the correctness of its abstract model. In some cases, the system can also be directly synthesized from the speci cation. However, when the system is too complex for a full veri cation or for synthesis, developers usually rely on testing to demonstrate the correct operation of the system. In this paper we present our ongoing work on automatic test cases generation, relying on Linear Temporal Logic (LTL) as a speci cation formalism. The presented algorithm is implemented in SpecPro, our library for supporting analysis and development of formal requirements in cyber-physical systems.
In the context of reactive systems, i.e., systems that maintain an ongoing interaction with the environment and react to external stimuli, it is important to check the correctness of their behavior over time. Formal veri cation techniques provides a viable solution to automatically check the system against a given speci cation, greatly increasing the con dence of their correctness. However, these techniques su er of known scalability issues and the complete veri cation of the speci cation becomes impractical or even impossible for complex systems. For this reason, testing is the preferred technique for hardware and software veri cation in industry, although it provides less guarantees; testing can only detect the presence of errors, not their absence. Nonetheless, a formal speci cation can still be of great practical use to automatically generate test suites to show conformance of the model and the actual implementation, or, just to derive \interesting" test cases to check the developed system [2].
In this paper, we present a new algorithm to automatically extract a test suite from the requirement speci cation, giving the user a tool to systematically ? The research of Simone Vuotto has been funded by the EU Commission's H2020
Programme under grant agreement N.732105 (CERBERO). analyze the behaviors described in the speci cation and to put them to work in the subsequent phases. In order to extract test cases from requirements, different requirement-based coverage metrics have been proposed in the literature, although they usually rely on a complete model of the system for test generation (see [6] for a survey of available methods). In particular, the proposed approach takes inspiration from [13], a linear temporal logic (LTL) [11] speci cation-based test-case generation methodology, and extend our previous work in [12].
Compared to [13], where a di erent automaton is built and checked against the model for each behavior, we build a single automaton representing all behaviors of the speci cation and we traverse it in order to extract valid test cases. This approach frees us from the need of a model, but we require a complete speci cation to be known in advance. In this regard, we are more closely related to the synthesis problem, but we limit our scope to the generation of a limited set of behaviors that the nal system should implement, and we do not aim at synthesizing the whole system. With respect to [12], we propose a di erent exploration strategy of the automaton and we introduce the concept of input and output sequences, that are used to generate the test cases. Finally, the proposed algorithm is implemented in the SpecPro open-source library, along with other features, such as the consistency checking of requirements and the identi cation of inconsistent minimal sets thereof [9, 10].
The rest of the paper is organized as follows. In Section 2 we present some basic notions and de nitions that are used in Section 3 to describe the proposed algorithm. Section 4 presents the experiments we made to illustrate how the algorithm works and to evaluate the generated test suite. Finally, Section 5 concludes the paper with some nal remarks. 2
LTL formulae consist of atomic propositions AP , Boolean operators, and temporal operators. The syntax of a LTL formula is given as follows: = > j ? j a j : 1 j 1 _ 2 j X 1 j 1 U 2 j ( ) where a 2 AP , ; 1; 2 are LTL formulae, X is the \next" operator and U is the \until" operator. We also consider other Boolean connectives like \^" and \!" with the usual meaning and the temporal operators (\eventually") to denote > U and (\always") to denote : : . In the following, unless speci ed otherwise using parentheses, unary operators have higher precedence than binary operators. Brie y, the semantics of an LTL formula yields a !language Words( ) of in nite words satisfying , i.e., in nite sequences over the 2AP alphabet (see [1] for a full description).
De nition 1 (Non Deterministic Buchi Automaton). A non deterministic Buchi Automaton (NBA) A is a tuple A = (Q, , , q0, F ) where Q is a nite set of states, is an alphabet, : Q ! 2Q is a transition function, q0 2 Q is the initial state, and F Q is a set of accept states, called acceptance , can be rewritten as : q !A q0. set. ! denotes the set of all in nite words over the alphabet . We denote = A0A1A2 : : : 2 ! one such word and [i] = Ai for the i-th element of . For sake of simplicity, the transition relation q0 2 (q,A) where q, q0 2 Q, and A 2 notation for the three transitions qi !a qi+1, qi a!;b qi+1, qi !b qi+1 In Figure 1 is presented an example of Buchi Automaton, where Q = f0,1,2,3g, = 2fa;b;cg, Q0 = f0g, F =f1g, and transition of the form qi a_!b qi+1 is a short
De nition 2 (Run). A run for a NBA A = (Q, , , q0, F ) is a an in nite sequence %= q0q1q2::: of states in A such that q0 is the initial state and qi+1 2 (qi; Ai) for some Ai 2 . Given a run %, we de ne Words(%) the set of words that can be produced following the transitions in %.
De nition 3 (Induced Run). Given a word , a run % is said to be induced by , denoted ` %, i qi+1 2 (qi; [i]) for all i 0.
De nition 4 (Accepting run). A run % is accepting if there exist qi 2 F such that qi occurs in nitely many times in %. We denote acc(A) the set of accepting runs for A.
De nition 5 (Lasso-Shaped run). A run % over a NBA A = (Q, , , q0, F ) is lasso-shaped if it has the form %= ( )!, where and are nite sequences over the states Q. A lasso-shaped run is also accepting if \ F 6= ;.
The length of % is de ned as j%j= j j + j j, where j j (resp. j j) is the length of the nite sequence of states (resp. ).
De nition 6 (!-language recognized by A). A !-language L(A) of a NBA A = (Q, , , q0, F ) is the set of all in nite words that are accepted by A. A wAoirndduc2ed b!y is.aFcocerpmtaedllyb,yLA(Ai) =thefre 2exis!tsja9n% a=ccep(ti)n!g:%la2ssaoc-sch(Aap)e^d ru`n %%go.f Transition System A transition system T is a tuple (T; t0; ) where T is a nite set of states, t0 is the initial state and : T 2I ! 2O T is the transition function. The sets I and O are a partition of the atomic propositions AP that are controllable by the environment and by the system respectively. The transition function maps a state t and a valuation of the inputs i 2 2I to a valuation of the outputs, also called labeling, and a next state t0. If the labeling produced by (t; i) is independent of i, we call T a state-labeled (or Moore) transition system and transition-labeled (or Mealy) otherwise. Most of the state of the art tools for reactive LTL synthesis, such as ACACIA+ [5], STRIX [8] or BOSY [4] use Mealy Machines to describe the reactive systems synthesized.
Given an in nite word i0i1 2 (2I )! over the inputs, T can be traversed applying (tj ; ij ) = (oj ; tj+1) for every j 0. The application of for every input ij , starting from t0, produces an in nite trace (t0 [ i0 [ o0)(t1 [ i1 [ o1) 2 (2T [I[O)!. The projection of a trace to the atomic propositions is a path w 2 (2I[O)!. We denote the set of all paths generated by a transition system T as P aths(T ). A transition system realizes an LTL formula ' if P aths(T ) L('). 3
In this section, we describe a new methodology to automatically generate a set of test cases from a given LTL speci cation. We rst give a general overview of the algorithm along with an example, and then in subsections 3.1 and 3.2 we describe the way we select input and output sequences respectively.
The algorithm, shown in Algorithm 1, takes in input a Buchi Automaton A of and the sets I and O of input and output atomic propositions, respectively, such that I [ O = AP and I \ O = ;. In the general case of multiple LTL requirements 1; : : : ; n, is build as a conjunctive formula = 1 ^ ^ n, while for a speci cation in TLSF [7] format, the formula is built with the SyFCo tool. The Buchi Automaton of the formula is built with Spot [3] v2.7.5 tool. The algorithm is divided into two steps: (i) we extract a set Is of suitable input sequences; (ii) for each input sequence i we compute one or more output sequences that have to be checked for input i.
Algorithm 1 Test Case Generation 1: function generate(A ; I; O) 2: T s ; 3: Is findInputSequences(A ; I) 4: for i 2 Is do 5: Os selectOutputs(A ; i; O) 6: T s T s [ f( i; Os)g 7: end for 8: return T s 9: end function
The distinction between input and output sequences is needed because of the intrinsic non-determinism normally allowed by a LTL speci cation. In fact, a speci cation usually describes a (possibly in nite) range of allowed sequences. The situation is even worst if the system is under-speci ed, i.e., the behavior of the atomic propositions is loosely restricted.
For example, consider the formula = (q ! r), meaning that every query q must be followed by a response r. In this case q is an input variable and r is an output variable. The corresponding NBA is depicted in gure 2. Now, let's consider a three steps input sequence = [fqg; fqg; fqg], where q is true only in the second step. If we check all possible pre xes of length 3 that are in Words( ), given the assignment of q xed by , we see that multiple solutions are possible. [fqrg; fqrg; fqrg] is such a solution, and so are [fqrg; fqrg; fqrg] and [fqrg; fqrg; fqrg]. Also the sequence [fqrg; fqrg; fqrg] is accepted by the language, where r is always true no matter what's the behavior of q. Finally, also the sequence in which r is always false is a valid pre x, because if extended can lead to words in which is eventually satis ed. However, the transition system realizing such requirement, will eventually implement only one of such behaviors. Therefore, we need to keep track of the relation between these words. In this context, we consider a test case to be successful if applying the input sequence to the system under test, the generated output is contained in the set of allowed output sequences. Algorithm 2 shows the steps implemented to nd the set of input sequences. After the initialization of the Is and visited sets, the function generateFilteredBA (line 4) returns AI , a ltered version of the given automaton. The new automaton AI has the same set of states Q, initial state q0 and acceptance set F of A , but the alphabet I = 2I and the transition function I = (q; A \ I) 8A 2 ; q 2 Q are built from the input atomic propositions I only. The resulting language L(AI ) is therefore more abstract then L(A ) and contains only words with input variables. The new automaton is therefore explored with the following strategy: { for each state q in AI , we check every outgoing transition not yet explored (i.e., not traversed by an already generated sequence) that lead to a new state q0; { for every such transition (q; q0) a run is built in the following way: the shortest path (computed with the function sp at line 9 of Algorithm 2) from q0 to q is concatenated to the shortest path to go from q0 to the nearest acceptance state q (computed at line 8, with a classical breadth- rst search strategy, within function findNearestAcceptanceState); { we extract a word from (line 10), we add it to the set of input sequences (line 11) and we mark each transition in as visited (lines 12-14).
At the end of the process, we have a set Is of input sequences, computed from the exploration of each state and transition of the automaton. The procedure is built with three goals in mind: (i) exercise every behavior contained in the automaton at least once; (ii) maintain the number of sequences small; and (iii) keep the sequences as short as possible. Finally, before returning the set of sequences, we call the reduce function that remove the sequences that are prexes of other ones. For instance, if both 1 = [frg; frg] and 2 = [frg; frg; frg] are generated, 1 can be removed because it is a pre x of 2. 3.2
Select Outputs As mentioned before, for each input sequence i, there could be one or more associated output sequences that the system can implement in order to ful ll the speci cation. In this section we analyze more in details how to select these sequences. First, remember that the sequences we are seeking to extract are words accepted by the automaton A over the alphabet = 2AP , namely the power set of all the atomic propositions in . A simple strategy could be to use the input sequence i as a word of the automaton to nd all induced runs, according to De nition 7 given in Section 2, and then use these runs to extract all accepted words. However, the problem with this de nition is that it is intended for words that share the same alphabet of the automaton, while in this case i is de ned over the alphabet I . Therefore, we modify the notion of induced run over input sequences as follow: De nition 7 (Input Induced Run). Given a NBA A = (Q, , , q0, F ), with = 2I[O, and an input word de ned over the alphabet I = 2I , a run % is said to be input induced by , denoted `I %, i qi+1 2 (qi; A) : A \ I = [i] for all i 0.
With this new de nition, we can now implement Algorithm 3. For each induced run, computed relying on the de nition above, we check if they are lasso shaped and accepting (line 5). If they are, we extract the corresponding words and we lter them out (lines 6-9) so that they only contain output variables. The generated words are inserted in Os (line 10) and nally returned (line 14) when all runs have been evaluated.
Algorithm 3 Select Output Sequences for input i from A
As a nal remark, Algorithm 3 computes for each input sequence i all the corresponding lasso-shaped accepting output sequences of length j ij. On the one hand, it could be possible to produce more output sequences, extracting longer runs or weakening the lasso-shaped accepting condition. On the other hand, one could also think to further reduce this set, ltering it out with some heuristics. For example, we could take into account only the runs that visit acceptance states more often, or the ones that reach an acceptance state rst.
Let us start our experimental evaluation by introducing the following specication as our running example, with I = frequest 0; request 1g and O = fgrant 0; grant 1g being the set of input and output variables, respectively: (:grant 0 _ :grant 1) :grant 0 W (request 0 ^ :grant 0) :grant 1 W (request 1 ^ :grant 1) (request 0 ! grant 0) (request 1 ! grant 1) ((grant 0 ^ :request 0) ! ( :grant 0)) ((grant 0 ^ X (:request 0 ^ :grant 0)) !
X (:grant 0 W (request 0 ^ :grant 0))) ((grant 1 ^ :request 1) ! ( :grant 1)) ((grant 1 ^ X (:request 1 ^ :grant 1)) !
X (:grant 1 W (request 1 ^ :grant 1)))
(
The speci cation describes the full arbiter of two clients; it eventually issues
a grant for each client if they send a request (see formulae (
Given the above speci cation, the algorithm described in Section 3 generates the 30 tests cases presented in Table 1. The rst column shows the generated input sequences (for the sake of space, request 0 and request 1 are replaced with r0 and r1 respectively) and the second column reports, for each input sequence, the corresponding number of generated output sequences. Notice that the output sequences are lasso-shaped; therefore, we could extend each test sequence inde nitely. However, each test must be nite, so we repeat the recurrent part of the lasso-shaped sequence only once.
In order to evaluate the e ectiveness of the generated test suite, we used Strix [8] to synthesize a Mealy Machine from the same speci cation and we run the generated tests on it. A representation of the synthesized transition system is depicted in Figure 3. Out of the 30 test cases, 23 of them were successful, i.e., the output sequence produced by the transition system was in the set of output sequences generated by the algorithm, while 7 tests failed. Analyzing the failed tests, we observe two phenomena. First, let's consider the case with input sequence 1i = [fr0; r1g; fr0; r1g; fr0; r1g; fr0; r1g]. The only generated output is 1o = [fg0; g1g; fg0; g1g; fg0; g1g; fg0; g1g] (where g0 and g1 stand for grant 0 and grant 1, respectively). On the other and, if we run 1i on the transition system in Figure 3, we see that it visits states S0, S1, S5, S7 and S4, and produces the output sequence ^1o = [fg0; g1g; fg0; g1g; fg0; g1g; fg0; g1g]. ^1o is a perfectly valid output sequence, recognized by the language, and the system behaves as we expect. In this case, the algorithm produced a too narrow set of output sequences and failed to nd the implemented one. This is due to the lasso-shaped condition and the limit on the sequence length, as explained at the end of Section 3. A less restrictive condition or a longer input sequence would have allowed the algorithm to nd the expected output. Now, let's consider the input sequence 2i = [fr0;r1g;fr0;r1g;fr0;r1g;fr0;r1g]. The expected output is 2o = [fg0;g1g;fg0;g1g;fg0;g1g;fg0;g1g]. Running 2i on the synthesized system, the system visits states S0, S2, S7, S1 and S4, and it outputs ^2o = [fg0;g1g;fg0;g1g;fg0;g1g;fg0;g1g]. In this case we see that the system has a strange behavior, because it keeps g0 active for two steps even if it is not needed. Although the speci cation does not forbid this behavior, and ^2o is a perfectly valid sequence, one may prefer to observe output 2o instead. In situations like this, having small sets of output sequences can be bene cial in identifying these subtle behaviors.
Finally, we report that the successful test cases were enough to cover all the
states of the synthesized transition systems and 87% of its transitions.
In this paper we presented an extension of our previous work [12] on
automatabased test generation. In particular, we propose a new framework that splits
the test case generation problem in two parts: rst all input sequences are
computed, i.e., sequences containing only input atomic propositions, and then the
corresponding set of output sequences is selected from the automaton. We
presented an algorithm to carry on both these tasks, and we shown its e ectiveness
using the full arbiter speci cation in out experimental evaluation. The results
reported in Section 4 gave interesting insights into both the challenges as well as
the potentials of such approach. In particular, further work is necessary in
order to explore and evaluate di erent generation strategies and outputs selection
conditions. Concerning current and future work, our next steps will focus on (