×

zbMATH — the first resource for mathematics

Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system. (English) Zbl 1356.68177
Summary: Interactive, or computer-assisted, theorem proving is the verification of statements in a formal system, where the proof is developed by a logician who chooses the appropriate inference steps, in turn executed by an automatic theorem prover. In this paper, interactive theorem proving is used to verify safety properties of a nonlinear (hybrid) control system.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
93C10 Nonlinear systems in control theory
93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
PDF BibTeX Cite
Full Text: DOI
References:
[1] Vande Wouwer, A.; Saucez, P.; Vilas Fernández, C., Simulation of ODE/PDE models with MATLAB, OCTAVE and SCILAB, (2014), Springer International Publishing · Zbl 1305.00007
[2] Campbell, S. L.; Chancelier, J.-P.; Nikoukhah, R., Modeling and simulation in scilab/scicos with scicoslab 4.4, (2010), Springer-Verlag New York · Zbl 1181.65005
[3] Fritzson, P., Principles of object-oriented modeling and simulation with modelica 3.3: A cyber-physical approach, (2014), Wiley
[4] Van Beek, D.; Reniers, M.; Rooda, J.; Schiffelers, R. R., Concrete syntax and semantics of the compositional interchange format for hybrid systems, (Myung Jin, C.; Pradeep, M., IFAC World Congress, IFAC 2008, (2008)), 7979-7986
[5] Schupp, S.; Ábrahám, E.; Chen, X.; Ben Makhlouf, I.; Frehse, G.; Sankaranarayanan, S.; Kowalewski, S., Current challenges in the verification of hybrid systems, (Mousavi, M. R.; Berger, C., Cyber Physical Systems. Design, Modeling, and Evaluation, Lect. Notes Comput. Sci., vol. 9361, (2015), Springer International Publishing), 8-24
[6] Alur, R., Formal verification of hybrid systems, (Proceedings of the Ninth ACM International Conference on Embedded Software, EMSOFT ’11, (2011), ACM New York, NY, USA), 273-278
[7] Tiwari, A.; Khanna, G., Nonlinear systems: approximating reach sets, (Alur, R.; Pappas, G., Hybrid Systems: Computation and Control, Lect. Notes Comput. Sci., vol. 2993, (2004), Springer Berlin, Heidelberg), 600-614 · Zbl 1135.93318
[8] Tiwari, A.; Khanna, G., Series of abstractions for hybrid automata, (Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control, HSCC ’02, (2002), Springer-Verlag London, UK), 465-478 · Zbl 1044.93523
[9] Cimatti, A.; Mover, S.; Tonetta, S., A quantifier-free SMT encoding of non-linear hybrid automata, (Formal Methods in Computer-Aided Design, FMCAD, 2012, (2012)), 187-195
[10] Cimatti, A.; Clarke, E.; Giunchiglia, E.; Giunchiglia, F.; Pistore, M.; Roveri, M.; Sebastiani, R.; Tacchella, A., Nusmv version 2: an opensource tool for symbolic model checking, (Proc. International Conference on Computer-Aided Verification, CAV 2002, Lect. Notes Comput. Sci., vol. 2404, (2002), Springer Copenhagen, Denmark) · Zbl 1010.68766
[11] Behrmann, G.; David, A.; Larsen, K.; Hakansson, J.; Petterson, P.; Yi, W.; Hendriks, M., Uppaal 4.0, (Third International Conference on Quantitative Evaluation of Systems, QEST 2006, (2006)), 125-126
[12] Tiwari, A., Hybridsal relational abstracter, (Proceedings of the 24th International Conference on Computer Aided Verification, CAV’12, (2012), Springer-Verlag Berlin, Heidelberg), 725-731
[13] Bensalem, S.; Ganesh, V.; Lakhnech, Y.; Muñoz, C.; Owre, S.; Rueß, H.; Rushby, J.; Rusu, V.; Saïdi, H.; Shankar, N.; Singerman, E.; Tiwari, A., An overview of SAL, (Proceedings of the Fifth NASA Langley Formal Methods Workshop, LFM 2000, (2000)), 187-196
[14] Benvenuti, L.; Bresolin, D.; Collins, P.; Ferrari, A.; Geretti, L.; Villa, T., Assume-guarantee verification of nonlinear hybrid systems with ARIADNE, Int. J. Robust Nonlinear Control, 24, 699-724, (2014) · Zbl 1284.93121
[15] Ratschan, S.; She, Z., Safety verification of hybrid systems by constraint propagation-based abstraction refinement, ACM Trans. Embed. Comput. Syst., 6, 1, (2007)
[16] Platzer, A.; Quesel KeYmaera, J.-D., A hybrid theorem prover for hybrid systems (system description), (Armando, A.; Baumgartner, P.; Dowek, G., Automated Reasoning, Lect. Notes Comput. Sci., vol. 5195, (2008), Springer Berlin, Heidelberg), 171-178 · Zbl 1165.68469
[17] Platzer, A., Differential dynamic logics, Künstl. Intell., 24, 1, 75-77, (2010)
[18] Paulin-Mohring, C., Introduction to the coq proof-assistant for practical software verification, (Meyer, B.; Nordio, M., Tools for Practical Software Verification, Lect. Notes Comput. Sci., vol. 7682, (2012), Springer Berlin, Heidelberg), 45-95
[19] Nipkow, T.; Wenzel, M.; Paulson, L. C., Isabelle/HOL: A proof assistant for higher-order logic, (2002), Springer-Verlag Berlin, Heidelberg · Zbl 0994.68131
[20] Owre, S.; Rushby, J.; Shankar PVS, N., A prototype verification system, (Kapur, D., Automated Deduction, CADE-11, Lect. Notes Comput. Sci., vol. 607, (1992), Springer Berlin, Heidelberg), 748-752
[21] Owre, S.; Rajan, S.; Rushby, J.; Shankar, N.; Srivas, M., PVS: combining specification, proof checking, and model checking, (Alur, R.; Henzinger, T., Computer-Aided Verification, CAV ’96, Lect. Notes Comput. Sci., vol. 1102, (1996), Springer-Verlag), 411-414
[22] Srivas, M.; Rueß, H.; Cyrluk, D., Hardware verification using PVS, (Kropf, T., Formal Hardware Verification: Methods and Systems in Comparison, Lect. Notes Comput. Sci., vol. 1287, (1997), Springer-Verlag), 156-205
[23] Carreño, V.; Muñoz, C., Aircraft trajectory modeling and alerting algorithm verification, (Aagaard, M.; Harrison, J., Theorem Proving in Higher Order Logics, Lect. Notes Comput. Sci., vol. 1869, (2000), Springer Berlin, Heidelberg), 90-105 · Zbl 0974.68548
[24] Carreño, V.; Muñoz, C., Safety verification of the small aircraft transportation system concept of operations, (Proceedings of the AIAA 5th Aviation, Technology, Integration, and Operations Conference, AIAA-2005-7423, (2005))
[25] Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and types, Camb. Tracts Theor. Comput. Sci., vol. 7, (1990), Cambridge University Press
[26] Gentzen, G. K.E., Untersuchungen über das logische schließen. I, Math. Z., 39, 2, 176-210, (1934) · Zbl 0010.14501
[27] Gentzen, G. K.E., Untersuchungen über das logische schließen. II, Math. Z., 39, 3, 176-210, (1934) · Zbl 0010.14501
[28] Owre, S.; Shankar, N.; Rushby, J. M.; Stringer-Calvert, D. W.J., PVS language reference, version 2.4, (2001), Tech. rep., SRI International Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park CA 94025, USA
[29] Shankar, N.; Owre, S.; Rushby, J. M.; Stringer-Calvert, D. W.J., PVS prover guide, version 2.4, (2001), Tech. rep., SRI International Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park CA 94025, USA
[30] Owre, S.; Shankar, N., The PVS prelude library, (2001), Tech. rep., SRI International Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park CA 94025, USA
[31] Dutertre, B., Elements of mathematical analysis in PVS, (Goos, G.; Hartmanis, J.; van Leeuwen, J.; von Wright, J.; Grundy, J.; Harrison, J., Theorem Proving in Higher Order Logics, Lect. Notes Comput. Sci., vol. 1125, (1996), Springer Berlin, Heidelberg), 141-156
[32] Gottliebsen, H., Transcendental functions and continuity checking in PVS, (Aagaard, M.; Harrison, J., Theorem Proving in Higher Order Logics, Lect. Notes Comput. Sci., vol. 1869, (2000), Springer Berlin, Heidelberg), 197-214 · Zbl 0974.68190
[33] Bliudze, S.; Krob, D., Modelling of complex systems: systems as dataflow machines, Fundam. Inform., 91, 2, 251-274, (2009) · Zbl 1176.68081
[34] Furic, S., Enforcing reliability of discrete-time models in modelica, (Proceedings of the 8th International Modelica Conference, (2011)), 638-649
[35] Di Vito, B., Strategy-enhanced interactive proving and arithmetic simplification for PVS, (Proceedings of the 1st International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, STRATA 2003, (2003)), 43-55
[36] Di Vito, B., Manip User’s guide, version 1.3, (2011)
[37] Bernardeschi, C.; Domenici, A.; Masci, P., Integrated simulation of implantable cardiac pacemaker software and heart models, (2d International Congress on Cardiovascular Technology, SCITEPRESS, CARDIOTECHNIX 2014, (2014)), 55-59
[38] Oladimeji, P.; Masci, P.; Curzon, P.; Thimbleby, H., Pvsio-web: a tool for rapid prototyping device user interfaces in PVS, (5th International Workshop on Formal Methods for Interactive Systems, FMIS2013, London, UK, June 24, 2013, (2013))
[39] Masci, P.; Zhang, Y.; Jones, P.; Oladimeji, P.; D’Urso, E.; Bernardeschi, C.; Curzon, P.; Thimbleby, H., Combining pvsio with stateflow, (Proceedings of the 6th NASA Formal Methods Symposium, NFM2014, (2014), Springer-Verlag Berlin, Heidelberg)
[40] Archer, M.; Vito, B. D., Developing user strategies in pvs: a tutorial, (Proceedings of the First International Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, STRATA, 2003, (2003))
[41] Muñoz, C.; Narkawicz, A.; Hagen, G.; Upchurch, J.; Dutle, A.; Consiglio, M., DAIDALUS: detect and avoid alerting logic for unmanned systems, (Proceedings of the 34th Digital Avionics Systems Conference, DASC 2015, Prague, Czech Republic, (2015))
[42] Daumas, M.; Lester, D.; Muñoz, C., Verified real number calculations: a library for interval arithmetic, IEEE Trans. Comput., 58, 2, 226-237, (2009) · Zbl 1367.65213
[43] Bernardeschi, C.; Cassano, L.; Domenici, A.; Masci, P., Simulation and test-case generation for PVS specifications of control logics, Int. J. Adv. Softw., 4, 3 & 4, 327-341, (2011)
[44] Bernardeschi, C.; Cassano, L.; Domenici, A.; Masci, P., Debugging PVS specifications of control logics via event-driven simulation, (Computation Tools 2010, IARIA, Lisbon, Portugal, (2010))
[45] Bernardeschi, C.; Domenici, A.; Masci, P., Towards a formalization of system requirements for an integrated clinical environment, (5th EAI International Conference on Wireless Mobile Communication and Healthcare, MOBIHEALTH 2015, (2015), ACM)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.