Runtime enforcers can be used to ensure that running applications satisfy desired correctness properties. Although runtime enforcers that are correct-by-construction with respect to abstract behavioral models are relatively easy to specify, the concrete software enforcers generated from these specifications may easily introduce issues in the target application. Indeed developers can generate test suites to verify the functional behavior of the enforcers, for instance exploiting the same models used to specify them. However, it remains challenging and tedious to verify the behavior of enforcers in terms of non-functional performance characteristics. This paper describes a practical approach to reveal runtime enforcers that may introduce inefficiencies in the target application. The approach relies on a combination of automatic test generation and runtime monitoring of multiple key performance indicators. We designed our approach to reveal issues in four indicators for mobile systems: responsiveness, launch time, memory, and energy consumption. Experimental results show that our approach can detect performance issues that might be introduced by automatically generated enforcers.
Riganelli, O., Micucci, D., Mariani, L. (2022). Non-functional Testing of Runtime Enforcers in Android. In Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22–30, 2022, Proceedings, Part I (pp.320-334). Springer Science and Business Media Deutschland GmbH [10.1007/978-3-031-19849-6_19].
Non-functional Testing of Runtime Enforcers in Android
Riganelli, O
;Micucci, D;Mariani, L
2022
Abstract
Runtime enforcers can be used to ensure that running applications satisfy desired correctness properties. Although runtime enforcers that are correct-by-construction with respect to abstract behavioral models are relatively easy to specify, the concrete software enforcers generated from these specifications may easily introduce issues in the target application. Indeed developers can generate test suites to verify the functional behavior of the enforcers, for instance exploiting the same models used to specify them. However, it remains challenging and tedious to verify the behavior of enforcers in terms of non-functional performance characteristics. This paper describes a practical approach to reveal runtime enforcers that may introduce inefficiencies in the target application. The approach relies on a combination of automatic test generation and runtime monitoring of multiple key performance indicators. We designed our approach to reveal issues in four indicators for mobile systems: responsiveness, launch time, memory, and energy consumption. Experimental results show that our approach can detect performance issues that might be introduced by automatically generated enforcers.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
