H. Barringer, Y. Falcone, K. Havelund, G. Reger, and D. E. Rydeheard, Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors, Proceedings. Ed. by Dimitra Giannakopoulou and Dominique Méry, vol.7436, pp.68-84, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00857285

H. Barringer, A. Goldberg, K. Havelund, and K. Sen, In: Verification, Model Checking, and Abstract Interpretation, 5th International Conference, pp.44-57, 2004.

H. Barringer, A. Groce, K. Havelund, and M. H. Smith, Formal Analysis of Log Files, pp.365-390, 2010.

H. Barringer, D. E. Rydeheard, and K. Havelund, Rule Systems for Run-time Monitoring: from Eagle to RuleR, In: J. Log. Comput, vol.20, pp.675-706, 2010.

D. A. Basin, F. Klaedtke, S. Marinovic, and E. Zalinescu, Monitoring of temporal first-order properties with aggregations, In: Formal Methods in System Design, vol.46, pp.262-285, 2015.

D. A. Basin, F. Klaedtke, S. Müller, and E. Zalinescu, Monitoring Metric First-Order Temporal Properties, In: J. ACM, vol.62, p.15, 2015.

A. Bauer, M. Leucker, and C. Schallhart, Comparing LTL Semantics for Runtime Verification, In: J. Log. Comput, vol.20, issue.3, pp.651-674, 2010.

A. Bauer, M. Leucker, and C. Schallhart, Runtime Verification for LTL and TLTL

, Softw. Eng. Methodol, vol.20, p.14, 2011.

A. Bauer, M. Leucker, and J. Streit, SALTStructured Assertion Language for Temporal Logic, 8th International Conference on Formal Engineering Methods, ICFEM, 2006.

, Lecture Notes in Computer Science, vol.4260, pp.757-775, 2006.

R. Andrew, B. P. Bernat, and . Miller, Anywhere, any-time binary instrumentation, Proceedings of the 10th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools, PASTE'11, pp.9-16, 2011.

A. Blandford, P. Buchanan, . Curzon, H. Furniss, and . Thimbleby, Who's looking? Invisible problems with interactive medical devices, Proceedings of the First International Workshop on Interactive Systems in Healthcare, pp.9-12, 2010.

Y. Blein, Y. Ledru, L. Bousquet, R. Groz, A. Clère et al., MODMED WP1/D1: Preliminary Definition of a Domain Specific Specification Language, Tech. rep. LIG, MinMaxMedical, 2017.

E. Bodden and K. Havelund, Racer: effective race detection using AspectJ, Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, pp.155-166, 2008.

B. Bonakdarpour, S. Navabpour, and S. Fischmeister, Sampling-Based Runtime Verification, FM 2011: Formal Methods -17th International Symposium on Formal Methods, Limerick, Ireland, vol.6664, pp.88-102, 2011.

W. Ricky, J. L. Butler, . Caldwell, A. Victor, M. Carreno et al., NASA Langley's research and technology-transfer program in formal methods, Computer Assurance, 1995. COMPASS'95. Systems Integrity, Software Safety and Process Security. Proceedings of the Tenth Annual Conference on, pp.135-149, 1995.

D. A. Bversiooasin, M. Harvan, F. Klaedtke, and E. Zalinescu, MONPOLY: Monitoring Usage-Control Policies, In: Runtime Verification -Second International Conference, vol.7186, pp.360-364, 2011.

F. Kalou-cabrera-castillos, J. Dadeau, K. Julliand-;-alexander, and . Petrenko, Coverage Criteria for Model-Based Testing using Property Patterns, Proceedings Ninth Workshop on Model-Based Testing, vol.141, pp.29-43, 2014.

F. Chen and G. Rosu, In: Tools and Algorithms for the Construction and Analysis of Systems, Proceedings. Ed. by Stefan Kowalewski and Anna Philippou, vol.5505, pp.246-261, 2009.

Z. Chen, Parametric runtime verification is NP-complete and coNP-complete, In: Inf. Process. Lett, vol.123, pp.14-20, 2017.

A. Clère, Y. Blein, and Y. Ledru, Generic Execution Traces Specification, 2018.

J. C. Corbett, M. B. Dwyer, J. Hatcliff, and R. , Expressing checkable properties of dynamic systems: the Bandera Specification Language, pp.34-56, 2002.

D. Crocker, Can C++ be made as safe as SPARK?, In: Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, pp.5-12, 2014.

D. Crockford, The application/JSON Media Type for JavaScript Object Notation (JSON), In: RFC, vol.4627, pp.1-10, 2006.

D. Ben, S. Angelo, C. Sankaranarayanan, W. Sánchez, B. Robinson et al., LOLA: Runtime Monitoring of Synchronous Systems, 12th International Symposium on Temporal Representation and Reasoning (TIME 2005, pp.166-174, 2005.

W. Damm, H. Hungar, B. Josko, T. Peikenkamp, and I. Stierand, Using contract-based component specifications for virtual integration testing and architecture design, Design, Automation and Test in Europe, pp.1023-1028, 2011.

N. Decker, J. Harder, T. Scheffel, M. Schmitz, and D. Thoma, Runtime Monitoring with Union-Find Structures, Lecture Notes in Computer Science, vol.9636, pp.868-884, 2016.

N. Decker, M. Leucker, and D. Thoma, Monitoring modulo theories, STTT 18, vol.2, pp.205-225, 2016.

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, Patterns in Property Specifications for Finite-State Verification, Proceedings of the 1999 International Conference on Software Engineering, ICSE' 99, pp.411-420, 1999.

M. Eysholdt and H. Behrens, Xtext: implement your language faster than the quick and dirty way, Companion to the 25th Annual ACM SIGPLAN Conference on ObjectOriented Programming, Systems, Languages, and Applications, SPLASH/OOPSLA 2010, pp.307-309, 2010.

Y. Falcone and S. Currea, Weave droid: aspectoriented programming on Android devices: fully embedded or in the cloud, IEEE/ACM International Conference on Automated Software Engineering, ASE'12, pp.350-353, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00857291

Y. Falcone, S. Krstic, G. Reger, and D. Traytel, A Taxonomy for Classifying Runtime Verification Tools, Runtime Verification -18th International Conference, RV 2018, Limassol, vol.11237, pp.241-262, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01882410

Y. Falcone, L. Mounier, J. Fernandez, and J. Richier, Runtime enforcement monitors: composition, synthesis, and enforcement abilities, In: Formal Methods in System Design, vol.38, pp.223-262, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00576948

A. Fantechi, W. Fokkink, and A. Morzenti, Some trends in formal methods applications to railway signaling, In: Formal Methods for Industrial Critical Systems, pp.61-84, 2012.

S. Fischmeister and P. Lam, On Time-Aware Instrumentation of Programs, 15th IEEE Real-Time and Embedded Technology and Applications Symposium, pp.305-314, 2009.

D. M. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, On the Temporal Basis of Fairness, Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, pp.163-173, 1980.

S. Hallé and R. Villemaire, Runtime Monitoring of Message-Based Workflows with Data, 12th International IEEE Enterprise Distributed Object Computing Conference, pp.63-72, 2008.

M. Hauswirth and T. M. Chilimbi, Low-overhead memory leak detection using adaptive statistical profiling, Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems, pp.156-164, 2004.

K. Havelund, Rule-based runtime verification revisited, In: STTT, vol.17, pp.143-170, 2015.

K. Havelund and G. Reger, Specification of Parametric Monitors, In: SyDe Summer School, pp.151-189, 2015.

X. Huang, J. Seyster, S. Callanan, K. Dixit, R. Grosu et al., Software monitoring with controllable overhead, In: STTT, vol.14, issue.3, pp.327-347, 2012.

G. Hutton and E. Meijer, Monadic Parsing in Haskell, In: J. Funct. Program, vol.8, pp.437-444, 1998.

, Medical devices -Quality management systemsRequirements for regulatory purposes. Standard. Geneva, Switzerland: International Organization for Standardization, ISO, vol.13485, 2016.

, Medical devices -Application of risk management to medical devices, 2007.

. Iso/iec, Medical device software -Software life cycle processes. Standard. Geneva, Switzerland: International Organization for Standardization, 2006.

D. Jackson and J. Wing, Lightweight Formal Methods, In: ACM Comput. Surv, vol.28, p.121, 1996.

S. Jaksic, E. Bartocci, R. Grosu, R. Kloibhofer, T. Nguyen et al., From signal temporal logic to FPGA monitors, ACM/IEEE International Conference on Formal Methods and Models for Codesign, pp.218-227, 2015.

S. Jaksic, E. Bartocci, R. Grosu, and D. Nickovic, Quantitative Monitoring of STL with Edit Distance, Runtime Verification -16th International Conference, vol.10012, pp.201-218, 2016.

D. Jin, O. Patrick, C. Meredith, G. Lee, and . Rosu, JavaMOP: Efficient parametric runtime monitoring framework, 34th International Conference on Software Engineering, ICSE 2012, pp.1427-1430, 2012.

G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm et al., An Overview of AspectJ, ECOOP 2001 -Object-Oriented Programming, p.15

, Proceedings, European Conference, vol.2072, pp.327-353, 2001.

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-C: A software analysis perspective, In: Formal Asp. Comput, vol.27, issue.3, pp.573-609, 2015.
URL : https://hal.archives-ouvertes.fr/cea-01808981

M. Laurenzano, M. M. Tikir, L. Carrington, and A. Snavely, PEBIL: Efficient static binary instrumentation for Linux, IEEE International Symposium on Performance Analysis of Systems and Software, ISPASS 2010, pp.175-183, 2010.

N. G. Leveson and C. Turner, Investigation of the Therac-25 Accidents, IEEE Computer, vol.26, pp.18-41, 1993.

J. Li, G. Pu, L. Zhang, Z. Wang, J. He et al., On the Relationship between LTL Normal Forms and Büchi Automata, In: Theories of Programming and Formal Methods, vol.8051, pp.256-270, 2013.

O. Maler and D. Nickovic, In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, Proceedings. Ed. by Yassine Lakhnech and Sergio Yovine, vol.3253, pp.152-166, 2004.

C. Marché, C. Paulin-mohring, and X. Urbain, The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML, In: J. Log. Algebr. Program, vol.58, pp.89-106, 2004.

D. Méry, B. Schätz, and A. Wassyng, The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062), pp.17-38

L. Mendonça-de-moura and N. Bjørner, Z3: An Efficient SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, vol.4963, pp.337-340, 2008.

N. Nethercote and J. Seward, Valgrind: a framework for heavyweight dynamic binary instrumentation, Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pp.89-100, 2007.

T. John, C. V. O'donnell, R. L. Hall, and . Page, Discrete mathematics using a computer, 2006.

A. Ourghanlian, Evaluation of static analysis tools used to assess software important to nuclear power plant safety, Nuclear Engineering and Technology. Special Issue on ISOFIC/ISSNP2014, vol.47, pp.212-218, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01857446

A. Pnueli, The Temporal Logic of Programs, 18th Annual Symposium on Foundations of Computer Science, pp.46-57, 1977.

A. Pnueli and A. Zaks, PSL Model Checking and Run-Time Verification Via Testers, FM 2006: Formal Methods, 14th International Symposium on Formal Methods, vol.4085, pp.573-586, 2006.

G. Reger, H. C. Cruz, and D. E. Rydeheard, MarQ: Monitoring at Runtime with QEA

, Lecture Notes in Computer Science, vol.9035, pp.596-610, 2015.

G. Reger and K. Havelund, In: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications -7th International Symposium, vol.9953, pp.339-355, 2016.

G. Reger and D. E. Rydeheard, From First-order Temporal Logic to Parametric Trace Slicing, Runtime Verification6th International Conference, pp.216-232, 2015.

G. Regis, R. Degiovanni, D. Nicolás, N. Ippolito, and . Aguirre, Specifying Event-Based Systems with a Counting Fluent Temporal Logic, In: ICSE (1), pp.733-743, 2015.

C. Schnurr, I. Güdden, P. Eysel, and D. König, Influence of computer navigation on TKA revision rates, International orthopaedics, vol.36, issue.11, pp.2255-2260, 2012.

R. S. Scowen, Extended BNF -A generic base standard, 1998.

J. Seyster, K. Dixit, X. Huang, R. Grosu, K. Havelund et al., InterAspect: aspect-oriented instrumentation with GCC, In: Formal Methods in System Design, vol.41, issue.3, pp.295-320, 2012.

R. Sipos, D. Fradkin, F. Mörchen, and Z. Wang, Log-based predictive maintenance, The 20th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD '14, pp.1867-1876, 2014.

R. L. Smith, G. S. Avrunin, L. A. Clarke, and L. J. Osterweil, PROPEL: an approach supporting property elucidation, Proceedings of the 24th International Conference on Software Engineering, pp.11-21, 2002.

J. Souyris, V. Wiels, D. Delmas, and H. Delseny, Formal Verification of Avionics Software Products, Proceedings. Ed. by Ana Cavalcanti and Dennis Dams, vol.5850, pp.532-546, 2009.

O. Spinczyk and D. Lohmann, The design and implementation of AspectC++, In: Knowl.-Based Syst, vol.20, pp.636-651, 2007.

V. Stolz, In: Runtime Verification, 7th International Workshop, Oleg Sokolsky and Serdar Tasiran, vol.4839, pp.176-187, 2007.

S. Taha, J. Julliand, and F. Dadeau, A compositional automatabased semantics and preserving transformation rules for testing property patterns, In: Formal Asp. Comput, vol.27, pp.641-664, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01228335

, colophon This document was typeset using the typographical look-and-feel classicthesis developed by André Miede and Ivo Pletikosi?. The style was inspired by Robert Bringhurst's seminal book on typography "The Elements of Typographic Style