Wang, ShaohuiDwarakanathan, SrinivasanSokolsky, OlegLee, Insup2023-05-222023-05-222012-01-012012-01-18https://repository.upenn.edu/handle/20.500.14332/7938We study the problem of extracting high-level state machine models from software source code. Our target domain is GUI-driven applications for small hand-held devices such as cell phones and PDAs. In such systems, a natural high-level model is captured by a state machine, where states are GUI screens and button/menu item tappings are actions that trigger transitions between states. The paper presents a symbolic execution technique that allows us to identify states and transitions from the application source code. We discuss an implementation of this technique that operates on a large subset of the C# language and apply as a case study to the subsystem of a decision support tool for medical diagnosis.Model based verificationmodel extractionsymbolic executionstatic program analysisGUI-driven applicationsReport