In this paper, we present the CLEAR visualizer tool, which supports the debugging task of behavioural models being analyzed using model checking techniques. The tool provides visualization techniques for simplifying the comprehension of counterexample by highlighting some specific states in the model where a choice is possible between executing a correct behaviour or falling into an erroneous part of the model. Our tool was applied successfully to many case studies and allowed us to visually identify several kinds of typical bugs. Video URL: https://youtu.be/nJLOnRaPe1A
Fri 31 MayDisplayed time zone: Eastern Time (US & Canada) change
Fri 31 May
Displayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30 | Specifications and ModelsPapers / Demonstrations / Technical Track at Van-Horne Chair(s): Sylvain Hallé Université du Québec à Chicoutimi, Canada | ||
14:00 20mTalk | PsALM: Specification of Dependable Robotic MissionsDemos Demonstrations Claudio Menghi University of Luxembourg, SnT, Christos Tsigkanos Technische Universität Wien, Thorsten Berger Chalmers University of Technology, Sweden / University of Gothenburg, Sweden, Patrizio Pelliccione Chalmers | University of Gothenburg and University of L'Aquila | ||
14:20 20mTalk | Symbolic Repairs for GR(1) SpecificationsTechnical Track Technical Track Shahar Maoz Tel Aviv University, Jan Oliver Ringert Tel Aviv University, Rafi Shalom Tel Aviv University | ||
14:40 20mTalk | ARepair: A Repair Framework for AlloyDemos Demonstrations Kaiyuan Wang Google, Inc., Allison Sullivan North Carolina Agriculture and Technical State University, Sarfraz Khurshid University of Texas at Austin | ||
15:00 20mTalk | Visual Debugging of Behavioural ModelsDemos Demonstrations Gianluca Barbon Université Grenoble Alpes, Inria, LIG, Vincent Leroy University of Grenoble - CNRS, Gwen Salaün University of Grenoble Alpes, Emmanuel Yah Université Grenoble Alpes | ||
15:20 10mTalk | Discussion Period Papers |