A formal approach to automatically analyse extra‐functional properties in mobile applications. (14th June 2019)

• Record Type: Journal Article
• Authors: Rosario Espada, Ana; del Mar Gallardo, Maria; Salmerón, Alberto; Panizo, Laura; Merino, Pedro
• Is Part Of: Software testing, verification & reliability. Volume 29:Number 4/5(2019)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2019-06-14
• Subjects: analysis of traces -- android -- extra‐functional properties -- model‐based testing -- verification; Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1699
• Languages: English
• ISSNs: 0960-0833

Abstract

Summary: This paper presents an integrated approach for testing mobile applications (apps) against a set of extra‐functional properties to be used by app developers. The approach starts with the (manual or automatic) extraction of the interaction model, that is, a formal model of the potential user interactions with the app. The model is constructed to allow a model checking tool to exhaustively extract the so‐called app user flows, that is, the sequences of user actions, that constitute the test cases. In the final step, the app user flows are executed on the app running on real devices. The resulting execution traces are enriched with different measures and verified against a set of extra‐functional properties of interest. The approach has been adapted to analyse several applications running at the same time with several devices supporting the applications. This paper presents the definition and formalization of both the modelling language for the interaction model and the specification language to represent the extra‐functional properties. It also describes a methodology for automatically extracting the model. Finally, it presents an implementation focused on Android apps, which is integrated in the TRIANGLE testing framework, and the evaluation of the approach. © 2019 The Authors. Software Testing, Verification & Reliability Published by John Wiley & Sons Ltd. Abstract : This paper presents an integrated approach for testing mobile apps against a set of extra‐functional properties defined by the developer. The process starts with the extraction of the possible interactions of the user with the app (interaction model). Then, a model‐checking tool extracts the app user flows, that is, the sequences of user actions. In the final step, the app user flows are executed on the app running on real devices and the execution traces are verified against the extra‐functional properties.