TY - JOUR
T1 - Two-layered falsification of hybrid systems guided by Monte Carlo tree search
AU - Zhang, Zhenya
AU - Ernst, Gidon
AU - Sedwards, Sean
AU - Arcaini, Paolo
AU - Hasuo, Ichiro
N1 - Funding Information:
Manuscript received April 3, 2018; revised June 8, 2018; accepted July 2, 2018. Date of publication July 23, 2018; date of current version October 18, 2018. This work was supported by ERATO HASUO Metamathematics for Systems Design Project (JST) under Grant JPMJER1603, and in part by JSPS under Grant 15KT0012. This article was presented in the International Conference on Embedded Software 2018 and appears as part of the ESWEEK-TCAD special issue. (Corresponding author: Zhenya Zhang.) Z. Zhang and I. Hasuo are with the Information Systems Architecture Science Research Division, National Institute of Informatics, Tokyo 101-8430, Japan, and also with the School of Multidisciplinary Sciences, Department of Informatics, Graduate University for Advanced Studies (SOKENDAI), Hayama 240-0193, Japan (e-mail: zhangzy@nii.ac.jp; i.hasuo@acm.org).
Publisher Copyright:
© 2018 IEEE.
PY - 2018/11
Y1 - 2018/11
N2 - Few real-world hybrid systems are amenable to formal verification, due to their complexity and black box components. Optimization-based falsification- A methodology of search-based testing that employs stochastic optimization-is thus attracting attention as an alternative quality assurance method. Inspired by the recent work that advocates coverage and exploration in falsification, we introduce a two-layered optimization framework that uses Monte Carlo tree search (MCTS), a popular machine learning technique with solid mathematical and empirical foundations (e.g., in computer Go). MCTS is used in the upper layer of our framework; it guides the lower layer of local hill-climbing optimization, thus balancing exploration and exploitation in a disciplined manner. We demonstrate the proposed framework through experiments with benchmarks from the automotive domain.
AB - Few real-world hybrid systems are amenable to formal verification, due to their complexity and black box components. Optimization-based falsification- A methodology of search-based testing that employs stochastic optimization-is thus attracting attention as an alternative quality assurance method. Inspired by the recent work that advocates coverage and exploration in falsification, we introduce a two-layered optimization framework that uses Monte Carlo tree search (MCTS), a popular machine learning technique with solid mathematical and empirical foundations (e.g., in computer Go). MCTS is used in the upper layer of our framework; it guides the lower layer of local hill-climbing optimization, thus balancing exploration and exploitation in a disciplined manner. We demonstrate the proposed framework through experiments with benchmarks from the automotive domain.
UR - http://www.scopus.com/inward/record.url?scp=85050594949&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85050594949&partnerID=8YFLogxK
U2 - 10.1109/TCAD.2018.2858463
DO - 10.1109/TCAD.2018.2858463
M3 - Article
AN - SCOPUS:85050594949
SN - 0278-0070
VL - 37
SP - 2894
EP - 2905
JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
IS - 11
M1 - 8418450
ER -