Mining parametric temporal logic properties in model-based design for cyber-physical systems

Lions, J.L., Lbeck, L., Fauquembergue, J.L., Kahn, G., Kubbat, W., Levedag, S., Mazzini, L., Merle, D., O’Halloran, C.: Ariane 5, flight 501 failure, report by the inquiry board. Technical report, CNES (1996)

Hoffman, E.J., Ebert, W.L., Femiano, M.D., Freeman, H.R., Gay, C.J., Jones, C.P., Luers, P.J., Palmer, J.G.: The near rendezvous burn anomaly of december 1998. Technical report, Johns Hopkins University (1999)

Oss, D.G.V.: Computer software in civil aircraft. In: Digital Avionics Systems Conference, 1991. Proceedings., IEEE/AIAA 10th, IEEE pp. 324–330. (1991)

Tripakis, S., Dang, T.: Modeling, verification and testing using timed and hybrid automata. In: Model-Based Design for Embedded Systems. CRC Press (2009)

Kapinski, J., Deshmukh, J., Jin, X., Ito, H., Butts, K.: Simulation-guided approaches for verification of automotive powertrain control systems. In: American Control Conference (ACC), 2015, IEEE, pp. 4086–4095 (2015)

Nghiem, T., Sankaranarayanan, S., Fainekos, G.E., Ivancic, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, ACM Press, pp. 211–220 (2010)

Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embed. Comput. Syst. (TECS) 12, 95 (2013)

Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2, 255–299 (1990)

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Proceedings of FORMATS-FTRTFT, volume 3253 of LNCS, pp. 152–166 (2004)

Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications. In: Formal Approaches to Testing and Runtime Verification, volume 4262 of LNCS., pp. 178–192. Springer (2006)

Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410, 4262–4291 (2009)

Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: ACM International Conference on Hybrid Systems: Computation and Control (2012)

Annapureddy, Y.S.R., Fainekos, G.E.: Ant colonies for temporal logic falsification of hybrid systems. In: Proceedings of the 36th Annual Conference of IEEE Industrial Electronics, pp. 91–96 (2010)

Yang, H., Hoxha, B., Fainekos, G.: Querying parametric temporal logic properties on embedded systems. In: Int. Conference on Testing Software and Systems (2012)

Asarin, E., Donzé, A., Maler, O., Nickovic, D.: Parametric identification of temporal properties. In: Runtime Verification, Volume 7186 of LNCS., Springer (2012)

Myers, R.H., Montgomery, D.C., Anderson-Cook, C.M.: Response Surface Methodology: Process and Product Optimization Using Designed Experiments. Wiley

Annapureddy, Y.S.R., Liu, C., Fainekos, G.E., Sankaranarayanan, S.: S-taliro: A tool for temporal logic falsification for hybrid systems. In: Tools and Algorithms for the Construction and Analysis of Systems, Volume 6605 of LNCS., pp. 254–257. Springer (2011)

S-TaLiRo: Temporal logic falsification of cyber-physical systems. https://sites.google.com/a/asu.edu/s-taliro/s-taliro (2015)

Hoxha, B., Bach, H., Abbas, H., Dokhanchi, A., Kobayashi, Y., Fainekos, G.: Towards formal specification visualization for testing and monitoring of cyber-physical systems. In: Int. Workshop on Design and Implementation of Formal Tools and Systems (2014)

Sankaranarayanan, S., Fainekos, G.: Simulating insulin infusion pump risks by in-silico modeling of the insulin-glucose regulatory system. In: Int. Conf. on Computational Methods in Systems Biology (2012)

Jiang, Z., Pajic, M., Mangharam, R.: Cyber-physical modeling of implantable cardiac medical devices. Proc. IEEE 100, 122–137 (2012)

Chen, T., Diciolla, M., Kwiatkowska, M.Z., Mereacre, A.: A simulink hybrid heart model for quantitative verification of cardiac pacemakers. In: Proceedings of the Int. Conf. on Hybrid systems: Computation and Control, ACM, pp. 131–136 (2013)

Abbas, H., Hoxha, B., Fainekos, G., Ueda, K.: Robustness-guided temporal logic testing and verification for stochastic cyber-physical systems. In: Cyber Technology in Automation, Control, and Intelligent Systems, 2014 IEEE 4th Annual Int. Conf. on. (2014)

Alur, R., Henzinger, T.A.: Real-Time Logics: Complexity and Expressiveness. In: Fifth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pp. 390–401 (1990)

Hoxha, B., Mavridis, N., Fainekos, G.: Vispec : A graphical tool for elicitation of mtl requirements. In: Proceedings of the 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (2015)

Zhao, Q., Krogh, B.H., Hubbard, P.: Generating test inputs for embedded control systems. IEEE Control Syst. Mag. August 49–57 (2003)

Legriel, J., Le Guernic, C., Cotton, S., Maler, O.: Approximating the pareto front of multi-criteria optimization problems. In: TACAS, pp. 69–83. Springer (2010)

Deb, K.: Multi-Objective Optimization Using Evolutionary Algorithms, vol. 16. Wiley, New Jersey (2001)

Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3–34 (1995)

Fainekos, G., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using s-taliro. In: Proceedings of the ACC. (2012)

Donze, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Formal Modelling and Analysis of Timed Systems. LNCS, Springer (2010)

Jin, X., Donzé, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, ACM, pp. 43–52 (2013)

Hoxha, B., Dokhanchi, A., Fainekos, G.E.: Mining parametric temporal logic properties in model based design for cyber-physical systems, extended version. Technical Report arXiv:1512.07956v2 (2016)

Chutinan, A., Butts, K.R.: Dynamic Analysis of Hybrid System Models for Design Validation. Technical report, Ford Motor Company (2002)

Simuquest: Enginuity. ( http://www.simuquest.com/products/enginuity ) Accessed 14 October 2013

Conrad, M., Fey, I.: Testing automotive control software. In: Automotive Embedded Systems Handbook. CRC Press (2008)

Koopman, P.: Better Embedded System Software. Drumnadrochit Education LLC (2010)

Tan, L., Kim, J., Sokolsky, O., Lee, I.: Model-based testing and monitoring for hybrid embedded systems. In: Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration, pp. 487–492 (2004)

Plaku, E., Kavraki, L.E., Vardi, M.Y.: Falsification of ltl safety properties in hybrid systems. In: Proc. of the Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS, Springer (2009)

Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink/stateflow verification. In: Proceedings of the Int. Conf. on Hybrid Systems: Computation and Control, pp. 243–252 (2010)

Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for model measuring. ACM Trans. Comput. Logic 2, 388–407 (2001)

Di Giampaolo, B., La Torre, S., Napoli, M.: Parametric metric interval temporal logic. In: Language and Automata Theory and Applications. LNCS. Springer (2010)

Fages, F., Rizk, A.: On temporal logic constraint solving for analyzing numerical data time series. Theor. Comput. Sci. 408, 55–65 (2008)

Rizk, A., Batt, G., Fages, F., Soliman, S.: On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: International Conference on Computational Methods in Systems Biology. Volume 5307 of LNCS., pp. 251–268. Springer (2008)

Chan, W.: Temporal-logic queries. In: Proceedings of the 12th International Conference on Computer Aided Verification. Volume 1855 of LNCS., pp. 450–463. Springer (2000)

Bruns, G., Godefroid, P.: Temporal logic query checking. In: Proceedings of the 16th Annual Symposium on Logic in Computer Science, IEEE Computer Society (2001)

Chechik, M., Gurfinkel, A.: Tlqsolver: A temporal logic query checker. In: Proceedings of the 15th International Conference on Computer Aided Verification. Volume 2725., pp. 210–214. Springer (2003)

Gurfinkel, A., Devereux, B., Chechik, M.: Model exploration with temporal logic query checking. SIGSOFT Softw. Eng. Notes 27, 139–148 (2002)

Singh, A., Ramakrishnan, C., Smolka, S.A.: Query-based model checking of ad hoc network protocols. In: Proceedings of Concurrency Theory, pp. 603–619. Springer (2009)

Wasylkowski, A., Zeller, A.: Mining temporal specifications from object usage. In: 24th International Conference on Automated Software Engineering (2009)

Kong, Z., Jones, A., Medina Ayala, A., Aydin Gol, E., Belta, C.: Temporal logic inference for classification and prediction from data. In: Proceedings of the 17th International Conference on Hybrid systems: Computation and Control, ACM, pp. 273–282 (2014)