I. .. Monolithic,

.. .. Zsh,

, Automatic Checkpointing to Debug a Sudoku Solver, p.92

. .. Micro-benchmark,

, User-Perceived Performance Impact

. .. Cost-of-checkpointing,

I. .. Distributed, 97 6.2.1 Detecting Deadlocks in MPI Applications

.. .. Testing,

. .. Systems, 103 7.7 Debugging of Distributed Systems From Message Traces, p.104

, Fault Detection Based on Statistical Models

, We provided some examples that illustrate distributed i-RV. More thorough evaluation is needed on usability of distributed i-RV as well as on its performance. A case study shall be conducted on real-life bugs with developers trying our tool. We consider using the DbgBench dataset, Evaluation

, !finalNumberReceived, vol.617

. //-otherwise,

. !=-receivedverdictsbyec,

/. Handleexpectedverdictnumber, , vol.628

, // If this is an FinalVerdictNumber message, same thing but the scenario

, // remembers that the execution controller should be sent a quit request. 633 :: curMsg[self].type == FinalVerdictNumber -> 634 finalNumberReceived

, // If this is an event notification (presumably because of a prior

. //-request,

, // If no verdicts are expected for this event, let's send

, // actions and resume the execution, vol.643

, // If this is an NbMonitors messages, let's store the given number and 653

, // set the number of expected verdicts for every execution controller

, // This is cheating, since execution controllers are not known yet at

, // this point in the real protocol

, // upon the reception of hello messages of the execution controllers

, // Verdicts for an execution controller can be received before their

/. , This makes the model simpler. 661 :: curMsg[self].type == NbMonitors -> 662 nbKnownMonitors = msgNumber(curMsg[self]) 663 for (i : 0

, // If this is an acknowledgment for a request, let's continue handling

, // The event receivers are the monitors and the scenario

, // These are components that can request and receive events

, // This array is a list of these component, by order of arrival

, // of Hello messages by this execution controller)

, // If this is an Hello message 715 :: curMsg[self].type == Hello ->

, // If the joining component is a monitor or a scenario

, // identifier is stored in the list of event receivers 720 :: senderKind(curMsg[self]) == CMonitor || senderKind(curMsg[self]) == CScenario -> 721 eventReceivers

/. Cscenario, !(senderKind(curMsg[self]) == CMonitor || senderKind(curMsg, the message is ignored, vol.725

, // If this is an event receiver, it is removed from the list of

, // known event receivers 735 :: senderKind(curMsg[self]) == CMonitor || senderKind(curMsg[self]) == CScenario -> 736 do 737 :: eventReceivers[i] == curMsg[self].sender -> 738 eventReceivers[i] = eventReceivers

/. Cscenario, !(senderKind(curMsg[self]) == CMonitor || senderKind(curMsg, the message is ignored, vol.746

, // an event is generated, and either the message is final

, // if so, final verdict number will be sent. Otherwise, an expected

, // verdict number will be sent

, // -limited (if LIMIT_EVENTS is true), in which case eventsSent

, // counts the number of sent events (using the fact that

, // LIMIT_EVENTS = true = 1), and EVENT_MAX is the maximum

, // number of non-final events to generate

, // -or not (if LIMIT_EVENTS is false), in which case eventsSent

, // remains equal to zero (using the fact that

, // LIMIT_EVENTS = false = 0), to avoid changing the state of the

, // I'm not sure limiting the number of events is a great idea in this

, // model anyway, so we are probably better off keeping LIMIT_EVENTS

, (!LIMIT_EVENTS) || (eventsSent < EVENT_MAX)) -> eventsSent = eventsSent + ? LIMIT_EVENTS, vol.772

, // For each event receiver, either we sent an event notification

/. Not, The number of monitors receiving the event notification

, // is computed and will be sent to the scenario. (i : 0 .. nEventReceivers -1) { 781 if 782 :: send(EventNotification, eventReceivers, p.783

, // If this is a regular request, the execution controller sends an

, // acknowledgment 798 :: curMsg[self].type == Request -> 799 send(Ack, curMsg[self].sender, 0)

, // We include a library that provides the following macros

/. &lt;&gt;-b,

, // at runtime. This allows smaller formulas

, // -defineLTL to define an LTL property with a name that can be reused in

/. ,

. **************************/,

, // Components receiving event notifications are monitors and scenarios, vol.825, p.827

, // Requests are sents by monitors and scenarios and received by execution controllers

, // Verdicts are sent by monitors to scenarios 838 defineAlwaysLTL(verdictsFromMonitorsAndToScenarios

. &amp;&amp;,

. /**************************,

. **************************/,

, // These properties are only defined if HANDLE_VERIF_MESSAGE is true

, // These properties rely on checking values of the current messages at

, // Only curMsg[BUS] should be used, except for messages that are

, // broadcast / generated by the bus (Hello messages, NbMonitors)

, // It is hard to think about messages from other queues correctly without

, // doing mistakes. For instance, one could be tempted to write

. //-request,

. //-forall-mon,

. //-curmsg,

+. and &. &amp;&amp;,

, +)')dnl 31 undefine

, defineLTL', 'define('$1', 'apply_noteq_implies($2)') ('defineAlwaysLTL', 38 'define

, $ ( SPIN ) -a $ < 9 10 irv . pml : irv . m4 . pml constants . m4 betterltl . m4 11 $ ( M4 ) < $ < > $@ 12 13 . PHONY : clean 14 15 clean : 16 rm -rf $$

F. B. Bowen-alpern and . Schneider, Defining liveness, Inf. Process. Lett, vol.21, issue.4, pp.181-185, 1985.

F. B. Bowen-alpern and . Schneider, Recognizing safety and liveness, Distributed Computing, vol.2, issue.3, pp.117-126, 1987.

, AspectJ

A. Almalaq and J. Zhang, Evolutionary deep learning-based energy consumption prediction for buildings, IEEE Access, vol.7, pp.1520-1531, 2019.

, Lectures on Runtime Verification -Introductory and Advanced Topics, vol.10457, 2018.

, Lectures on Runtime Verification -Introductory and Advanced Topics, vol.10457, 2018.

. Bfr-+-16]-borzoo, P. Bonakdarpour, S. Fraigniaud, D. A. Rajsbaum, C. Rosenblueth et al., Decentralized asynchronous crash-resilient runtime verification, :15. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, vol.59, pp.1-16, 2016.

G. Bronevetsky, I. Laguna, S. Bagchi, R. Bronis, D. H. De-supinski et al., Automaded: Automata-based debugging for dissimilar parallel tasks, Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010, pp.231-240, 2010.

M. Brörkens and M. Möller, Dynamic event generation for runtime checking using the JDI, Electr. Notes Theor. Comput. Sci, vol.70, issue.4, pp.21-35, 2002.

, Runtime Verification -5th International Conference, vol.8734, 2014.

. Bsc-+-17]-marcel, E. O. Böhme, S. Soremekun, E. Chattopadhyay, A. Ugherughe et al., How developers debug software the dbgbench dataset: poster, Proceedings of the 39th International Conference on Software Engineering, pp.244-246, 2017.

D. Bruening and Q. Zhao, Practical memory checking with dr. memory, The 9th International Symposium on Code Generation and Optimization, pp.213-223, 2011.

D. Bruening, Q. Zhao, and S. P. Amarasinghe, Transparent dynamic instrumentation, Proceedings of the 8th International Conference on Virtual Execution Environments, pp.133-144, 2012.

P. Cousot and R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pp.238-252, 1977.

, 5th USENIX Symposium on Networked Systems Design & Implementation, NSDI, 2008.

C. Colombo, A. Francalanza, and R. Gatt, Elarva: A monitoring tool for erlang, Runtime Verification -Second International Conference, vol.7186, pp.370-374, 2011.

E. M. Clarke, O. Grumberg, and D. A. Peled, Model checking, 2001.

P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles et al., Frama-c -A software analysis perspective, Software Engineering and Formal Methods -10th International Conference, SEFM 2012, vol.7504, pp.233-247, 2012.

. Springer, , 2012.

Y. Cheon and G. T. Leavens, A simple and practical approach to unit testing: The JML and junit way, ECOOP 2002 -Object-Oriented Programming, p.16

, European Conference, pp.231-255, 2002.

C. Colombo and M. Leucker, Runtime Verification -18th International Conference, vol.11237, 2018.

M. Chabot, K. Mazet, and L. Pierre, Automatic and configurable instrumentation of C programs with temporal assertion checkers, ACM/IEEE International Conference on Formal Methods and Models for Codesign, vol.13, pp.208-217, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01393418

F. Chen and G. Rosu, Mop: an efficient and generic runtime verification framework, Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp.569-588, 2007.

F. Chen and G. Rosu, Parametric trace slicing and monitoring, Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, pp.246-261, 2009.

, Comparison of checkpoint and restore solutions

T. Dybå and T. Dingsøyr, Empirical studies of agile software development: A systematic review, Information & Software Technology, vol.50, issue.9, pp.833-859, 2008.

, Pdp-1 program library -DEC Debugging Tape, vol.21, 2019.

M. Ducassé and E. Jahier, Efficient automated trace analysis: Examples with morphine, Electr. Notes Theor. Comput. Sci, vol.55, issue.2, pp.118-133, 2001.

Q. B. Fabio and . Da-silva, Correctness proofs of compilers and debuggers : an approach based on structural operational semantics, 1992.

M. Ducassé, Opium: an extendable trace analyzer for prolog, The Journal of Logic Programming, vol.39, issue.1, pp.177-223, 1999.

, The DWARF debugging standard

E. , A. Emerson, and E. M. Clarke, Characterizing correctness properties of parallel programs using fixpoints, Automata, Languages and Programming, 7th Colloquium, Noordweijkerhout, The Netherland, vol.85, pp.169-181, 1980.

A. El, -. Hokayem, and Y. Falcone, Monitoring decentralized specifications, Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp.125-135, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01653725

A. El, -. Hokayem, and Y. Falcone, Can we monitor all multithreaded programs?, Colombo and Leucker [CL18], pp.64-89
URL : https://hal.archives-ouvertes.fr/hal-01882414

E. Ernst, R. Merola, and D. Samaan, The economics of artificial intelligence: Implications for the future of work, vol.10, 2018.

J. Engblom, A review of reverse debugging, System, Software, SoC and Silicon Debug Conference (S4D), pp.1-6, 2012.

Y. Falcone, You should better enforce than verify, Runtime Verification -First International Conference, RV 2010, St. Julians, Malta, vol.6418, pp.89-105, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00523653

Y. Falcone, J. Fernandez, and L. Mounier, What can you verify and enforce at runtime? STTT, vol.14, pp.349-382, 2012.

Y. Falcone, K. Havelund, and G. Reger, A tutorial on runtime verification, D: Information and Communication Security, vol.34, pp.141-175, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00853727

A. Francalanza, C. A. Mezzina, and E. Tuosto, Reversible choreographies via monitoring in erlang, Distributed Applications and Interoperable Systems -18th IFIP WG 6.1 International Conference, DAIS 2018, Held as Part of the 13th International Federated Conference on Distributed Computing Techniques, vol.10853, pp.75-92, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01824635

K. Georgiev and V. Marangozova-martin, Mpsoc zoom debugging: A deterministic record-partial replay approach, 12th IEEE International Conference on Embedded and Ubiquitous Computing, pp.73-80, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01006231

F. Gorostiaga and C. Sánchez, Striver: Stream runtime verification for real-time event-streams, Colombo and Leucker [CL18], pp.282-298

K. Havelund, Using runtime analysis to guide model checking of java programs, SPIN Model Checking and Software Verification, 7th International SPIN Workshop, vol.1885, pp.245-264, 2000.

, Held as Part of the Joint European Conferences on Theory and Practice of Software, vol.4959, 2008.

K. Havelund and A. Goldberg, Verify your runs, Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, vol.4171, pp.374-383, 2005.

T. Hynninen, J. Kasurinen, A. Knutas, and O. Taipale, Software testing: Survey of the industry practices, MIPRO, pp.1449-1454, 2018.

G. J. Holzmann, The model checker SPIN, IEEE Trans. Software Eng, vol.23, issue.5, pp.279-295, 1997.

K. Havelund and G. Rosu, Synthesizing monitors for safety properties, Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, vol.2280, pp.342-356, 2002.

J. Itkonen, M. Mäntylä, and C. Lassenius, Defect detection efficiency: Test case based vs. exploratory testing, Proceedings of the First International Symposium on Empirical Software Engineering and Measurement, pp.61-70, 2007.

J. Itkonen, M. Mäntylä, and C. Lassenius, How do testers do it? an exploratory study on manual testing practices, Proceedings of the Third International Symposium on Empirical Software Engineering and Measurement, pp.494-497, 2009.

. Jdb-website,

R. Jakse, Y. Falcone, J. Méhaut, and K. Pouget, Interactive runtime verification -when interactive debugging meets runtime verification, 28th IEEE International Symposium on Software Reliability Engineering, pp.182-193, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01592671

J. Joyce, G. Lomow, K. Slind, and B. W. Unger, Monitoring distributed systems, ACM Trans. Comput. Syst, vol.5, issue.2, pp.121-150, 1987.

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.

H. William and . Josephs, An on-line machine language debugger for OS/360, American Federation of Information Processing Societies: Proceedings of the AFIPS '69 Fall Joint Computer Conference, vol.35, pp.179-186, 1969.

M. José, O. Jiménez, J. Romero, J. R. Lloret, and . Diaz, Energy savings consumption on public wireless networks by SDN management, vol.24, pp.667-677, 2019.

Z. Jiang and K. P. Scheibe, Sree Nilakanta, and Xinxue (Shawn) Qu. The economics of public beta testing, Decision Sciences, vol.48, issue.1, pp.150-175, 2017.

L. Jin and C. Zhang, Process planning optimization with energy consumption reduction from a novel perspective: Mathematical modeling and a dynamic programming-like heuristic algorithm, IEEE Access, vol.7, pp.7381-7396, 2019.

S. Katz, Transactions on aspect-oriented software development I, Transactions on Aspect-Oriented Software Development I, chapter Aspect Categories and Classes of Temporal Properties, pp.106-134, 2006.

J. C. +-97]-péter-kacsuk, G. Cunha, J. Dózsa, T. Lourenço, T. R. Fadgyas et al., A graphical development and debugging environment for parallel programs, Parallel Computing, vol.22, issue.13, pp.1747-1770, 1997.

G. Kiczales, AspectJ(tm): Aspect-oriented programming in Java, Objects, Components, Architectures, Services, and Applications for a Networked World, International Conference NetObject-Days, vol.2591, 2002.

J. Klm-+-97]-gregor-kiczales, A. Lamping, C. Mendhekar, C. V. Maeda, J. Lopes et al., Aspect-oriented programming, ECOOP'97 -Object-Oriented Programming, p.11

, European Conference, vol.1241, pp.220-242, 1997.

L. Lamport, Time, clocks, and the ordering of events in a distributed system, Commun, vol.21, issue.7, pp.558-565, 1978.

W. Landi, Undecidability of static analysis, LOPLAS, vol.1, issue.4, pp.323-337, 1992.

J. C. Lck-+-97]-joão-lourenço, H. Cunha, P. Krawczyk, M. Kuzora, B. Neyman et al., An integrated testing and debugging environment for parallel and distributed programs, 23rd EUROMICRO Conference '97, p.291, 1997.

C. Luk, R. S. Cohn, R. Muth, H. Patil, A. Klauser et al., Pin: building customized program analysis tools with dynamic instrumentation, Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, pp.190-200, 2005.

. Lgds-+-11]-ignacio, T. Laguna, . Gamblin, R. Bronis, S. De-supinski et al., Large scale debugging of parallel tasks with automaded, Conference on High Performance Computing Networking, Storage and Analysis, vol.50, pp.1-50, 2011.

. Lgw-+-08]-xuezheng, Z. Liu, X. Guo, F. Wang, X. Chen et al., D3S: debugging deployed distributed systems, Crowcroft and Dahlin [CD08], pp.423-437

I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan, Runtime assurance based on formal specifications, Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 1999, pp.279-287, 1999.

M. Leucker and C. Schallhart, A brief account of runtime verification, J. Log. Algebr. Program, vol.78, issue.5, pp.293-303, 2009.

N. Kyu-hyung-lee, X. Sumner, P. Zhang, and . Eugster, Unified debugging of distributed systems with recon, Proceedings of the 2011 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2011, pp.85-96, 2011.

D. Lecomber and P. Wohlschlegel, Debugging at scale with allinea DDT

. Nagel, Tools for High Performance Computing 2012 -Contributed Papers Presented at the 6th International Parallel Tools Workshop, pp.3-12, 2012.

J. F. Maranzano and S. R. Bourne, A tutorial introduction to ADB, vol.21, 2019.

M. Mostafa and B. Bonakdarpour, Decentralized runtime verification of LTL specifications in distributed systems, 2015 IEEE International Parallel and Distributed Processing Symposium, pp.494-503, 2015.

R. Milner, Communication and concurrency. PHI Series in computer science, 1989.

C. Ben, Z. Moszkowski, and . Manna, Reasoning in interval temporal logic, Logics of Programs, Workshop, vol.164, pp.371-382, 1983.

A. V. Mirgorodskiy, N. Maruyama, and B. P. Miller, Scalable systems software -problem diagnosis in large-scale computing environments, Proceedings of the ACM/IEEE SC2006 Conference on High Performance Networking and Computing, p.88, 2006.

O. Maler and D. Nickovic, 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, FTRTFT 2004, vol.3253, pp.152-166, 2004.

D. Mahrenholz, O. Spinczyk, and W. Schröder-preikschat, Program instrumentation for debugging and monitoring with aspectc++, 5th International Symposiun on Object Oriented Real-Time Distributed Computing, pp.249-256, 2002.

R. Mvt-+-16]-reed-milewicz, J. Vanka, D. Tuck, P. Quinlan, and . Pirkelbauer, Lightweight runtime checking of C programs with RTC, Computer Languages, Systems & Structures, vol.45, pp.191-203, 2016.

S. Navabpour, Y. Joshi, C. Wu, S. Berkovich, R. Medhat et al., Rithm: a tool for enabling time-triggered runtime verification for C programs, Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE'13, pp.603-606, 2013.

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.

D. Ongaro and J. K. Ousterhout, In search of an understandable consensus algorithm, 2014 USENIX Annual Technical Conference, USENIX ATC '14, pp.305-319, 2014.

D. D. Pnp-+-19]-fabio-palomba, A. Nucci, A. Panichella, A. D. Zaidman, and . Lucia, On the impact of code smells on the energy consumption of mobile applications, Information & Software Technology, vol.105, pp.43-55, 2019.

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science, pp.46-57, 1977.

, Static Analysis -25th International Symposium, vol.11002, 2018.

K. Pouget, Programming-Model Centric Debugging for multicore embedded systems / Debogage Interactif des systemes embarques multicoeur base sur le model de programmation, 2014.
URL : https://hal.archives-ouvertes.fr/tel-01010061

, Protocul Buffers website

[. Psk-+-16a]-fábio-petrillo, Z. Soh, F. Khomh, M. Pimenta, C. M. Freitas et al., Towards understanding interactive debugging, 2016 IEEE International Conference on Software Quality, Reliability and Security, QRS 2016, pp.152-163, 2016.

Z. Psk-+-16b]-fábio-petrillo, F. Soh, M. Khomh, C. M. Pimenta, Y. Freitas et al., Towards understanding interactive debugging, 2016.

, IEEE International Conference on Software Quality, Reliability and Security, pp.152-163, 2016.

A. Pnueli and A. Zaks, PSL model checking and run-time verification via testers, FM, vol.4085, pp.573-586

. Springer, , 2006.

N. Ramsey, Correctness of trap-based breakpoint implementations, Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.15-24, 1994.

J. Roos, L. Courtrai, and J. Méhaut, Execution replay of parallel programs, Euromicro Workshop on Parallel and Distributed Processing, pp.429-434, 1993.

B. Raghavan and J. Ma, The energy and emergy of the internet, Tenth ACM Workshop on Hot Topics in Networks (HotNets-X), HOTNETS '11, p.9, 2011.

. Patrick-reipschläger, A. Burcu-kulahcioglu-ozkan, S. Shankar-mathur, R. Gumhold, R. Majumdar et al., Debugar: Mixed dimensional displays for immersive debugging of distributed systems, Extended Abstracts of the 2018 CHI Conference on Human Factors in Computing Systems, CHI 2018, 2018.

M. M. Lambèr, J. Royakkers, L. Timmer, R. Kool, and . Van-est, Societal and ethical issues of digitization, Ethics Inf. Technol, vol.20, issue.2, pp.127-142, 2018.

D. Scott, E. Stoller, J. Bartocci, R. Seyster, K. Grosu et al., Runtime verification with state estimation, RV, vol.7186, pp.193-207, 2011.

E. D. Smilowitz, M. J. Darnell, and A. E. Benson, Are we overlooking some usability testing methods? A comparison of lab, beta, and forum tests, Behaviour & IT, vol.13, issue.1-2, pp.183-190, 1994.

O. Sokolsky, K. Havelund, and I. Lee, Introduction to the special section on runtime verification, International Journal on Software Tools for Technology Transfer, vol.14, issue.3, pp.243-247, 2012.

G. Singh, T. Ch, V. N. Kumar, and . Naikan, Efficiency monitoring as a strategy for cost effective maintenance of induction motors for minimizing carbon emission and energy consumption, Rel. Eng. & Sys. Safety, vol.184, pp.193-201, 2019.

I. Stripe, The developer coefficient

X. Tu, H. Jin, X. Fan, and J. Ye, Meld: A real-time message logic debugging system for distributed systems, 5th IEEE Asia-Pacific Services Computing Conference, vol.2010, pp.59-66, 2010.

. Le-trésor-de-la-langue-française and . Informatisé,

, Wordnet, vol.20, 2019.

, Wordnet definition of computer science, vol.20, 2019.

B. Zhou, M. Kulkarni, and S. Bagchi, Vrisha: using scaling properties of parallel programs for bug detection and localization, Proceedings of the 20th ACM International Symposium on High Performance Distributed Computing, HPDC 2011, pp.85-96, 2011.