Art

J-GLOBAL ID：202002279180698363   Reference number：20A0553758

Visualization of Counterexamples of Memory Model-aware Model Checking Using SPIN

SPINを用いたメモリモデルを意識したモデル検査の反例の可視化

Author (2)： Matsumoto Kosuke (Kochi University of Technology) ,  Ugawa Tomoharu (Kochi University of Technology)
Material： Journal of Information Processing (Web)  (J Inf Proc (Web))
Volume： 27  Page： 489-498(J-STAGE)  Publication year： 2019 
JST Material Number： U0109A  ISSN： 1882-6652  Document type： Article
Article type： 原著論文  Country of issue： Japan (JPN)  Language： ENGLISH (EN)

Thesaurus term： *model checking ,  memory(computer) ,  *computer processing system ,  *connection ,  order(sequence) ,  language ,  error(measure)
Semi thesaurus term： *SPIN ,  memory ,  *memory access ,  *computer processing system ,  counterexample ,  command language

Author keywords (5)： SPIN ,  memory model ,  model checking ,  debug ,  visualization

JST classification (1)： Computer system development  (JD02010R)

Reference (16)：

• [1] Abe, T. and Maeda, T.: A General Model Checking Framework for Various Memory Consistency Models, Proc. 19th High-Level Parallel Programming Models and Supportive Environments, pp.332-341 (2014).
• [2] Aljazzar, H., Leitner-Fischer, F., Leue, S. and Simeonov, D.: DiPro - A Tool for Probabilistic Counterexample Generation, Proc. 18th International SPIN Workshop on Model Checking Software, pp.183-187 (2011).
• [3] Behrmann, G., David, A., Guldstrand Larsen, K., Håkansson, J., Pettersson, P., Yi, W. and Hendriks, M.: Uppaal 4.0, Proc. 3rd International Conference on the Quantitative Evaluation of Systems, pp.125-126 (2006).
• [4] Czyz, J.K. and Jayaraman, B.: Declarative and Visual Debugging in Eclipse, Proc. 2007 OOPSLA Workshop on Eclipse Technology eXchange, pp.31-35 (2007).
• [5] Iiboshi, H. and Ugawa, T.: Towards Model Checking Library for Persistent Data Structures, Proc. 7th Non-Volatile Memory Systems and Applications Symposium, pp.119-120 (2018).

Terms in the title (6)： SPIN ,  モデル ,  意識 ,  モデル検査 ,  反例 ,  可視化