APSEC 2022
Tue 6 - Fri 9 December 2022
Wed 7 Dec 2022 13:40 - 13:55 at Room3 - Model Checking 1 Chair(s): Hiroyuki Nakagawa

Model-based Testing (MBT) has been proposed to create test cases more efficiently and effectively. In contrast, analysis techniques (e.g., model checking) have been used separately from testing and have shown great potential when applied early in the development process. Still, these are confronted by applicability and scalability issues and work on specific modeling languages. The combined use of MBT and analysis techniques can support engineers in using both dynamic and static techniques. This paper proposes a hybrid approach by combining MBT using GraphWalker (GW) with Model-Based Analysis using UPPAAL by transforming the GW model into UPPAAL timed automata and supporting a combined analysis and testing process. The approach enables the automatic verification of both reachability and deadlock freedom properties to exploit the results obtained from this analysis step to improve the test model before generating and executing test cases on the system under test. The proposed approach can improve the combination of analysis and testing using a promising open-source MBT tool and is currently being evaluated in the context of actual use cases.

Wed 7 Dec

Displayed time zone: Osaka, Sapporo, Tokyo change

13:00 - 14:00
Model Checking 1Technical Track / ERA - Early Research Achievements at Room3
Chair(s): Hiroyuki Nakagawa Osaka University
13:00
20m
Paper
Bisection Value Iteration
Technical Track
Jia Lu East China Normal University, Ming Xu East China Normal University
13:20
20m
Paper
Non-Intrusive Annotation-Based Domain-Specific Analysis to Certify Event-B Models Behaviours
Technical Track
Ismail Mendil INPT-ENSEEIHT/IRIT, Peter Rivière INPT-ENSEEIHT / IRIT, University of Toulouse, France, Yamine Ait Ameur IRIT/INPT-ENSEEIHT, Neeraj Singh INPT-ENSEEIHT / IRIT, University of Toulouse, France, Dominique Mery Université de Lorraine, LORIA, Philippe Palanque ICS-IRIT, Université Toulouse III Paul Sabatier
13:40
15m
Paper
Combining Model-Based Testing and Automated Analysis of Behavioural Models using GraphWalker and UPPAAL
ERA - Early Research Achievements
Saurabh Tiwari DA-IICT Gandhinagar, Parv Shah DA-IICT Gandhinagar, India, Eduard Paul Enoiu Mälardalen University