Abstract
The use of formal methods in software engineering imparts a high degree of rigor and precision on the software development process. While formal methods are crucial for ensuring system dependability, their practical adoption has been limited in part due to scalability concerns, even though many automated analysis tools are available. In this paper, we address the scalability challenge in one type of formal analysis approach, model-finding. Prior work on EvoAlloy has demonstrated the potential for extending the Alloy Analyzer with an evolutionary algorithm by loosening the completeness guarantee while preserving soundness. However, that approach was evaluated on a small set of programs and failed to find many small-scope models that Alloy can find. In this work we introduce a new technique, called AdaptiveAlloy, which uses a novel adaptive fitness function for the analysis of Alloy relational logic specifications. Through our experiments, we illustrate that AdaptiveAlloy is capable of finding models of higher scope, and achieving greater scalability than both EvoAlloy and a state-of-the-art Alloy analyzer.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Alloy toolset. https://alloytools.org. Accessed Apr 2024
Alhanahnah, M., Stevens, C., Bagheri, H.: Scalable analysis of interaction threats in IoT systems. In: ISSTA, pp. 272–285 (2020)
Almulla, H., Gay, G.: Learning how to search: generating effective test cases through adaptive fitness function selection. Empir. Softw. Eng. 27(2), 38 (2022). https://doi.org/10.1007/s10664-021-10048-8
Bagheri, H., Kang, E., Malek, S., Jackson, D.: A formal approach for detection of security flaws in the Android permission system. FAOC 30, 525–544 (2018)
Bagheri, H., Malek, S.: Titanium: efficient analysis of evolving alloy specifications. In: FSE, pp. 27–38 (2016)
Bagheri, H., Wang, J., Aerts, J., Malek, S.: Efficient, evolutionary security analysis of interacting Android apps. In: ICSME, pp. 357–368. IEEE (2018)
Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: The electrum analyzer: model checking relational first-order temporal specifications. In: ASE (2018)
Dinges, P., Agha, G.A.: Solving complex path conditions through heuristic search on induced polytopes. In: Proceedings of FSE, pp. 425–436 (2014)
Galeotti, J.P., Rosner, N., López Pombo, C.G., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: ISSTA, pp. 25–36 (2010)
Godefroid, P., Khurshid, S.: Exploring very large state spaces using genetic algorithms. Int. J. Softw. Tools Technol. Transf. 6(2), 117–127 (2004)
Harman, M., Mansouri, S.A., Zhang, Y.: Search-based software engineering: trends, techniques and applications. ACM Comput. Surv. 45(1), 11:1–11:61 (2012)
Jackson, D.: Software Abstractions, 2nd edn. MIT Press (2012)
Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. FMSD 55, 1–32 (2019)
Mirzaei, N., Garcia, J., Bagheri, H., Sadeghi, A., Malek, S.: Reducing combinatorics in GUI testing of Android applications. In: ICSE, pp. 559–570 (2016)
Nelson, T., Saghafi, S., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: Aluminum: principled scenario exploration through minimality. In: ICSE, pp. 232–241 (2013)
Soltana, G., Sabetzadeh, M., Briand, L.C.: Practical constraint solving for generating system test data. TOSEM 29(2), 11:1–11:48 (2020). https://doi.org/10.1145/3381032
Stevens, C., Bagheri, H.: Reducing run-time adaptation space via analysis of possible utility bounds. In: ICSE, pp. 1522–1534. ACM (2020). https://doi.org/10.1145/3377811.3380365
Stevens, C., Bagheri, H.: Combining solution reuse and bound tightening for efficient analysis of evolving systems. In: ISSTA, pp. 89–100 (2022)
Stevens, C., Bagheri, H.: Parasol: efficient parallel synthesis of large model spaces. In: ESEC/FSE, pp. 620–632. ACM (2022). https://doi.org/10.1145/3540250.3549157
Thomé, J., Shar, L.K., Bianculli, D., Briand, L.C.: Search-driven string constraint solving for vulnerability detection. In: ICSE, pp. 198–208 (2017)
Torlak, E.: A constraint solver for software engineering: finding models and cores of large relational specifications. Ph.D. thesis, MIT, February 2009
Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_49
Wang, J., Bagheri, H., Cohen, M.B.: An evolutionary approach for analyzing alloy specifications. In: ASE, pp. 820–825 (2018)
Wang, J., Stevens, C., Kidmose, B., Cohen, M.B., Bagheri, H.: AdaptiveAlloy webpage, May 2024. https://sites.google.com/view/adaptivealloy
Wang, W., Wang, K., Gligoric, M., Khurshid, S.: Incremental analysis of evolving alloy models. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 174–191. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_10
Wilhelmstötter, F.: Jenetics (2021). http://jenetics.io
Wu, N., Simpson, A.C.: Formal relational database design: an exercise in extending the formal template language. FAOC 26(6), 1231–1269 (2014). https://doi.org/10.1007/S00165-014-0299-6
Zheng, G., Bagheri, H., Rothermel, G., Wang, J.: Platinum: reusing constraint solutions in bounded analysis of relational logic. In: FASE 2020. LNCS, vol. 12076, pp. 29–52. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45234-6_2
Acknowledgment
We thank the anonymous reviewers for their valuable comments. This work was supported in part by National Science Foundation awards CCF-1618132, CCF-1755890, CCF-1909688, CCF-2139845, and CCF-2124116.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Wang, J., Stevens, C., Kidmose, B., Cohen, M.B., Bagheri, H. (2024). Evolutionary Analysis of Alloy Specifications with an Adaptive Fitness Function. In: Jahangirova, G., Khomh, F. (eds) Search-Based Software Engineering. SSBSE 2024. Lecture Notes in Computer Science, vol 14767. Springer, Cham. https://doi.org/10.1007/978-3-031-64573-0_1
Download citation
DOI: https://doi.org/10.1007/978-3-031-64573-0_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-64572-3
Online ISBN: 978-3-031-64573-0
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science