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

Etienne André

Description

Sous la direction de Emmanuelle Encrenaz-Tiphene, Laurent Fribourg
Thèse soutenue le 08 décembre 2010: École normale supérieure de Cachan
Cette thèse propose une nouvelle approche pour la synthèse de valeurs temporelles dans les systèmes temporisés. Notre approche est basée sur la méthode inverse suivante : à partir d’une instance de référence des paramètres, nous synthétisons une contrainte sur les paramètres, garantissant le même comportement que pour l’instance de référence, abstraction faite du temps. Il en résulte un critère de robustesse pour le système. En itérant cette méthode sur des points dans un domaine paramétrique borné, nous sommes alors à même de partitionner l’espace des paramètres en bonnes et mauvaises zones par rapport à une propriété à vérifier. Ceci nous donne une cartographie comportementale du système. Cette méthode s’étend aisément aux systèmes probabilistes. Nous présentons également des variantes de la méthode inverse pour les graphes orientés valués et les processus de décision markoviens. Parmi les prototypes implémentés, IMITATOR II implémente la méthode inverse et la cartographie pour les 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 STMicroelectronics, ainsi que plusieurs protocoles de communication.
-Vérification
-Automates temporisés paramétrés
-Synthèse de paramètres
-Vérification de circuits
-Automates temporisés probabilistes
-Protocoles de c ommunication
This thesis proposes a novel approach for the synthesis of delays for timed systems, in particular in the framework oftimed automata, a model for verifying real-time systems. Our approach relies on the following inverse method: given a reference valuation of the parameters, we synthesize a constraint on the parameters, guaranteeing the same timeabstract linear behavior as for the reference valuation. This gives a criterion of robustness to the system. By iterating this inverse method on various points 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. This gives a behavioral cartography of the system. This method extended to probabilistic systems allows to preserve minimum and maximum probabilities of reachability properties. We also present variants of the inverse method for directed weighted graphs and Markov Decision Processes. Several prototypes have been implemented; in particular, IMITATOR II implements the inverse method and the cartography for timed automata. It allowed us to synthesize parameter values for several case studies such as an abstract model of a memory circuit sold by the chipset manufacturer ST-Microelectronics, and various communication protocols.
-Model-checking
Source: http://www.theses.fr/2010DENS0044/document

Sujets

• Vérification

Informations

• Publié par: Thesee
• Nombre de lectures: 21
• Langue: English
• Poids de l'ouvrage: 3 Mo

Extrait

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 . . . . .