TY - GEN
T1 - Verification of uncertain embedded systems by computing reachable sets based on zonotopes
AU - Althoff, Matthias
AU - Stursberg, Olaf
AU - Buss, Martin
N1 - Funding Information:
The authors gratefully acknowledge partial financial support by the German Research Foundation (DFG) within the Transregional Collaborative Research Centre 28 Cognitive Automobiles.
PY - 2008
Y1 - 2008
N2 - Formal verification using reachability analysis has been shown to be useful for detecting design failures for controlled embedded systems, and thus to improve dependability. If the state space is hybrid, however, the growth of complexity with the dimension of the continuous dynamics limits the applicability significantly. This paper proposes an efficient approach to computing reachable sets for hybrid systems with time-varying linear continuous dynamics and uncertain inputs. The key idea is to combine zonotopes and polytopes for set representation when reachable sets are intersected with the transition guards which determine the discrete behavior of the hybrid system. Different methods for conservatively transforming zonotopes into polytopes (and vice versa) are proposed and experimentally compared.
AB - Formal verification using reachability analysis has been shown to be useful for detecting design failures for controlled embedded systems, and thus to improve dependability. If the state space is hybrid, however, the growth of complexity with the dimension of the continuous dynamics limits the applicability significantly. This paper proposes an efficient approach to computing reachable sets for hybrid systems with time-varying linear continuous dynamics and uncertain inputs. The key idea is to combine zonotopes and polytopes for set representation when reachable sets are intersected with the transition guards which determine the discrete behavior of the hybrid system. Different methods for conservatively transforming zonotopes into polytopes (and vice versa) are proposed and experimentally compared.
KW - Hybrid systems modeling and control
KW - Switched discrete and hybrid systems
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=79961020168&partnerID=8YFLogxK
U2 - 10.3182/20080706-5-KR-1001.2564
DO - 10.3182/20080706-5-KR-1001.2564
M3 - Conference contribution
AN - SCOPUS:79961020168
SN - 9783902661005
T3 - IFAC Proceedings Volumes (IFAC-PapersOnline)
BT - Proceedings of the 17th World Congress, International Federation of Automatic Control, IFAC
T2 - 17th World Congress, International Federation of Automatic Control, IFAC
Y2 - 6 July 2008 through 11 July 2008
ER -