, En cas de problème d'observation il nous faut "spéculer" et considérer tous les cas possibles pondérés par des probabilités. L'état devient alors une densité de probabilité. Pour comprendre comment un tel modèle fonctionne considérons l'observation suivante : « K , AD ». Le premier évènement reçu est K. Ce pseudo évènement signifie qu'un évènement a eu lieu, mais que l'on ne l'a pas observé. Si l'on veut pouvoir maintenir un état « spéculatif », il est nécessaire de savoir quand un évènement a été manqué, le capteur situé entre les pièces A et B. Ce?e fois-ci l'évènement ne permet pas de savoir dans quel état le système est

, avec la présence du robot en place A et D. Le probabilité de ?/? associé à la place D en (b) retourne dans la place A en (c) ; par contre la probabilité d'?/? de la place B n'est pas compatible avec l'observation et doit être supprimée. On obtient alors l'état en (c)

, Ce?e petite exécution nous montre une des difficultés principales de ce?e appro?e : il est nécessaire de renormaliser les probabilité après suppression d'une possibilité afin d'obtenir (d)

, Sur un exemple aussi trivial, la normalisation est aisée ; elle se complique dans le cas général. Il n'est pas évident qu'une telle simplification soit faisable avec un moniteur à mémoire bornée

?. ?. , D'observateur à chef d'orchestre

, Une dernière piste consiste à enri?ir le rôle de notre moniteur en lui faisant utiliser son observation pour agir sur le système. Ce?e enri?issement peut avoir deux utilisations possibles

, Ainsi à ?aque fois que la transition sera fran?ie, un actionneur sera enclen?é. Ceci permet d'introduire des boucles de rétroactions, de déclen?er des modes dégradés en cas d'erreur détectée, Actionneur L'idée est d'associer à certaines transitions (logiques ou évènementielles) un actionneur

, Injection de fautes Pour l'instant nous avons systématiquement utilisé notre moniteur pour surveiller un système en production. Cependant, un tel outil serait particulièrement adapté à l'injection de fautes. Le principe de l'injection de faute est comme son nom l'indique une pratique qui consiste à générer des entrées fautives pour voir comment le logiciel se comporte en cas d'entrée ne vérifiant pas les spécifications. L'intérêt d'un tel outil serait de générer des entrées à la volée

A. Oliver, B. Andreas, L. Martin, and S. Christian, Runtime verification revisited. Rapport te?nique TUM-I????. Te?nis?e Universität Mün?en

B. Karthikeyan, C. Satish, J. Peter, . M?c???, A. Carl et al., « What pa?ets may come : automata for network monitoring, ACM SIGPLAN Notices. T. ??. ?. ACM. ????, pp.p. ???-???

A. Klaus, F. Et-yliès, L. Decentralised, and . Monitoring, FM ???? : Formal Methods-??th International Symposium. T. ????. ????, pp.p. ??-???

K. B????????, A. Carl, and . G?????, « Requirements for a practical network event recognition language, Electronic Notes in ?eoretical Computer Science ??.? (????), pp.p. ?-??

A. B?????????, S. H???, E. F????, and C. J???, « Distributed monitoring of concurrent and asyn?ronous systems, CONCUR ????-Concurrency ?eory (????), pp.p. ?-??

A. B????, M. L??????, and C. S?????????, « Monitoring of real-time properties, FSTTCS ???? : Foundations of So?ware Technology and ?eoretical Computer Science (????), pp.p. ???-???

M. B???? and O. H. R???, On the compared expressiveness of arc, place and transition time Petri nets, Fundamenta Informaticae ??.? (????)

T. Deepak, C. Vassos, H. Sam, and T. , « ?e weakest failure detector for solving consensus, Journal of the ACM (JACM) ??.? (????), pp.p. ???-???

T. C?????? and C. J. , Time supervision of concurrent systems using symbolic unfoldings of time Petri nets, Formal Modeling and Analysis of Timed Systems (????), pp.p. ???-???

C. Feng and R. Grigore, « Mop : an efficient and generic runtime verification framework, ACM SIGPLAN Notices. T. ??. ??. ACM. ????, pp.p. ???-???

T. Deepak, C. Sam, and T. , Unreliable failure detectors for reliable distributed systems, Journal of the ACM (JACM) ??.? (????), pp.p. ???-???

F. Jean-charles and A. Jean, Building SWIFI tools from temporal logic specifications, ???? ??rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp.p. ??-??

E. F????, A. B?????????, S. H???, and C. J???, « Distributed Monitoring of Concurrent and Asyn?ronous Systems, Discrete Event Dynamic Systems ??.? (????), pp.p. ??-??

J. Mi?ael, . F??????, A. Nancy, . L????, S. Mi?ael et al., « Impossibility of distributed consensus with one faulty process, Journal of the ACM (JACM) ??.? (????), pp.p. ???-???

E. Alwyn, . G??????, and P. Lee, Monitoring distributed real-time systems : A survey and future directions. National Aeronautics et Space Administration

H. Klaus, Runtime verification of C programs

R. H. Distributable-nets, Advances in Petri Nets ???? (????), pp.p. ???-???

K. H???????, R. Grigore, and . Java, PathExplorer-A runtime verification tool, ?e ?th International Symposium on Artificial Intelligence, Robotics and Automation in Space : A New Space Odyssey. ????, pp.p. ??-??

H. Klaus and R. Grigore, « Synthesizing monitors for safety properties, Tools and Algorithms for the Construction and Analysis of Systems, pp.p. ???-???

H. Klaus and R. Grigore, « An overview of the runtime verification tool Java PathExplorer, Formal methods in system design ??.? (????), pp.p. ???-???

F. J???????, R. R???????, and S. C. R???, Runtime Monitoring of Timing Constraints in Distributed Real-Time Systems, Real-Time Systems ?.? (????), pp.p. ???-???

K. Angeliki, B. Olivier, P. Claire, R. Christine, and R. Ma?hieu, « Run-time Control to Increase Task Parallelism in MixedCritical Systems, Proceedings of the ??th Euromicro Conference on RealTime Systems (ECRTS??). ????. ??? B????????????

K. Angeliki, B. Olivier, P. Claire, R. Christine, R. Ma?hieu et al., Monitoring On-line Timing Information to Support Mixed-Critical Workloads, pp.p. ?-??

K. Moonjoo, V. Mahesh, B. Hanene, K. Sampath, . ??? et al., « Formally specified monitoring of temporal properties, Real-Time Systems, ????. Proceedings of the ??th, pp.???-???

L. Leslie, « Paxos made simple, ACM Sigact News ??.? (????), pp.p. ??-??

J. L?????, Guide de la sûreté de fonctionnement, Cépaduès-Éditions

L. François, M. Nicolas, and S. Philippe, Logic in Computer Science, Symposium on, pp.p. ???-???

P. M??????? and G. R???, « Runtime Verification with the RV system, Proceedings of the First international conference on Runtime verification, pp.p. ???-???

M. Masoud and S. Morris, « Monitoring distributed systems, pp.p. ??-??

P. Rodolfo, M. Patri?, C. Marco, and R. Grigore, « Hardware runtime monitoring for dependable cots-based real-time embedded systems, Real-Time Systems Symposium, ????. IEEE. ????, pp.p. ???- ???

M. R?????, Communication and Agreement Abstractions For Fault Tolerant Distributed Systems

T. R?????, J. C. F????, and M. R. , On-line monitoring of real time applications for early error detection, ???? ??th IEEE Pacific Rim International Symposium on Dependable Computing. IEEE. ????, pp.p. ??-??

S. Koushik, V. Abhay, A. Gul, and R. Grigore, « Decentralized runtime analysis of multithreaded applications, Parallel and Distributed Processing Symposium

K. Jun-z??-et-fabrice and . Petri, Net based runtime monitoring method for Web services specified with BPEL, Information Management and Engineering (ICIME), ???? ?e ?nd IEEE, pp.???-???

W. Z???, O. S???????, B. T. L??, and I. L. Dmac, Lecture Notes in Computer Science ???? (????)