=Paper=
{{Paper
|id=Vol-2457/paper10
|storemode=property
|title=Automata-Based Generation of Test Cases for Reactive Systems
|pdfUrl=https://ceur-ws.org/Vol-2457/10.pdf
|volume=Vol-2457
|authors=Simone Vuotto
|dblpUrl=https://dblp.org/rec/conf/cpsschool/Vuotto19
}}
==Automata-Based Generation of Test Cases for Reactive Systems==
https://ceur-ws.org/Vol-2457/10.pdf
Automata-Based Generation of Test Cases
for Reactive Systems ?
Simone Vuotto
1
Università degli Studi di Genova
simone.vuotto@edu.unige.it
2
Università degli Studi di Sassari
svuotto@uniss.it
Abstract. The definition of a formal specification is a fundamental step
in the design of safety-critical systems. The specification defines the be-
haviors and constraints that the system under development is required to
satisfy. Depending on the system dimension, the specification 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 specification.
However, when the system is too complex for a full verification 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 specification formalism. The presented algorithm is implemented in
SpecPro, our library for supporting analysis and development of formal
requirements in cyber-physical systems.
1 Introduction
In the context of reactive systems, i.e., systems that maintain an ongoing in-
teraction with the environment and react to external stimuli, it is important to
check the correctness of their behavior over time. Formal verification techniques
provides a viable solution to automatically check the system against a given
specification, greatly increasing the confidence of their correctness. However,
these techniques suffer of known scalability issues and the complete verification
of the specification becomes impractical or even impossible for complex systems.
For this reason, testing is the preferred technique for hardware and software
verification in industry, although it provides less guarantees; testing can only
detect the presence of errors, not their absence. Nonetheless, a formal specifica-
tion 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 specification, 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 specification and to put them to work
in the subsequent phases. In order to extract test cases from requirements, dif-
ferent 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] specification-based
test-case generation methodology, and extend our previous work in [12].
Compared to [13], where a different automaton is built and checked against
the model for each behavior, we build a single automaton representing all be-
haviors of the specification 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
specification 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 final system should implement, and we do not aim at
synthesizing the whole system. With respect to [12], we propose a different ex-
ploration 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 identification
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 definitions 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 final remarks.
2 Background
LTL formulae consist of atomic propositions AP , Boolean operators, and tem-
poral operators. The syntax of a LTL formula φ is given as follows:
φ = > | ⊥ | a | ¬φ1 | φ1 ∨ φ2 | X φ1 | φ1 U φ2 | (φ)
where a ∈ 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
specified otherwise using parentheses, unary operators have higher precedence
than binary operators. Briefly, the semantics of an LTL formula φ yields a ω-
language Words(φ) of infinite words satisfying φ, i.e., infinite sequences over the
2AP alphabet (see [1] for a full description).
Definition 1 (Non Deterministic Büchi Automaton). A non determinis-
tic Büchi Automaton (NBA) A is a tuple A = (Q, Σ, δ, q0 , F ) where Q is a
finite set of states, Σ is an alphabet, δ : Q × Σ → 2Q is a transition function,
q0 ∈ Q is the initial state, and F ⊆ Q is a set of accept states, called acceptance
set. Σ ω denotes the set of all infinite words over the alphabet Σ. We denote σ =
A0 A1 A2 . . . ∈ Σ ω one such word and σ[i] = Ai for the i-th element of σ. For
sake of simplicity, the transition relation q 0 ∈ δ(q,A) where q, q 0 ∈ Q, and A ∈
A
Σ, can be rewritten as : q − → q0 .
In Figure 1 is presented an example of Büchi Automaton, where Q = {0,1,2,3},
a∨b
Σ = 2{a,b,c} , Q0 = {0}, F ={1}, and transition of the form qi −−→ qi+1 is a short
a a,b b
notation for the three transitions qi −
→ qi+1 , qi −−→ qi+1 , qi →
− qi+1
Fig. 1. Büchi Automata example.
Definition 2 (Run). A run for a NBA A = (Q, Σ, δ, q0 , F ) is a an infinite
sequence %= q0 q1 q2 ... of states in A such that q0 is the initial state and qi+1 ∈
δ(qi , Ai ) for some Ai ∈ Σ. Given a run %, we define Words(%) the set of words
that can be produced following the transitions in %.
Definition 3 (Induced Run). Given a word σ, a run % is said to be induced
by σ, denoted σ ` %, iff qi+1 ∈ δ(qi , σ[i]) for all i ≥ 0.
Definition 4 (Accepting run). A run % is accepting if there exist qi ∈ F such
that qi occurs infinitely many times in %. We denote acc(A) the set of accepting
runs for A.
Definition 5 (Lasso-Shaped run). A run % over a NBA A = (Q, Σ, δ, q0 ,
F ) is lasso-shaped if it has the form %=α(β)ω , where α and β are finite sequences
over the states Q. A lasso-shaped run is also accepting if β ∩ F 6= ∅.
The length of % is defined as |%|= |α| + |β|, where |α| (resp. |β|) is the length
of the finite sequence of states α (resp. β).
Definition 6 (ω-language recognized by A). A ω-language L(A) of a NBA
A = (Q, Σ, δ, q0 , F ) is the set of all infinite words that are accepted by A. A
word σ ∈ Σ ω is accepted by A iff there exists an accepting lasso-shaped run % of
A induced by σ. Formally, L(A) = {σ ∈ Σ ω | ∃% = α(β)ω .% ∈ acc(A) ∧ σ ` %}.
Transition System A transition system T is a tuple (T, t0 , τ ) where T is a finite
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 ∈ 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 infinite word i0 i1 · · · ∈ (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 infinite trace (t0 ∪ i0 ∪ o0 )(t1 ∪ i1 ∪ o1 ) · · · ∈
(2T ∪I∪O )ω . The projection of a trace to the atomic propositions is a path w ∈
(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 Automatic Test Case Generation
In this section, we describe a new methodology to automatically generate a set
of test cases from a given LTL specification. We first 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 Büchi 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 specification in TLSF [7] format, the formula is built with the SyFCo
tool. The Büchi 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: Ts ← ∅
3: Is ← findInputSequences(AΦ , I)
4: for σi ∈ Is do
5: Os ← selectOutputs(AΦ , σi , O)
6: T s ← T s ∪ {(σi , Os)}
7: end for
8: return T s
9: end function
Fig. 2. Büchi Automaton corresponding to the formula “ (q → ♦ r)”
The distinction between input and output sequences is needed because of
the intrinsic non-determinism normally allowed by a LTL specification. In fact,
a specification usually describes a (possibly infinite) range of allowed sequences.
The situation is even worst if the system is under-specified, 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 figure 2. Now,
let’s consider a three steps input sequence σ = [{q}, {q}, {q}], where q is true
only in the second step. If we check all possible prefixes of length 3 that are in
Words(φ), given the assignment of q fixed by σ, we see that multiple solutions
are possible. [{qr}, {qr}, {qr}] is such a solution, and so are [{qr}, {qr}, {qr}]
and [{qr}, {qr}, {qr}]. Also the sequence [{qr}, {qr}, {qr}] 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 prefix, because if extended
can lead to words in which φ is eventually satisfied. 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.
3.1 Find Input Sequences
Algorithm 2 shows the steps implemented to find the set of input sequences. After
the initialization of the Is and visited sets, the function generateFilteredBA
(line 4) returns AIΦ , a filtered version of the given automaton. The new automa-
ton 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)
∀A ∈ Σ, q ∈ Q are built from the input atomic propositions I only. The result-
ing 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 q 0 ;
Algorithm 2 Find Input Sequences from AΦ
1: function findInputSequences(AΦ , I)
2: Is ← ∅
3: visited ← ∅
4: AIΦ ← generateFilteredBA(AΦ , I)
5: for q ∈ AIΦ .Q do
6: for q 0 ∈ AIΦ .δ(q, .) do
7: if (q, q 0 ) ∈
/ visited then
8: q ∗ ← findNearestAcceptanceState(AIΦ , q 0 )
9: ρ ← sp(AIΦ , q0, q) . sp(AIΦ , q 0 , q ∗ )
10: σ ← getWord(AIΦ , ρ)
11: Is ← Is ∪ σ
12: for i ← 0 to |ρ| − 1 do
13: visited ← visited ∪ (ρ[i], ρ[i + 1])
14: end for
15: end if
16: end for
17: end for
18: Is0 ← reduce(Is)
19: return Is0
20: end function
– for every such transition (q, q 0 ) 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 q 0 to the nearest
acceptance state q ∗ (computed at line 8, with a classical breadth-first 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 proce-
dure 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 pre-
fixes of other ones. For instance, if both σ1 = [{r}, {r}] and σ2 = [{r}, {r}, {r}]
are generated, σ1 can be removed because it is a prefix 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 fulfill
the specification. 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 find all induced runs,
according to Definition 7 given in Section 2, and then use these runs to extract all
accepted words. However, the problem with this definition is that it is intended
for words that share the same alphabet of the automaton, while in this case σi is
defined over the alphabet Σ I ⊆ Σ. Therefore, we modify the notion of induced
run over input sequences as follow:
Definition 7 (Input Induced Run). Given a NBA A = (Q, Σ, δ, q0 , F ),
with Σ = 2I∪O , and an input word σ defined over the alphabet Σ I = 2I , a run %
is said to be input induced by σ, denoted σ `I %, iff qi+1 ∈ δ(qi , A) : A ∩ I = σ[i]
for all i ≥ 0.
With this new definition, we can now implement Algorithm 3. For each in-
duced run, computed relying on the definition above, we check if they are lasso
shaped and accepting (line 5). If they are, we extract the corresponding words
and we filter them out (lines 6-9) so that they only contain output variables.
The generated words are inserted in Os (line 10) and finally returned (line 14)
when all runs have been evaluated.
Algorithm 3 Select Output Sequences for input σi from AΦ
1: function selectOtputs(AΦ , σi , O)
2: Os ← ∅
3: InducedRuns ← findInputInducedRuns(AΦ , σi )
4: for ρ ∈ InducedRuns do
5: if isLassoShapedAndAccepting(AΦ , ρ) then
6: for σ ∈ getWords(AΦ , ρ) do
7: for i ← 0 to |σ| do
8: σ[i] ← σ[i] ∩ O
9: end for
10: Os ← Os ∪ σ
11: end for
12: end if
13: end for
14: return Os
15: end function
As a final remark, Algorithm 3 computes for each input sequence σi all the
corresponding lasso-shaped accepting output sequences of length |σi |. 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, filtering 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 first.
4 Experiments
Let us start our experimental evaluation by introducing the following speci-
fication as our running example, with I = {request 0, request 1} and O =
{grant 0, grant 1} being the set of input and output variables, respectively:
((grant 0 ∧ ¬request 0) → (♦ ¬grant 0)) (1)
((grant 0 ∧ X (¬request 0 ∧ ¬grant 0)) → (2)
X (¬grant 0 W (request 0 ∧ ¬grant 0)))
((grant 1 ∧ ¬request 1) → (♦ ¬grant 1)) (3)
((grant 1 ∧ X (¬request 1 ∧ ¬grant 1)) → (4)
X (¬grant 1 W (request 1 ∧ ¬grant 1)))
(¬grant 0 ∨ ¬grant 1) (5)
¬grant 0 W (request 0 ∧ ¬grant 0) (6)
¬grant 1 W (request 1 ∧ ¬grant 1) (7)
(request 0 → ♦ grant 0) (8)
(request 1 → ♦ grant 1) (9)
The specification describes the full arbiter of two clients; it eventually issues
a grant for each client if they send a request (see formulae (8) and (9)). The
specification also states that the grant should not be issued to the two clients
at the same time (see formula (5)), that if no further requests arrive it should
stop issuing the grant (formulae (1) and (3)) and that no grant should be issued
until new requests arrives (formulae (2), (4), (6) and (7)).
Given the above specification, the algorithm described in Section 3 generates
the 30 tests cases presented in Table 1. The first 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 out-
put sequences are lasso-shaped; therefore, we could extend each test sequence
indefinitely. However, each test must be finite, so we repeat the recurrent part
of the lasso-shaped sequence only once.
In order to evaluate the effectiveness of the generated test suite, we used
Strix [8] to synthesize a Mealy Machine from the same specification 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 = [{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }]. The only generated output
is σ1o = [{g0 , g1 }, {g0 , g1 }, {g0 , g1 }, {g0 , g1 }] (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 = [{g0 , g1 }, {g0 , g1 }, {g0 , g1 }, {g0 , g1 }]. σ̂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
Table 1. Generated Input Sequences
Input Seq. # of Output Seq.
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 10
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 3
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 4
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 1
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 4
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 21
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 1
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 12
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 6
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 8
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 10
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 22
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 2
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 4
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 7
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 1
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 11
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 4
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 1
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 6
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 6
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 1
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 10
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 3
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 4
{r0 , r1 } 1
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 9
{r0 , r1 }, {r0 , r1 }, {r0 , r1 } 2
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 9
{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 } 3
of output sequences and failed to find 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 find the expected output. Now, let’s con-
sider the input sequence σ2i = [{r0 , r1 }, {r0 , r1 }, {r0 , r1 }, {r0 , r1 }]. The expected
output is σ2o = [{g0 , g1 }, {g0 , g1 }, {g0 , g1 }, {g0 , g1 }]. Running σ2i on the synthe-
sized system, the system visits states S0, S2, S7, S1 and S4, and it outputs
σ̂2o = [{g0 , g1 }, {g0 , g1 }, {g0 , g1 }, {g0 , g1 }]. 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 specification does not forbid this behavior, and σ̂2o is a per-
fectly valid sequence, one may prefer to observe output σ2o instead. In situations
like this, having small sets of output sequences can be beneficial 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.
Fig. 3. The transition system generated from the full arbiter specification. S0 is the
initial state and the label on every edge represents the value of the input and output
variables. In particular, before the “/” are the values of the request 0 and request 1
input variables, respectively; after the “/” are the values of corresponding output vari-
ables grant 0 and grant 1, respectively. The “-” symbol means “don’t-care”, namely
it can assume both values.
5 Conclusion and Future Work
In this paper we presented an extension of our previous work [12] on automata-
based test generation. In particular, we propose a new framework that splits
the test case generation problem in two parts: first all input sequences are com-
puted, i.e., sequences containing only input atomic propositions, and then the
corresponding set of output sequences is selected from the automaton. We pre-
sented an algorithm to carry on both these tasks, and we shown its effectiveness
using the full arbiter specification 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 or-
der to explore and evaluate different generation strategies and outputs selection
conditions. Concerning current and future work, our next steps will focus on (1)
performing an extensive evaluation of the algorithm with different benchmarks,
(2) extending the current idea with new heuristics and selection conditions, and
(3) evaluate the possibility to replace the set of output sequences with a more
general oracle for the output validation. Finally, SpecPro is still under active
development and we aim at adding new functionalities and exploring more ex-
pressive logics.
References
1. Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008)
2. Broy, M., Jonsson, B., Katoen, J.P., Leucker, M., Pretschner, A.: Model-based
testing of reactive systems. In: Volume 3472 of Springer LNCS. Springer (2005)
3. Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.:
Spot 2.0 — a framework for LTL and ω-automata manipulation. In: Proceedings of
the 14th International Symposium on Automated Technology for Verification and
Analysis (ATVA’16). Lecture Notes in Computer Science, vol. 9938, pp. 122–129.
Springer (Oct 2016)
4. Faymonville, P., Finkbeiner, B., Tentrup, L.: Bosy: An experimentation framework
for bounded synthesis. In: Proceedings of CAV. LNCS, vol. 10427, pp. 325–332.
Springer (2017)
5. Filiot, E., Jin, N., Raskin, J.F.: Exploiting structure in ltl synthesis. International
Journal on Software Tools for Technology Transfer 15(5-6), 541–561 (2013)
6. Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey.
Software Testing, Verification and Reliability 19(3), 215–261 (2009)
7. Jacobs, S., Klein, F., Schirmer, S.: A high-level ltl synthesis format: Tlsf v1. 1.
arXiv preprint arXiv:1604.02284 (2016)
8. Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes
back! In: Computer Aided Verification - 30th International Conference, CAV 2018,
Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July
14-17, 2018, Proceedings, Part I. pp. 578–586 (2018)
9. Narizzano, M., Pulina, L., Tacchella, A., Vuotto, S.: Consistency of property speci-
fication patterns with boolean and constrained numerical signals. In: NASA Formal
Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA,
April 17-19, 2018, Proceedings. vol. 10811, pp. 383–398. Springer (2018)
10. Narizzano, M., Pulina, L., Tacchella, A., Vuotto, S.: Property specification patterns
at work: verification and inconsistency explanation. Innovations in Systems and
Software Engineering pp. 1–17 (2019)
11. Pnueli, A., Manna, Z.: The temporal logic of reactive and concurrent systems.
Springer 16, 12 (1992)
12. Vuotto, S., Narizzano, M., Pulina, L., Tacchella, A.: Automata based test genera-
tion with specpro. In: Proceedings of the 6th International Workshop on Require-
ments Engineering and Testing. pp. 13–16. IEEE Press (2019)
13. Zeng, B., Tan, L.: Test reactive systems with büchi-automaton-based temporal re-
quirements. In: Theoretical Information Reuse and Integration, pp. 31–57. Springer
(2016)