Runtime enforcement of regular timed properties by suppressing and delaying events

Schneider, 2000, Enforceable security policies, ACM Trans. Inf. Syst. Secur., 3, 30, 10.1145/353323.353382 Hamlen, 2006, Computability classes for enforcement mechanisms, ACM Trans. Program. Lang. Syst., 28, 175, 10.1145/1111596.1111601 Ligatti, 2009, Run-time enforcement of nonsafety policies, ACM Trans. Inf. Syst. Secur., 12, 19:1, 10.1145/1455526.1455532 Falcone, 2011, Runtime enforcement monitors: composition, synthesis, and enforcement abilities, Form. Methods Syst. Des., 38, 223, 10.1007/s10703-011-0114-4 Pinisetty, 2012, Runtime enforcement of timed properties, vol. 7687, 229 Zeng, 2013, Strato: a retargetable framework for low-level inlined-reference monitors, 369 Erlingsson, 2000, IRM enforcement of Java stack inspection, 246 Pinisetty, 2014, Runtime enforcement of parametric timed properties with practical applications, 420 Pinisetty, 2014, Runtime enforcement of regular timed properties, 1279 Falcone, 2012, What can you verify and enforce at runtime?, Int. J. Softw. Tools Technol. Transf., 14, 349, 10.1007/s10009-011-0196-8 Alur, 1994, A theory of timed automata, Theor. Comput. Sci., 126, 183, 10.1016/0304-3975(94)90010-8 Bengtsson, 2003, Timed automata: semantics, algorithms and tools, vol. 3098, 87 Henzinger, 1994, Symbolic model checking for real-time systems, Inf. Comput., 111, 193, 10.1006/inco.1994.1045 Behrmann, 2004, A tutorial on UPPAAL, vol. 3185, 200 Alur, 1999, Event-clock automata: a determinizable class of timed automata, Theor. Comput. Sci., 211, 253, 10.1016/S0304-3975(97)00173-4 Bengtsson, 2003, Timed automata: semantics, algorithms and tools, vol. 3098, 87 Maler, 2006, From MITL to timed automata, 274 Nickovic, 2010, From MTL to deterministic timed automata, vol. 6246, 152 Bouyer, 2007, On the optimal reachability problem of weighted timed automata, Form. Methods Syst. Des., 31, 135, 10.1007/s10703-007-0035-4 S. Pinisetty, Y. Falcone, T. Jéron, H. Marchand, TiPEX: a tool chain for timed property enforcement during execution, in: Bartocci and Majumdar [56], pp. 306–320, http://dx.doi.org/10.1007/978-3-319-23820-3_22. Larsen, 1997, UPPAAL in a nutshell, Int. J. Softw. Tools Technol. Transf., 1, 134, 10.1007/s100090050010 Gruhn, 2006, Patterns for timed property specifications, Electron. Notes Theor. Comput. Sci., 153, 117, 10.1016/j.entcs.2005.10.035 Pinisetty, 2014, Runtime enforcement of timed properties revisited, Form. Methods Syst. Des., 45, 381, 10.1007/s10703-014-0215-y Havelund, 2002, Synthesizing monitors for safety properties, 342 Havelund, 2005, Verify your runs, vol. 4171, 374 Leucker, 2009, A brief account of runtime verification, J. Log. Algebraic Program., 78, 293, 10.1016/j.jlap.2008.08.004 Sokolsky, 2012, Introduction to the special section on runtime verification, Int. J. Softw. Tools Technol. Transf., 14, 243, 10.1007/s10009-011-0218-6 Falcone, 2013, A tutorial on runtime verification, vol. 34, 141 Seto, 1998, The simplex architecture for safe online control system upgrades, 3504 Bak, 2011, Sandboxing controllers for cyber-physical systems, 3 Bak, 2013, Using run-time checking to provide safety and progress for distributed cyber-physical systems, 287 S. Mitsch, A. Platzer, Modelplex: verified runtime validation of verified cyber-physical system models, in: Bonakdarpour and Smolka [55], pp. 199–214, http://dx.doi.org/10.1007/978-3-319-11164-3_17. Colombo, 2012, Fast-forward runtime monitoring – an industrial case study, vol. 7687, 214 D.A. Basin, G. Caronni, S. Ereth, M. Harvan, F. Klaedtke, H. Mantel, Scalable offline monitoring, in: Bonakdarpour and Smolka [55], pp. 31–47, http://dx.doi.org/10.1007/978-3-319-11164-3_4. A. Kassem, Y. Falcone, P. Lafourcade, Monitoring electronic exams, in: Bartocci and Majumdar [56], pp. 118–135, http://dx.doi.org/10.1007/978-3-319-23820-3_8. Goodloe, 2010 Sokolsky, 2006, Run-time checking of dynamic properties, Electron. Notes Theor. Comput. Sci., 144, 91, 10.1016/j.entcs.2006.02.006 Bauer, 2011, Runtime verification for LTL and TLTL, ACM Trans. Softw. Eng. Methodol., 20, 14:1, 10.1145/2000799.2000800 Thati, 2005, Monitoring algorithms for metric temporal logic specifications, Electron. Notes Theor. Comput. Sci., 113, 145, 10.1016/j.entcs.2004.01.029 D.A. Basin, F. Klaedtke, E. Zalinescu, Algorithms for monitoring real-time properties, in: Khurshid and Sen [57], pp. 260–275, http://dx.doi.org/10.1007/978-3-642-29860-8_20. Sammapun, 2005, RT-MaC: runtime monitoring and checking of quantitative and probabilistic properties, 147 Nickovic, 2007, AMT: a property-based monitoring tool for analog systems, vol. 4763, 304 Colombo, 2008, Dynamic event-based runtime monitoring of real-time and contextual properties, vol. 5596, 135 Colombo, 2009, LARVA – safer monitoring of real-time Java programs, 33 Falcone, 2010, You should better enforce than verify, vol. 6418, 89 Bielova, 2011, Do you really mean what you actually enforced?, Int. J. Inf. Secur., 10, 239, 10.1007/s10207-011-0137-2 Meredith, 2010, Runtime verification with the RV system, vol. 6418, 136 Colombo, 2012, Safer asynchronous runtime monitoring using compensations, Form. Methods Syst. Des., 41, 269, 10.1007/s10703-012-0142-8 Basin, 2013, Enforceable security policies revisited, ACM Trans. Inf. Syst. Secur., 16, 3, 10.1145/2487222.2487225 Kim, 2002, Computational analysis of run-time monitoring – fundamentals of Java-MaC, Electron. Notes Theor. Comput. Sci., 70, 80, 10.1016/S1571-0661(04)80578-4 Pnueli, 2006, PSL model checking and run-time verification via testers, vol. 4085, 573 A.P. Sistla, M. Zefran, Y. Feng, Runtime monitoring of stochastic cyber-physical systems with hybrid state, in: Khurshid and Sen [57], pp. 276–293, http://dx.doi.org/10.1007/978-3-642-29860-8_21. Rosu, 2012, On safety properties and their monitoring, Sci. Ann. Comput. Sci., 22, 327 Viswanathan, 2004, Foundations for the run-time monitoring of reactive systems – fundamentals of the MaC language, vol. 3407, 543 2014, vol. 8734 2015, vol. 9333 2012, vol. 7186