Une méthode inverse pour la synthèse de paramètres temporels dans les systèmes concurrents, An inverse method for the synthesis of timing parameters in concurrent systems

THÈSE
présentéeàl’ coleNormaleSupérieuredeCachan
envuedel’obtentiondugradede
Docteurdel’ÉcoleNormaleSupérieuredeCachan
par?tienneANDR?
Spécialitéinformatique
AnInverseMethodfortheSynthesis
ofTimingParametersinConcurrentSystems
Soutenuele8décembre2010devantunjurycomposéde
EugeneASARIN Examinateur
BernardBERTHOMIEU Rapporteur
FranckCASSEZ Rapporteur
EmmanuelleENCRENAZ-TIPHENE Co-directricedethèse
LaurentFRIBOURG Co-directeurdethèse
MartaKWIATKOWSKA Examinatrice
KimG.LARSEN Eateur
tel-00595268, version 1 - 24 May 2011tel-00595268, version 1 - 24 May 2011Abstract
Thisthesisproposesanovelapproachforthesynthesisofdelaysfortimedsys-
tems. Whenverifyingareal-timesystem, e.g., ahardwaredevice oracommu-
nicationprotocol,itisimportanttocheckthatnotonlythefunctionalbutalso
the timed behavior is correct. This correctness depends on the values of the
delaysofinternaloperationsandoftheenvironment.
Formal verification methods guarantee the correctness of a timed system
for a given set of delays, but do not give information for other values of the
delays. Checking the correctness of for various values of those delays can be
difficultandtimeconsuming. Itisthusinterestingtoconsiderthatthesedelays
are parameters. The problem then consists in synthesizing “good values” for
thoseparameters,i.e.,valuesforwhichthesystemisguaranteedtobehavewell.
We are here interested in the synthesis of parameters in the framework of
timed automata, a model for verifying real-time systems. Our approach relies
onthefollowinginversemethod: givenareferencevaluationoftheparameters,
we synthesize a constraint on the parameters, guaranteeing the same time-
abstract linear behavior as for the reference valuation. This gives a criterion
ofrobustnesstothesystem. Byiteratingthisinversemethodonvariouspoints
of a bounded parameter domain, we are then able to partition the parametric
space into good and bad zones, with respect to a given property one wants to
verify. Thisgivesabehavioralcartographyofthesystem.
This method extended to probabilistic systems allows to preserve mini-
mum and maximum probabilities of reachability properties. We also present
variantsoftheinversemethodfordirectedweightedgraphsandMarkovDeci-
sion Processes. Several prototypes have been implemented; in particular, IM-
ITATORII implements the inverse method and the cartography for timed au-
tomata. It allowed us to synthesize parameter values for several case studies
such as an abstract model of a memory circuit sold by the chipset manufac-
turerST-Microelectronics,andvariouscommunicationprotocols.
Keywords: verification, model checking, timed systems, parametric timed
automata, synthesis of parameters, hardware verification, probabilistic timeda,randomizedprotocols.
tel-00595268, version 1 - 24 May 2011ii Abstract
tel-00595268, version 1 - 24 May 2011Résumé
Cettethèseproposeunenouvelleapprochepourlasynthèsedevaleurstempo-
rellesdanslessystèmestemporisés.Lorsquel’onvérifieunsystèmetemps-réel,
commeuncircuitouunprotocoledecommunication,ilestimportantdevéri-
fiernonseulementl’aspectfonctionnel,maiségalementtemporisé.Lacorrec-
tiondusystèmedépenddevaleurstemporellesinternesetdel’environnement.
Les méthodes formelles de vérification garantissentlacorrectiond’un sys-
tèmetemporisépourunensembledevaleurstemporelles,maisnedonnentpas
d’information pour d’autres valeurs. Vérifier la correction d’un système pour
de nombreuses valeurspeuts’avérer longetdifficile. Il estalors intéressantde
lesconsidérercommeparamètres.Leproblèmeconsistealorsàsynthétiserdes
valeursdecesparamètrespourlesquelleslesystèmeestcorrect.
Nous nous intéressons ici à la synthèse de paramètres dans le cadre des
automates temporisés. Notre approche est basée sur la méthode inverse sui-
vante:àpartird’uneinstancederéférencedesparamètres,noussynthétisons
une contrainte sur les paramètres, garantissant le même comportement que
pourl’instancederéférence,abstractionfaitedutemps.Ilenrésulteuncritère
derobustessepourlesystème.Enitérantcetteméthodesurdespointsdansun
domaineparamétriqueborné,noussommesalorsàmêmedepartitionnerl’es-
pacedesparamètresenbonnesetmauvaiseszonesparrapportàunepropriété
àvérifier.Cecinousdonneunecartographiecomportementaledusystème.
Cette méthode s’étend aisément aux systèmes probabilistes. Nous présen-
tons également des variantes de la méthode inverse pour les graphes orien-
tésvaluésetlesprocessusdedécisionmarkoviens.Parmilesprototypesimplé-
mentés,IMITATORIIimplémentelaméthodeinverseetlacartographiepourles
automates temporisés. Ce prototype nous a permis de synthétiser de bonnes
valeurs pour les paramètres temporels de plusieurs études de cas, dont un
modèle abstrait d’une mémoire commercialisée par le fabricant de puces ST-
Microelectronics,ainsiqueplusieursprotocolesdecommunication.
Mots-clés : vérification, model-checking, systèmes temporisés, automates
temporisés paramétrés, synthèse de paramètres, vérification de circuits, auto-
matestemporisésprobabilistes,protocolesdecommunication.
tel-00595268, version 1 - 24 May 2011iv Résumé
tel-00595268, version 1 - 24 May 2011Remerciements
Je remercie en premier lieu mes directeurs de thèse Emmanuelle ENCRENAZ
et Laurent FRIBOURG pour les pistes de recherche qu’ils ont su me conseiller
au cours de ces trois années, pour leurs conseils avisés, pour nos discussions
parfoiscontradictoiresettoujoursbénéfiques.
JetienségalementàremercierBernardBERTHOMIEUetFranckCASSEZpour
m’avoir fait l’honneur de relire ma thèse, et y avoir apporté des commentaires
constructifs. I would also like to thank Eugene ASARIN, Marta KWIATKOWSKA
and Kim G. LARSEN to have done me the great honor of accepting to take part
tomyjury.
Ungrandmerciégalementàplusieurspersonnesquim’ont,d’unemanière
oud’uneautre,encouragéàentreprendreunethèse:Patrice QUINTON enpre-
mierlieupoursesconseilstrèsjudicieux,SébastienFERRÉetMireilleDUCASSÉ
pour m’avoir accordé leur confiance et leur soutien pendant mon Master 2, et
enfinArnaudGOTLIEBpoursesencouragements.
Cette thèse n’aurait pu exister dans sa forme actuelle sans les personnes
avec qui j’ai eu l’occasion de travailler au cours de ces trois années. En tant
quemembreduprojetVALMEM,j’aieulachancedebénéficierd’uneétudede
cas réaliste et très motivante en la mémoire SPSMALL, grâce aux travaux des
autresmembresduprojetquesont,outremesdeuxdirecteursdethèse,Abdel-
rezzak BARA, Pirouz BAZARGAN-SABET, Remy CHEVALLIER, Dominique LE DU
et Patricia RENAULT. Cette étude de cas a, par sa complexité, motivé plusieurs
techniques développées dans cette thèse, et notamment la réalisation de IMI-
TATORII. Merci également à Ulrich KÜHNE pour avoir poursuivi le développe-
mentd’IMITATORII,etàRomain SOULAT pouravoirexpérimentédenouvelles
techniques permettant ainsi l’analyse de deux modèles de la mémoire SPS-
MALL(etpouravoirmartyrisé delonguesnuitsdurant). Ialsothank
Jeremy SPROSTON for reading my thesis and suggesting numerous interesting
enhancements.
Évidemment,merciauLSVpourlatrèsbonneambiancequiyrègne,etqui
permet d’y réaliser une thèse dans d’excellentes conditions. Et puis, comme
#$% !""
tel-00595268, version 1 - 24 May 2011vi Remerciements
il est d’usage de glisser dans cet exercice oblig quelques allusions private
que personne ne comprendra ou ne lira jamais, probablement pas m!me les
personnes concern es, merci aux occupants de la salle Renodo pour leurs
(bruyantes)partiesdetravailcollaboratifdutempsoùilstentaientencorederi-
valiseravecmoi,merci#laRATPdem’avoirpermisder aliserTicketII,quiaura
gay le mur en face de moi # d faut de m’enrichir, merci # mon presque voi-
sin de bureau pour m’avoir emmen # la d couverte des paysages ferroviaires
d’Asiecentraleaubeaumilieudel’hiveretdemath$seetaugranddamdenos
encadrants respectifs, merci # Val rie pour avoir contribu # d velopper nos
capacit s cr atrices et nous avoir fait d couvrir tout Paris # pied, merci # mes
pimentspouravoirconsciencieusementpouss ,m!medanslesmomentsdif-
ficilesquerepr sentel’hivercachannais,merci#ceux(etsurtoutcelles)quiles
ontarros s–etpuis, last but not least commeondit,merci#monv lo.Enfin,
merci#mesparentssansquijeneseraispasl#(c’estunetautologie). 最後，
非常感謝黃磊長久以來的支持和幫助。
tel-00595268, version 1 - 24 May 2011Contents
Abstract i
Résuméenfrançais iii
Remerciements v
ListofAlgorithms xi
ListofFigures xv
ListofTables xvii
1 Introduction 1
1.1 TheGoodParametersProblem . . . . . . . . . . . . . . . . . . . . . 2
1.2 Context . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.2.1 ClassicalProblems . . . . .