Repairing Timed Automata Clock Guards through Abstraction and Testing
Étienne André Paolo Arcaini Angelo Gargantini Marco Radavelli



















 ifpackageloadedhyperref
 doi#1https://doi.org/#1
   https://doi.org/#1
 doi#1https://doi.org/#1
 `_=12doi






 




 













Inputinput
Outputoutput



 


ienumeration
	[i)] 
	


oneenumeration
	[1)]
	



















arrows,automata,positioning,shapes 
every node=[initial text=]
location=[rectangle, rounded corners, minimum size=12pt, draw=black, fill=blue!10, inner sep=2pt]
invariant=[draw=black, dotted, inner sep=1pt, node distance=0] 
final=[double, fill=blue!50]


urgent=[fill=yellow, thick, dotted] 


























 



 








 

 
 

 






















	draft
	15
	[gray]0.9








 
linelinelines 






	


	




















 






	
	
	
	 
	taRepairTAP2019.bib

	
	*doi+eprint+url
		bbx:doi
			doi
			
		bbx:eprint
			eprint
			
		bbx:url
	
			url+urldate
			
	














































 





 
 
 
 
 
















 

 



 





 
 

 






 
 
 
 
 
 

 


 





 
 
 
 




 








 
 
 
 
 



 







 








 


















researchquestionCount


	


	























































assumptionAssumption







plain











Université Paris 13, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France
JFLI, CNRS, Tokyo, Japan
National Institute of Informatics, Tokyo, Japan
University of Bergamo, Bergamo, Italy



Repairing Timed Automata Clock Guards
through Abstraction and TestingThis is the version with comments. To disable comments, comment out line 3 in the  source.
	This is the author (and slightly extended) version of the manuscript of the same name published in the proceedings of the https://tap.sosy-lab.org/2019/13th International Conference on Tests and Proofs (TAP 2019).
	This version contains some additional explanations and all proofs.
	The published version is available at 
		https://www.springer.comspringer.com.
	
	This work is partially supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST
		and
	by the ANR national research program PACS (ANR-14-CE28-0002).

    Étienne André1,2,30000-0001-8473-9555
Paolo Arcaini30000-0002-6253-4062 Angelo Gargantini40000-0002-4035-0131 Marco Radavelli40000-0002-1165-9981

    December 30, 2023
====================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================





Timed automata (TAs) are a widely used formalism to specify systems having temporal requirements. However, exactly specifying the system may be difficult, as the user may not know the exact clock constraints triggering state transitions. In this work, we assume the user already specified a , and (s)he wants to validate it against an oracle that can be queried for acceptance. Under the assumption that the user only wrote wrong guard transitions ( the structure of the TA is correct), the search space for the correct TA can be represented by a Parametric Timed Automaton (PTA),  a TA in which some constants are parametrized. The paper presents a process that

[(i)]

  * abstracts the initial (faulty) TA in a PTA ;

  * generates some test data ( timed traces) from ;

  * assesses the correct evaluation of the traces with the oracle;

  * uses the tool for synthesizing some constraints on the parameters of ;

  * instantiate from a as final repaired model.we can remove this part?


Experiments show that the approach is successfully able to partially repair the initial design of the user.


 Regular research papers: full submissions describing original research, of up to 16 pages (excluding references).







§ INTRODUCTION




Timed automata () <cit.> represent a widely used formalism for modeling and verifying concurrent timed systems.
A common usage is to develop a describing the running system and then apply analysis techniques to it ( <cit.>). However, exactly specifying the system under analysis may be difficult, as the user may not know the exact clock constraints that trigger state transitions, or may perform errors at design time. Therefore, validating the produced against the real system is extremely important to be sure that we are analyzing a faithful representation of the system. Different testing techniques have been proposed for timed automata, based on different coverage criteria as,  transition coverage <cit.> and fault-based coverage <cit.>, and they can be used for validation. However, once some failing tests have been identified, it remains the problem of detecting and removing (repair) the fault from the under validation. How to do this in an automatic way is challenging. One possible solution could be to use mutation-based approaches <cit.> in which mutants are considered as possible repaired versions of the original ; however, due to the continuous nature of timed automata, the number of possible mutants ( repair actions) is too big also for small and, therefore, such approaches do not appear to be feasible. We here propose to use a symbolic representation of the possible repaired and we reduce the problem of repairing to finding an assignment of this symbolic representation.

Contribution
In this work, we address the problem of testing/validating under the assumption that only clock guards may be wrong, that is, we assume that the structure (states and transitions) is correct.
Moreover, we assume to have an oracle that we can query for acceptance of timed traces, but whose internal structure is unknown: this oracle can be a Web-service, a medical device, a protocol, etc. In order to symbolically represent the search space of possible repaired , we use the formalism of parametric timed automata (PTAs) <cit.> as an abstraction to represent all possible behaviors under all possible clock guards.


We propose a framework for automatic repair of that takes as input a to repair and an oracle. The process works as follows:


	
  * starting from , we build a PTA where to look for the repaired ;
	
  * we build a symbolic representation of the language accepted by in terms of an extended parametric zone graph ;
	
  * we then generate some test data from ;
	
  * we assess the correct evaluation of by querying the oracle, so building the test suite ;
	
  * we feed the tests to the <cit.> tool that finds some constraints that restrict only to those that correctly evaluate all the tests in ;
	
  * as the number of that are correct repairs may be infinite, we try to obtain, using a constraint solver based on local search, the closest to the initial . Note that trying to modify as less as possible the initial is reasonable if we assume the competent programmer hypothesis <cit.>.


In order toTo evaluate the feasibility of the approach, we have performed some preliminary experiments showing that the approach is able to (partially) repair a faulty . 





Outline
The paper is structured as follows.
<ref> explains the definitions we need in our approach.
Then <ref> presents the process we propose that combines model abstraction, test generation, constraint generation, and constraint solving.
<ref> describes experiments we performed to evaluate our process.
Finally, <ref> reviews some related work, and <ref> concludes the paper.






§ DEFINITIONS









 §.§ Timed words and languages



A timed word <cit.> over an alphabet of actions  is a possibly infinite sequence of the form
(_0 , d_0) (_1, d_1) ⋯
such that, for all integer i ≥ 0, _i ∈ and d_i ≤ d_i+1.
A timed language is a (possibly infinite) set of timed words.







 §.§ Clocks, parameters and guards





We assume a set = {_1, …, _} of clocks,  real-valued variables that evolve at the same rate.
A clock valuation is a function
: →.
We write  for the clock valuation assigning 0 to all clocks.
Given d ∈, + d isdenotes the valuation  ( + d)() = () + d, for all ∈.

Given ⊆, we define the reset of a valuation , denoted by , as follows: () = 0 if ∈, and ()=() otherwise.


We assume a set = {_1, …, _} of parameters,  unknown constants.
A parameter valuation  is a function
: →.
We assume ∈{<, ≤, =, ≥, >}.
A clock guard  is a constraint over ∪ defined by a conjunction of inequalities of the form




∑_1 ≤ i ≤α_i _i + d, with
	_i ∈,
	and
	α_i, d ∈.

Given , we write () if 
the expression obtained by replacing each  with () and each  with () in  evaluates to true.






 §.§ Parametric timed automata



Parametric timed automata (PTAs) extend timed automata with parameters within guards and invariants in place of integer constants <cit.>.



	A PTA  is a tuple , where:
	
		
  *  is a finite set of actions,
		
  *  is a finite set of locations,
		
  * ∈ is the initial location,
		
  * ⊆ is the set of accepting locations,
		
  *  is a finite set of clocks,
		
  *  is a finite set of parameters,
		
  *  is the invariant, assigning to every ∈ a clock guard (),
		
  *  is a finite set of edges = (,,,,')
		where ,'∈ are the source and target locations, ∈, ⊆ is a set of clocks to be reset, and  is a clock guard.
	



Given = (,,,,'), we define () =.



Consider the PTA in <ref>, containing two clocks x and y and three parameters 2, 3 and 4.
The initial location is _1.








Given a parameter valuation , we denote by  the non-parametric structure where all occurrences of a parameter _i have been replaced by (_i).

	We denote as a timed automaton any such structure , by assuming a rescaling of the constants: by multiplying all constants in  by the least common multiple of their denominators, we obtain an equivalent (integer-valued) TA, as defined in <cit.>.





  §.§.§ Synchronized product of PTAs



The synchronous product (using strong broadcast,  synchronization on a given set of actions), or parallel composition, of several PTAs gives a PTA (see <cit.> for a common formal definition).












  §.§.§ Concrete semantics of TAs




Let us now recall the concrete semantics of TA.




	Given a PTA = (, , , , , , , ),
	and a parameter valuation ,
	the semantics of  is given by the timed transition system (TTS) (, , ), with
	
		
  * = { (, ) ∈×^|()}, 
		
  *  = (, ),
		
  *  consists of the discrete and (continuous) delay transition relations:
		
			
  * discrete transitions: (,)  (','), 
				if (, ) , (',') ∈, and there exists = (,,,,') ∈, such that '=, and ().
				
			
  * delay transitions: (,) d (, +d), with d ∈, if ∀ d' ∈ [0, d], (, +d') ∈.
		
	


  Moreover we write (, )(, d) (',') for a combination of a delay and discrete transition if
		
		∃” : (,) d (,”)  (',').

Given a TA  with concrete semantics (, , ), we refer to the states of  as the concrete states of .
A run of  is an 
alternating sequence of concrete states of  and pairs of edges and delays starting from the initial state  of the form
_0, (_0, d_0), _1, ⋯
with
i = 0, 1, …, _i ∈, d_i ∈ and
	_i (_i, d_i)_i+1.
The associated timed word is ((_0) , d_0) ((_1), ∑_0 ≤ i ≤ 1 d_i) ⋯.
A run is maximal if it is infinite or cannot be extended by any discrete action.
The (timed) language of a TA, denoted by (), is the set of timed words associated with maximal runs of .







Given a state =(, ), we say that  is reachable in  if  appears in a run of .
By extension, we say that  is reachable in ; and by extension again, given a set  of locations, we say that  is reachable if there exists ∈ such that  is reachable in .










	Consider the TA  in <ref>. 
	Consider the following run  of :
	
    (_1,
    		 ( [ x = 0; y = 0;       ] ) )
    
    		(a, 2.5)
    (_4,
    		 ( [ x = 2.5;   y = 0;         ] ) )
    
    (c, 2)
    	(_5,
    		 ( [ x = 4.5;   y = 2;         ] ) )


	We write “= 2.5” instead of “ such that () = 2.5”.
	The associated timed word is (a, 2.5) (c, 4.5).



















	Consider again the PTA  in <ref>.
	The parametric zone graph of  is given in <ref>, where
		_1 is the edge from _1 to _2 in <ref>,
		_2 is the edge from _2 to _3,
		_3 is the edge from _1 to _4,
		and
		_4 is the edge from _4 to _5.
	In addition, the symbolic states are:

!
		_1 =(     _1     ,     0 ≤x = y≤ 4 2≥ 0 _3 ≥ 0 _4 ≥ 0     )

		_2 =(     _2     ,     0 ≤x = y≤32≥ 0 _3 ≥ 0 _4 ≥ 0     )

		_3 =(     _3     ,     x = y≥32≥ 0 _3 ≥ 4 _4 ≥ 0     )

		_4 =(     _4     ,     2 < x≤ 6 y≥ 0 2 < x - y≤ 4  4 > 2≥ 0 _3 ≥ 0 _4 ≥ 0     )

		_5 =(     _5     ,     2 < x4 < xy > 1 2 < x - y≤ 4  4 > 2≥ 0 _3 ≥ 0  6 > _4 ≥ 0     )
	










	







 §.§ Reachability synthesis





We will use reachability synthesis to solve the problem in <ref>.
This procedure, called , takes as input a PTA  and a set of target locations , and attempts to synthesize all parameter valuations  for which  is reachable in .
(, ) was formalized in  <cit.> and is a procedure that traverses the parametric zone graph of ;
 may not terminate (because of the infinite nature of the graph), but computes an exact result (sound and complete) if it terminates.





	Consider again the PTA  in <ref>.





	(, {_5 }) returns 0 ≤2 < 4  0 ≤4≤ 6 3≥ 0.
	Intuitively, this corresponds to all parameter constraints in the parametric zone graph in <ref> associated to symbolic states with location _5 (there is a single such state).









	We finally recall the correctness of .

	










§ A REPAIRING PROCESS USING ABSTRACTION AND TESTING









 §.§ Problem




In this paper, we address the guard-repair problem of timed automata.
Given a reference TA  and an oracle  knowing an unknown timed language , our goal is to modify (“repair”) the timing constants in the clock guards of  such that the repaired automaton matches the timed language .

The setting assumes that the oracle can be queried for acceptance of timed words by ; that is,  can decide whether a timed word belongs to , but the internal structure of the object leading to  ( an unknown timed automaton) is unknown.

This setting makes practical sense when testing black-box systems.

guard-repair
	an initial TA , an unknown timed language 
	Repair the constants in the clock guards of  so as to obtain a TA  such that () =

While the ultimate goal is to solve this problem, in practice the best we can hope for is to be as close as possible to the unknown oracle TA, notably due to the undecidability of language equivalence of timed automata <cit.> ( if  was generated by another TA).








 §.§ Overview of the method



From now on, we describe the process we propose to automatically repair an initial timed automaton .
<ref> describes the approach:I'd prefer have a nice vectorial TikZ image… but let's see for the final version :-)





  Step 192 a PTA is generated starting from the initial .

  Step 193 the extended parametric zone graph (an extension of ) is built.

  Step 194 a test generation algorithm generates relevant test data from .


  Step 195 is evaluated using the oracle, therefore building the test suite .

  Step 196 some constraints are generated, restricting to the that evaluate correctly the generated tests .

  Step 197 one possible satisfying the constraints is obtained.




<ref> formalizes steps 192–196 for which we can provide some theoretical guarantees ( the non-emptiness of the returned valuation set, and its inclusion of ).



[!tb]
{| (, ) ∈}*Tests that must be accepted

{| (, ) ∈}*Tests that must be rejected











⋀_∈(, ) ⋀_∈(, )


GenConstraints(,)



For step 197, instead, different approaches could be adopted: in the paper, we discuss a possible one.
We emphasize that, with the exception of Step 192, our process is entirely automated.
We describe each phase in details in the following sections.





 §.§ Step 192: Abstraction



Starting from the initial , through abstraction, the user obtains a PTA that generalizes in all the parts that can be possibly changed in order to repair (<ref> in <ref>). For instance, a clock guard with a constant value can be parametrized. Therefore, represents the set of all the that can be obtained when repairing . is built on the base of the domain knowledge of the developer who has a guess of the clock guards that may be faulty. 


Consider again the TA in <ref>.
A possible abstraction of this TA is the PTA in <ref>, where we chose to abstract some of the timing constants with parameters.
Note that not all timing constants must necessarily be substituted with parameters; also note that a same parameter can be used in different places (this is the case of 3).







  
Assumption


We define below an important assumption for our method; we will discuss in <ref> how to lift it.


	We here assume that is a correct abstraction,  it contains a that precisely models the oracle.
	That is, there exists  such that () =.



Note that this assumption is trivially valid if faults lay in the clock guards (which is the setting of this work), and if all constants used in clock guards are turned to parameters.









 §.§ Step 193: construction of the extended parametric zone graph



Starting from , we build a useful representation of its computations in terms of an extended parametric zone graph (<ref> in <ref>).
This original data structure will be used for test generation.
In the following, we describe how we build from .



We extend the parametric zone graph  with the two following pieces of information:

	
  the parameter constraint characterizing each symbolic state: from a state (, ), the parameter constraint is  and gives the exact set of parameter valuations for which there exists an equivalent concrete run in the automaton. That is, a state (, ) is reachable in  iff  (see <cit.> for details).
	
  the minimum and maximum arrival times: that is, we compute the minimum (m_i) and maximum (M_i) over all possible parameter valuations of the possible absolute times reaching this symbolic state.

While the construction of the first information is standard, the second one is original to our work and requires more explanation.
We build for each state a (possibly unbounded) interval that encodes the absolute minimum and maximum arrival time.
This can be easily obtained from the parametric zone graph by adding an extra clock never reset (that encodes the absolute time), and projecting the obtained constrained on this extra clock, thus giving minimum and maximum times over all possible parameter valuations.



	Consider again the PTA  in <ref> and its parametric zone graph in <ref>. The parameter constraints associated to each of the symbolic states, and the possible absolute reachable timesvocabulary!, are given in <ref>.

	






	If all locations of the original PTA contain an invariant with at least one inequality of the form  or d, with ∈{ <, ≤}, and if the parameters are boundedvocabulary, then the maximum arrival time in each symbolic state will always be finite.
	Note that this condition is not fulfilled in <ref> because _2 features an invariant x≤3, with 3 unbounded, thus allowing to remain arbitrarily long in _2 for an arbitrarily large value of 3.
	Therefore, the arrival time in _3 is ∈ [4, ∞).



in fact,  is “even more infinite” than ; should we mention it as a remark?





 §.§ Step 194: Test data generation



Starting from , we generate some test data (<ref> in <ref>) in terms of timed words.



  §.§.§ Constructing timed words

We use the minimal and maximum arrival times in the abstract PTA to generate test data.
That is, we will notably use the boundary information,  runs close to the fastest and slowest runs, to try to discover the actual timing guards of the oracle.

The procedure to generate a timed word from the EPZG is as follows:

	
  * Pick a run _0 _0 _1 ⋯ … _n from .
	
  * Construct the timed word (_0, d_0) (_1, d_1) ⋯ (_n-1, d_n-1), where _i = (_i) and d_i belongs to the interval of reachable times associated with symbolic state _i+1, for 0 ≤ i ≤ n - 1.

	Note that, depending on the policy (see below), we sometimes choose on purpose valuations outside of the reachable times.


lemma concerning correctness/completeness?

Given an EPZG, we generate, for each finite path of the EPZG up to a given depth K, one timed word.

In order to chose a timed word from a (symbolic) path of the EPZG, we identified different policies.





  §.§.§ Policies


For each k < K, we instantiate (_0, d_0) (_1, d_1) ⋯ (_k, d_k) by selecting particular values for each d_i using different policies:



  * : d_j ∈ I_± 1, where I_± 1={-1, , +1, -1, , +1} and and are the minimum and maximum arrival times of the symbolic state.


  * : d_j ∈ I_ minMax2 with I_ minMax2 = I_± 1∪{(+)/2 }.

  * : d_j ∈ I_ minMax4 with I_ minMax4 = I_ minMax2∪{+ (-)/4, + ((-)/4)*3}.

  * : d_j being a random value such that ≤ d_j ≤.




Consider again the PTA  in <ref> and its parametric zone graph in <ref> together with reachable times in <ref>.
Pick the run _1 _3 _4 _4 _5.
First note that (_3) = a and (_4) = c.
According to <ref>, the reachable times associated with _4 are (0,4] while those associated with _5 are (1,6].
Therefore, a possible timed word generated with is (a, 1) (c, 5).
Note that this timed word does not belong to the TA to be repaired (<ref>) because of the guard x > 2; however, it does belong to an instance TA of <ref> for a sufficiently small value of 2 (namely (2) < 1).
We will see later that such tests are tagged as failing.







 §.§ Step 195: Test labeling



Then, every test sequence in is checked against the oracle in order to label it as accepted or not (<ref> in <ref>), therefore the test suite ;
a test case in is a pair (, ()), being  a timed word, and () the evaluation of the oracle,  () is defined as a Boolean the value of which is ∈.[To limit the number of tests, we only keep the maximal accepted traces ( we remove accepted traces included in longer accepted traces), and the minimal rejected traces ( we remove rejected traces having as prefix another rejected trace).]
A test case fails if () ≠(),  the initial TA and the oracle timed language disagree. Note that, if is no test case fails, is considered correct[
	This does not necessarily mean that both TAs have the same language, but that the tests did not exhibit any discrepancy.
]
and the process terminates.

In different settings, different oracles can be used. In this work, we assume that the oracle is the real system of which we want to build a faithful representation; the system is black-box, and it can only be queried for acceptance of timed words. In another setting, the oracle could be the user who can easily assess which words should be accepted, and wants to validate their initial design. Of course, the type of oracle also determines how many test data we can provide for assessment: while a real implementation can be queried a lot (modulo the time budget and the execution time of a single query), a human oracle usually can evaluate only few tests.note: “their” is better than “her/his” and is (here) perfectly equivalent





 §.§ Step 196: Generating constraints from timed words




Given the test suite , our approach generates constraints that restrict to only those that correctly evaluate the tests (<ref> in <ref>).


In this section, we explain how to “replay a timed word”,  given a PTA , how to synthesize the exact set of parameter valuations  for which a finite timed word belongs to the timed language of .


Replaying a timed word is close to two undecidable problems for PTAs:
[ i)]
	
  *  the reachability of a location is undecidable for PTAs <cit.>, and therefore this result trivially extends to the reachability of a single action;
	
  *  the emptiness of the set of valuations for which the set of untimed words is the same as a given valuation is undecidable for PTAs <cit.> (where a proof is given even for a unique untimed word).

Nevertheless, computingComputing
the set of parameter valuations for which a given finite timed word belongs to the timed language can be done easily by exploring a small part of the symbolic state space.
Replaying a timed word is also very close to theprocedure in <cit.> where we synthesized valuations corresponding to a trace,  a timed word without the time information—which is decidable.TODO later: cite Michal and Woijciech

  §.§.§ From timed words to timed automata

First, we convert the timed word into a (non-parametric) timed automaton.
This straightforward procedure was introduced in <cit.>, and simply consists in converting a timed word of the form(_1, d_1), ⋯ , (_n, d_n)into a sequence of transitions labeled with_iand guarded with = d_i(wheremeasures the absolute time,  is an extra clock never reset).

Let  denote this procedure.[
	This procedure transforms the word to a non-parametric TA; we nevertheless use the name  for consistency with <cit.>.
]

	Consider again the timed word  mentioned in <ref>: (a, 0.5) (c, 5).
	The result of () is given in <ref>.


0.5
Consider again the timed word  mentioned in <ref>: (a, 0.5) (c, 5). The result of () is given in <ref>.
  0.47[scale=0.9, xscale=1.1, yscale=1.5, auto, ->, >=stealth']

[location, initial] at (0, 0) (l0) _0;

[location] at (2, 0) (l1) _1;

[location] at (4, 0) (l2) _2;

 (l0) edge node[align=center][above]= 0.5 node[below]a (l1);
 (l1) edge node[align=center][above]= 5 node[below]c (l2);

figureTranslation of timed word (a, 0.5) (c, 5)

  §.§.§ Synchronized product and synthesis

The second part of step 196 consists in performing the synchronized product of()and, and calling  on the resulting PTA with the last location of the timed word as the target of.

Let(, )denote the entire procedure of synthesizing the valuations associated that make a timed word possible.



	Consider again the PTA  in <ref> and the timed word (a, 0.5) (c, 5) translated to a (P)TA in <ref>.
	The result of  applied to the synchronized product of these two PTAs with {_2} as target location set is





	0 ≤4 < 5  0 ≤2 < 1/23≥ 0.
	
    0 ≤4 < 5  0 ≤2 < 1/23≥ 0.

	This set indeed represents all possible valuations for which (a, 0.5) (c, 5) is a run of the automaton.
	
	Note that the result can be non-convex.
	If we now consider the simpler timed word (a, 3), then the result of (, ) becomes








	3≥ 3 2≥ 0 4≥ 0     2 < 3 3≥ 0 4≥ 0
	
    3≥ 3 2≥ 0 4≥ 0     2 < 3 3≥ 0 4≥ 0

	This comes from the fact that the action a can correspond to either _1 (from _1 to _2) or _3 (from _1 to _4) in <ref>.I haven't reread my examples, that were generated by , but hopefully no figure has changed since

	Despite the non-guarantee of termination of the general  procedure,  not only always terminates, but is also very efficient in practice: indeed, it only explores the part of the PTA corresponding to the sequence of (timed) transitions imposed by the timed word.
	This comes from the fact that we take the synchronized product of  with (), the latter PTA being linear and finite.
	(Recall that there are no silent transitions “ϵ” in our setting.)

	Let  be a PTA, and  be a timed word.
	Then (, ) terminates.


From the definition of the synchronous product (<ref>), the composition of () ∥_ will only allow the transitions shared by both the timed word and the original PTA , thanks to the synchronization of the whole set of actions .
Although the PTA may contain cycles (and therefore yield an infinite state space), note that the timed word automaton () consists of a single sequence of transitions without any cycles.
Therefore the composition () ∥_ will yield an acyclic automaton;
this is true only because, in our setting, we do not allow silent (“ϵ”) transitions, that could create cycles in  without synchronization with ().

With an acyclic composed PTA, the PZG (and therefore the EPZG) will be trivially finite.
As  relies on these structures, it will terminate.
Therefore,  terminates.



 §.§ Correctness
We introduce a result assessing the capabilities of the proposed process.

Recall that <ref> assumes that there exists a valuationsuch that() = . We show that, under <ref>, our resulting constraint is always non-empty and contains the valuation.



	Let = (, ).
	Then ≠ and .


	Proofs of <ref> can be found in <cit.>.


 As a first remark, note that, if the test data generated are in finite number (<ref> in <ref>), the algorithm  always terminates: a finite number of test cases lead to a finite calls to , and thanks to <ref>, these calls terminate.



Fix .
Let us show that a timed word  belongs to the timed automaton  iff (, ).

Since  is called on the synchronized product of () and , then the timed word  is automatically a timed word of () ∥_ iff the last location (say _n) of () is reachable in () ∥_.

Therefore, from <ref>,  is a timed word of () ∥_ iff (() ∥_, _n).

Now note that, due to the synchronous product between () and , we have that, for any word  and valuation ,  is a word of  iff  is a word of () ∥_.
Therefore  is a timed word of  iff (() ∥_, _n).


After these preliminary results, let us move to the main proof of <ref>.
The result of (, ) is given by the conjunction of the results of  called on the words accepted by the oracle with the conjunction of the negation of the results of  called on the words rejected by the oracle.
From the above reasoning,  will contain all valuations  for which  is a timed word of  for each ∈, and will contain all valuations  for which  is not a timed word of  for each ∈.
Therefore, by definition from the oracle and from <ref>, the result  must contain at least .



Therefore, since from <ref>,  exists, then trivially ≠.



 §.§ Step 197: Instantiation of a repaired 

Any assignment satisfying  characterizes a correct  the generated tests in ; however, not all of them exactly capture the oracle behaviour.

If the user wants to select one , (s)he can select one assignment  of , and use it to instantiate the final repaired .

In order to select one possible assignment , different strategies may be employed, on the base of the assumptions of the process. In this work, we assume the  competent programmer hypothesis <cit.> that the developer produced an initial  close to be correct; therefore, we want to generate a final  that is  not too different from . In particular, we assume that the developer did small mistakes on setting the values of the clock guards.

In order to find the closest values of the clock guards that respect the constraints, we exploit the local search capability of the constraint solver Choco <cit.>:


  *  we start from the observation that  is an instantiation of . We therefore select the parameter evaluation  that generates  from , = ();

  *  we initialize Choco with ; Choco then performs a local search trying to find the assignment closest (according to a notion of distance defined later in <ref>) to , and that satisfies .



 §.§ Discussing <ref>

<ref> assumes that the user provides a PTA  that contains the oracle.

If this is not the case, the test generation phase (<ref>) may generate a negative test ( not accepted by any instance of ) that is instead accepted by the oracle or a positive test that is not accepted by the oracle;
in this case, the constraints generation phase would produce an unsatisfiable constraint . In this case, the user should refine the abstraction by parameterizing some other clock guards, or by relaxing the constraints on some existing parameters.

Moreover, it could be that the correct oracle has a different structure (additional states and transitions): as future work, we plan to apply other abstractions as CoPtA models <cit.> that allow to parametrize states and transitions.





Note that, even if the provided abstraction is wrong, our approach could still be able to refine it. In order to do this, we must avoid to use for constraint generation (step 196) tests that produce unsatisfiable constraints. We use a greedy incremental version of  in which  is called incrementally: if the constraint generated for a testis not compatible with the other constraints generated previously, then it is discarded; otherwise it is conjuncted.
<ref> shows a  that we will use in the experiments as alternative oracle.



§ EXPERIMENTAL EVALUATION



In order to evaluate our approach, we selected some benchmarks from the literature to be used as initial : the model of a coffee machine () <cit.>, of a car alarm system () <cit.>, and the running case study (). For each benchmark model, <ref> reports its number of locations and transitions.



The proposed approach requires that the developer, starting from , provides an abstraction in terms of a PTA . For the experiments, as we do not have any domain knowledge, we took the most general case and we built  by adding a parameter for each guard constant; the only optimization that we did is to use the same parameter when the same constant is used on entering and/or exiting transitions of the same location (as in <ref>).

In the approach, the oracle should be the real system that we can query for acceptance; in the experiments, the oracle is another𝑡𝑎_othat we obtained by slightly changing some constants on the guards. The oracle has been built in a way that it is an instance of , following <ref>.

In order to measure  how much a  (either the initial one  or the final one ) is different from the oracle, we introduce a syntactic and a semantic measure, that provide different kinds of comparison with the oracle𝑡𝑎_o.

Given a model𝑡𝑎, the oracle𝑡𝑎_o, and a PTA  having parametersp_1, …, p_n, letvandv_obe the corresponding evaluations,𝑡𝑎 = v()and𝑡𝑎_o = v_o(). We define the syntactic distance of𝑡𝑎to the oracle as follows:


(𝑡𝑎) = ∑_i=1^n |v(p_i) - v_o(p_i)|
 The syntactic distance roughly measures how much𝑡𝑎must be changed (under the constraints imposed by ) in order to obtain𝑡𝑎_o.

The  semantic conformance, instead, tries to assess the distance between the languages accepted by𝑡𝑎and the oracle𝑡𝑎_o. As the set of possible words is infinite, we need to select a representative set of test data ;
	to this aim, we generate, from  and𝑡𝑎_o, sampled test data 
		in the two ;
	moreover, we also add negative tests by extending the positive tests with one forbidden transition at the end.
The semantic conformance is defined as follows:where is the maximum length defined, here?Probably we do not fix the maximum length. We just generate tests achieving a given coverage.but what is “path coverage”, then? We can't guarantee path coverage, can we?

(𝑡𝑎) = |{t ∈ | (t ∈(𝑡𝑎) ∧ t ∈(𝑡𝑎_o)) ∨ (t ∉(𝑡𝑎) ∧ t ∉(𝑡𝑎_o)) }|/||
<ref> also reports  and  of each benchmark .

Experiments have been executed on a Mac OS X 10.14, Intel Core i3, with 4 GiB of RAM. Code is implemented in Java,  2.11 “Butter Kouign-amann” <cit.> is used for constraint generation, and Choco 4.10 for constraint solving. The code and the benchmarks are available at <https://github.com/ERATOMMSD/repairTAsThroughAbstraction>.





 §.§ Results
<ref> reports the experimental results.


For each benchmark and each test generation policy (see <ref>), it reports the execution time (divided between the different phases), the total number of generated tests, the number of tests that fail on , and  and  of the final .

We now evaluate the approach answering the following research questions.

Is the approach able to repair faulty ?

We evaluate whether the approach is actually able to (partially) repair . From the results, we observe that, in three cases out of four, the process can completely repair  since  becomes 0, meaning that we obtain exactly the oracle (therefore, also  becomes 100%). For  and , it almost always reduces the syntactical distance , but it never finds the exact oracle. On the other hand, the semantic conformance  is 100% in five cases. Note that  can be 100% with  different from 0 for two reasons: either the test data  we are using for  are not able to show the unconformity, or  is indeed equivalent to the oracle, but with a different structure of the clock guards.

Which is the best test generation strategy?

In <ref>, we proposed different test generation policies over . We here assess the influence of the generation policy on the final results. , , and  obtain the same best results for two benchmarks ( and ), meaning that the most useful tests are those on the boundaries of the clock guards: those are indeed able to expose the failure if the fault is not too large. On the other hand, for ,  performs slightly worse than the other two, meaning that also generating tests inside the intervals (as done by  and ) can be beneficial for repair.  is able to improve (but not totally repair) only ; for the other two benchmarks, instead, it is not able to improve neither  nor .


How long does the approach take?

The time taken by the process depends on the size of  and on the test generation policy. The most expensive phase is the generation of the constraints, as it requires to call  for each test that must be accepted.
As future work, we plan to optimize this phase by modifying  to synthesize valuations guaranteeing the acceptance of multiple timed words in a single analysis.
In the experiments, we use as oracle another  that we can visit for acceptance; this visit is quite fast and so step 195 does not take too much time. However, in the real setting, the oracle is the real system whose invocation time may be not negligible; in that case, the invocation of the oracle could become a bottleneck and we would need to limit the number of generated tests.




Which is the process performance if  does not include the oracle?<ref> assumes that the user provides a PTA that contains the oracle. In <ref>, we discussed about the possible consequences when this assumption does not hold. We here evaluate whether the approach is still able to partially repair  using an oracle having a different structure. We took the  shown in <ref> as oracle of the running example, that is structurally different from  and  shown in <ref> (we name this experiment as ); the semantic conformance  of  the new oracle is shown at the last row of <ref>[Note that it does not make sense to measure the syntactical distance, as the structure of the oracle is different.]. We performed the experiments with the new oracle using the greedy approach described in <ref>, and results are reported in <ref>.


We observe that policies , , and , although they find some failing tests, they are not able to improve . This is partially due to the fact that  is computed on some timed words  that may be not enough to judge the improvement. On the other hand, as the three policies try to achieve a kind of coverage of  (so implicitly assuming <ref>), it could be that they are not able to find  interesting failing tests ( they cannot be repaired); this seems to be confirmed by the fact that the random policy  is instead able to partially repair the initial  using only three tests, out of which one fails. We conclude that, if the assumption does not hold, trying to randomly select tests could be more efficient.






§ RELATED WORK

Testing timed automata
Works related to ours are approaches for test case generation for timed automata. In <cit.>, a fault-based approach is proposed. The authors defined 8 mutation operators for  and a test generation technique based on bounded-model checking; tests are then used for model-based testing to check that System Under Test (SUT) is conformant with the specification. Our approach is different, as we aim at building a faithful representation of the SUT ( the oracle). Their mutation operators could be used to repair our initial , as done in <cit.>; however, due to continuous nature of , the possible mutants could be too many. For this reason, our approach symbolically represents all the possible variations of the clock guards (similar to “change guard” mutants in <cit.>). Other classical test generation approaches for timed automata are presented in <cit.>; while they aim at coverage of a single , we aim at coverage of a family of  described by .



Learning timed systems
	In a different direction, learning timed systems has been studied in the past.
	Learning consists in retrieving an unknown language, with membership and equivalence queries made to a teacher.

The (timed) language inclusion is undecidable for timed automata <cit.>, making learning impossible for this class.
In <cit.>, timed extensions of theL^*algorithm <cit.> were proposed for event-recording automata <cit.>, a subclass of timed automata for which language equivalence can be decided.
Learning is essentially different from our setting, as the system to be learned is usually a white-box system, in which the equivalence query can be decided.
In our setting, the oracle does not necessarily know the structure of the unknown system, and simply answers membership queries.
In addition, we address in our work the full class of timed automata, for which learning is not possible (a non-necessarily terminating procedure is given in <cit.>).






§ CONCLUSION AND PERSPECTIVES



This paper proposes an approach for automatically repairing timed automata, notably in the case where clock guards shall be repaired.
Our approach generates an abstraction of the initial TA in terms of a PTA, generates some tests, and then refines the abstraction by identifying only those TAs contained in the PTA that correctly evaluate all the tests.

As future work, we plan to adopt also other formalisms to build the abstraction where to look for the repaired timed automata;
The CoPtA model <cit.>, for example, extends timed automata with feature models and allows to specify additional/alternative states and transitions.
In addition, when the oracle acts as a white-box,  when the oracle is able to test language equivalence, we could also make use of learning techniques for timed automata despite the undecidability of the language inclusion problem, using the often terminating procedure for language inclusion in <cit.>.






	 
















[title=References]
splncs04