×

Abstractions refinement for hybrid systems diagnosability analysis. (English) Zbl 1461.93236

Sayed-Mouchaweh, Moamar (ed.), Diagnosability, security and safety of hybrid dynamic and cyber-physical systems. Cham: Springer. 279-318 (2018).
In this chapter authors present the abstractions refinement for hybrid systems diagnosability analysis. The authors first present the hybrid automata formalism and define diagnosability for hybrid systems. A formal framework for constructing hybrid automata abstractions while defining the refinement relation is given. The counter example guided abstraction refinement (CUGAR) scheme adapted for the diagnosability verification is given and a case study example to illustrate the scheme is presented.
For the entire collection see [Zbl 1417.68011].

MSC:

93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
93B07 Observability
93C65 Discrete event control/observation systems

Software:

Uppaal; Kronos; HyComp
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] M. Althoff, O. Stursberg, M. Buss, Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes. Nonlinear Anal. Hybrid Syst. 4(2), 233-249 (2010) · Zbl 1201.93017
[2] R. Alur, D.L. Dill, A theory of timed automata. Theor. Comput. Sci. 126(2), 183-235 (1994) · Zbl 0803.68071
[3] R. Alur, T. Dang, F. Ivančić, Counterexample-guided predicate abstraction of hybrid systems. Theor. Comput. Sci. 354(2), 250-271 (2006) · Zbl 1088.68096
[4] S. Ault, E. Holmgreen, Dynamics of the Brusselator. Academia (2009)
[5] M. Basseville, M. Kinnaert, M. Nyberg, On fault detectability and isolability. Eur. J. Control. 7(6), 625-641 (2001) · Zbl 1293.68062 · doi:10.3166/ejc.7.625-637
[6] M. Bayoudh, L. Travé-Massuyès, Diagnosability analysis of hybrid systems cast in a discrete-event framework. Discrete Event Dyn. Syst. 24(3), 309-338 (2014) · Zbl 1307.93247 · doi:10.1007/s10626-012-0153-z
[7] M. Bayoudh, L. Travé-Massuyès, X. Olive, Hybrid systems diagnosability by abstracting faulty continuous dynamics, in Proceedings of the 17th International Workshop on Principles of Diagnosis (DX’06) (2006), pp. 9-15
[8] M. Bayoudh, L. Travé-Massuyès, X. Olive, Coupling continuous and discrete event system techniques for hybrid systems diagnosability analysis, in Proceedings of the 18th European Conference on Artificial Intelligence (ECAI-08), Patras (2008), pp. 219-223
[9] M. Bayoudh, L. Travé-Massuyès, X. Olive, Active diagnosis of hybrid systems guided by diagnosability properties. IFAC Proc. Vol. 42(8), 1498-1503 (2009) · doi:10.3182/20090630-4-ES-2003.00244
[10] G. Behrmann, A. David, K.G. Larsen, A tutorial on Uppaal, in Formal Methods for the Design of Real-Time Systems (Springer, Berlin, 2004), pp. 200-236 · Zbl 1105.68350 · doi:10.1007/978-3-540-30080-9_7
[11] S. Biswas, D. Sarkar, S. Mukhopadhyay, A. Patra, Diagnosability analysis of real time hybrid systems, in Proceedings of the IEEE International Conference on Industrial Technology (ICIT’06), Mumbai (2006), pp. 104-109
[12] O. Botchkarev, S. Tripakis, Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations, in Proceedings of the 3rd International Workshop on Hybrid Systems: Computation and Control (HSCC’00). LNCS, vol. 1790 (Springer, Berlin, 2000), pp. 73-88 · Zbl 1037.93510
[13] M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, S. Yovine, Kronos: a model-checking tool for real-time systems, in International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (Springer, Berlin, 1998), pp. 298-302 · doi:10.1007/BFb0055357
[14] L. Brandán Briones, A. Lazovik, P. Dague, Optimizing the system observability level for diagnosability, in Proceedings of the 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA08), Chalkidiki, Kassandra (2008)
[15] J. Chen, R. Patton, A re-examination of the relationship between parity space and observer- based approaches in fault diagnosis, in Proceedings of the IFAC Symposium on Fault Detection, Supervision and Safety of Technical Systems Safeprocess’94, Helsinki (1994), pp. 590-596
[16] A. Cimatti, C. Pecheur, R. Cavada, Formal verification of diagnosability via symbolic model checking, in Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI-03) (2003), pp. 363-369
[17] A. Cimatti, S. Mover, S. Tonetta, SMT-based scenario verification for hybrid systems. Formal Methods Syst. Des. 42(1), 46-66 (2013) · Zbl 1284.03216 · doi:10.1007/s10703-012-0158-0
[18] A. Cimatti, A. Griggio, S. Mover, S. Tonetta, HyComp: an SMT-based model checker for hybrid systems, in Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2015), London (2015), pp. 52-67
[19] V. Cocquempot, T.E. Mezyani, M. Staroswiecki, Fault detection and isolation for hybrid systems using structured parity residuals, in Proceedings of the IEEE/IFAC-ASCC: Asian Control Conference, vol. 2, Melbourne (2004), pp. 1204-1212
[20] M.J. Daigle, A qualitative event-based approach to fault diagnosis of hybrid systems. PhD thesis, Vanderbilt University, 2008
[21] M. Daigle, X. Koutsoukos, G. Biswas, An event-based approach to hybrid systems diagnosability, in Proceedings of the 19th International Workshop on Principles of Diagnosis (DX’08) (2008), pp. 47-54
[22] M.J. Daigle, D. Koutsoukos, G. Biswas, An event-based approach to integrated parametric and discrete fault diagnosis in hybrid systems. Trans. Inst. Meas. Control. (Special Issue on Hybrid and Switched Systems) 32(5), 487-510 (2010)
[23] M.J. Daigle, I. Roychoudhury, G. Biswas, D. Koutsoukos, A. Patterson-Hine, S. Poll, A comprehensive diagnosis methodology for complex hybrid systems: a case study on spacecraft power distribution systems. IEEE Trans. Syst. Man Cybern. Part A (Special Issue on Model-based Diagnosis: Facing Challenges in Real-world Applications) 4(5), 917-931 (2010)
[24] Y. Deng, A. D’Innocenzo, M.D. Di Benedetto, S. Di Gennaro, A.A. Julius, Verification of hybrid automata diagnosability with measurement uncertainty. IEEE Trans. Autom. Control 61(4), 982-993 (2016) · Zbl 1359.68163 · doi:10.1109/TAC.2015.2455111
[25] O. Diene, E.R. Silva, M.V. Moreira, Analysis and verification of the diagnosability of hybrid systems, in Proceedings of the 53rd IEEE Conference on Decision and Control (CDC-14) (IEEE, New York, 2014), pp. 1-6 · doi:10.1109/CDC.2014.7039350
[26] O. Diene, M.V. Moreira, V.R. Alvarez, E.R. Silva, Computational methods for diagnosability verification of hybrid systems, in Proceedings of the IEEE Conference on Control Applications (CCA-15) (IEEE, New York, 2015), pp. 382-387
[27] S. Ding, Model-Based Fault Diagnosis Techniques: Design Schemes, Algorithms, and Tools (Springer, London, 2008)
[28] C. Edmund, F. Ansgar, H. Zhi, K. Bruce, S. Olaf, T. Michael, Verification of hybrid systems based on counterexample-guided abstraction refinement, in Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-2003), ed. by H. Garavel, J. Hatcliff. Lecture Notes in Computer Science, vol. 2619 (Springer, Cham, 2003), pp. 192-207 · Zbl 1031.68078
[29] G. Fourlas, K. Kyriakopoulos, N. Krikelis, Diagnosability of hybrid systems, in Proceedings of the 10th Mediterranean Conference on Control and Automation (MED-2002), Lisbon (2002), pp. 3994-3999
[30] J.-P. Gallois, J.-Y. Pierron, Qualitative simulation and validation of complex hybrid systems, in Proceedings of the 8th European Congress on Embedded Real Time Software and Systems (ERTS-2016), Toulouse (2016)
[31] S. Gao, S. Kong, E. Clarke, Satisfiability modulo ODEs, in Formal Methods in Computer-Aided Design (FMCAD) (2013)
[32] V. Germanos, S. Haar, V. Khomenko, S. Schwoon, Diagnosability under weak fairness, in Proceedings of the 14th International Conference on Application of Concurrency to System Design (ACSD’14), Tunis (IEEE Computer Society Press, New York, 2014)
[33] J. Gertler, Fault Detection and Diagnosis in Engineering Systems (Marcel Dekker, New York, 1998)
[34] A. Grastien, Symbolic testing of diagnosability, in Proceedings of the 20th International Workshop on Principles of Diagnosis (DX-09) (2009), pp. 131-138
[35] A. Grastien, L. Travé-Massuyès, V. Puig, Solving diagnosability of hybrid systems via abstraction and discrete event techniques, in Proceedings of the 27th International Workshop on Principles of Diagnosis (DX-16) (2016)
[36] S. Gulwani, A. Tiwari, Constraint-based approach for analysis of hybrid systems, in Proceedings of the 20th International Conference on Computer Aided Verification (CAV-2008) (2008), pp. 190-203 · Zbl 1155.68437
[37] E. Hainry, Decidability and undecidability in dynamical systems. Rapport de recherche (CiteSeer, 2009). http://hal.inria.fr/inria-00429965/en/
[38] T.A. Henzinger, The theory of hybrid automata, in Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (IEEE Computer Society Press, Los Alamitos, CA, 1996), pp. 278-292 · Zbl 0959.68073
[39] T.A. Henzinger, P.W. Kopke, A. Puri, P. Varaiya, What’s decidable about hybrid automata?, in Proceedings of the 27th Annual Symposium on Theory of Computing (ACM Press, New York, 1995), pp. 373-382 · Zbl 0978.68534
[40] S. Jiang, Z. Huang, V. Chandra, R. Kumar, A polynomial algorithm for testing diagnosability of discrete-event systems. IEEE Trans. Autom. Control 46(8), 1318-1321 (2001) · Zbl 1008.93053 · doi:10.1109/9.940942
[41] E. Kilic, Diagnosability of fuzzy discrete event systems. Inf. Sci. 178(3), 858-870 (2008) · Zbl 1128.93037 · doi:10.1016/j.ins.2007.09.009
[42] K.-D. Kim, S. Mitra, P.R. Kumar, Computing bounded epsilon-reach set with finite precision computations for a class of linear hybrid automata, in Proceedings of the ACM International Conference on Hybrid Systems: Computation and Control (2011) · Zbl 1362.68144
[43] B. Kuipers, Qualitative Reasoning: Modeling and Simulation with Incomplete Knowledge (MIT Press, Cambridge, MA, 1994)
[44] F. Liu, D. Qiu, Safe diagnosability of stochastic discrete-event systems. IEEE Trans. Autom. Control 53(5), 1291-1296 (2008) · Zbl 1367.93620 · doi:10.1109/TAC.2008.921035
[45] O. Maler, G. Batt, Approximating continuous systems by timed automata, in Formal Methods in Systems Biology (Springer, Berlin, 2008), pp. 77-89 · Zbl 1374.68262 · doi:10.1007/978-3-540-68413-8_6
[46] T. Melliti, P. Dague, Generalizing diagnosability definition and checking for open systems: a Game structure approach, in Proceedings of the 21st International Workshop on Principles of Diagnosis (DX’10), Portland, OR (2010), pp. 103-110
[47] M. Nyberg, Criterions for detectability and strong detectability of faults in linear systems. Int. J. Control. 75(7), 490-501 (2002) · Zbl 1031.93048 · doi:10.1080/00207170110121303
[48] Y. Pencolé, Diagnosability analysis of distributed discrete event systems, in Proceedings of the 16th European Conference on Artificial Intelligent (ECAI-04) (2004), pp. 43-47
[49] Y. Pencolé, A. Subias, A chronicle-based diagnosability approach for discrete timed-event systems: application to web-services. J. Universal Comput. Sci. 15(17), 3246-3272 (2009) · Zbl 1217.68046
[50] P. Ribot, Y. Pencolé, Design requirements for the diagnosability of distributed discrete event systems, in Proceedings of the 19th International Workshop on Principles of Diagnosis (DX’08), Blue Mountains (2008), pp. 347-354
[51] J. Rintanen, Diagnosers and diagnosability of succinct transition systems, in Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI-07), Hyderabad (2007), pp. 538-544
[52] M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, D. Teneketzis, Diagnosability of discrete event systems. Trans. Autom. Control 40(9), 1555-1575 (1995) · Zbl 0839.93072 · doi:10.1109/9.412626
[53] A. Schumann, J. Huang, A scalable jointree algorithm for diagnosability, in Proceedings of the 23rd American National Conference on Artificial Intelligence (AAAI-08) (2008), pp. 535-540
[54] D. Thorsley, D. Teneketzis, Diagnosability of stochastic discrete-event systems. IEEE Trans. Autom. Control 50(4), 476-492 (2005) · Zbl 1365.93478 · doi:10.1109/TAC.2005.844722
[55] L. Travé-Massuyès, P. Dague, Modèles et raisonnements qualitatifs (Hermès, Paris, 2003)
[56] L. Travé-Massuyès, M. Cordier, X. Pucel, Comparing diagnosability criterions in continuous systems and discrete events systems, in Proceedings of the 6th IFAC Symposium on Fault Detection, Supervision and Safety of Technical Processes (Safeprocess’06), Beijing (2006), pp. 55-60
[57] L. Travé-Massuyès, T. Escobet, X. Olive, Diagnosability analysis based on component-supported analytical redundancy relations. IEEE Trans. Syst. Man Cybern. Part A 36(6), 1146-1160 (2006) · doi:10.1109/TSMCA.2006.878984
[58] S. Tripakis, Fault diagnosis for timed automata, in Proceedings of International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT-2002). Lecture Notes in Computer Science, vol. 2469 (Springer, Berlin, 2002), pp. 205-221 · Zbl 1278.68140
[59] Y. Yan, L. Ye, P. Dague, Diagnosability for patterns in distributed discrete event systems, in Proceedings of the 21st International Workshop on Principles of Diagnosis (DX’10), Portland, OR (2010), pp. 345-352
[60] L. Ye, P. Dague, Diagnosability analysis of discrete event systems with autonomous components, in Proceedings of the 19th European Conference on Artificial Intelligence (ECAI-10) (2010), pp. 105-110 · Zbl 1211.90063
[61] T.-S. Yoo, S. Lafortune, Polynomial-time verification of diagnosability of partially observed discrete-event systems. IEEE Trans. Autom. Control 47(9), 1491-1495 (2002) · Zbl 1364.93176 · doi:10.1109/TAC.2002.802763
[62] M. Yu, D. Wang, M. Luo, D. Zhang, Q. Chen, Fault detection, isolation and identification for hybrid systems with unknown mode changes and fault patterns. Expert Syst. Appl. 39(11), 9955-9965 (2012) · doi:10.1016/j.eswa.2012.01.103
[63] J. · doi:10.1016/j.arcontrol.2013.09.009
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.