Abstract
“Testing can be quite effective for showing the presence of bugs, but is hopelessly inadequate for showing their absence”. This famous remark, which was made by Dijkstra, has often been used to indicate a dichotomy between testing and verification. From a practitioner’s point of view, however, there is not much difference in the ways testing and verification techniques may be used in practice. While engineers would try to demonstrate that their systems are correct (verification), they often find themselves in a situation where they have to prioritize bug finding (testing). As a result, the choice to go for formal verification versus testing is largely driven by the practical needs and the context specificities. In this keynote, I will focus on search-based software testing (SBST) and review some recent research that combines ideas from the SBST and the formal verification communities to improve the analysis of models of cyber physical systems (CPS). I will present an empirical study that compares CPS model testing and verification, a search-based testing approach for compute-intensive CPS models that builds on a well-known formal verification framework, and a technique to automatically generate formal environment assumptions for CPS models using search algorithms and genetic programming.
This short paper provides an outline of the keynote talk given by Shiva Nejati at SSBSE 2020.
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
Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_25
Bittanti, S.: Model Identification and Data Analysis. Wiley, New York (2019)
Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Design 19(1), 7–34 (2001)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Cohen, M.B.: The maturation of search-based software testing: successes and challenges. In: Gorla, A., Rojas, J.M. (eds.) Proceedings of the 12th International Workshop on Search-Based Software Testing, SBST@ICSE 2019, Montreal, QC, Canada, 27 May 2019, pp. 13–14. IEEE/ACM (2019). https://doi.org/10.1109/SBST.2019.00013
Colanzi, T.E., Assunção, W.K.G., Farah, P.R., Vergilio, S.R., Guizzo, G.: A review of ten years of the symposium on search-based software engineering. In: Nejati, S., Gay, G. (eds.) SSBSE 2019. LNCS, vol. 11664, pp. 42–57. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-27455-9_4
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238–252. ACM (1977). https://doi.org/10.1145/512950.512973
Gaaloul, K., Menghi, C., Nejati, S., Briand, L., Wolfe, D.: Mining assumptions for software components using machine learning. In: Foundations of Software Engineering ESEC/SIGSOFT FSE 2020. ACM (2020)
Giannakopoulou, D., P"s"reanu, C.S., Barringer, H.: Assumption generation for software component verification. In: Proceedings of the 17th IEEE International Conference on Automated Software Engineering, ASE 2002, p. 3. IEEE Computer Society (2002)
Li, W., Dworkin, L., Seshia, S.A.: Mining assumptions for synthesis. In: International Conference on Formal Methods and Models, pp. 43–50. IEEE (2011)
Matinnejad, R., Nejati, S., Briand, L.C., Bruckmann, T.: Test generation and test prioritization for Simulink models with dynamic behavior. IEEE Trans. Software Eng. 45(9), 919–944 (2019). https://doi.org/10.1109/TSE.2018.2811489
Menghi, C., Nejati, S., Briand, L.C., Parache, Y.I.: Approximation-refinement testing of compute-intensive cyber-physical models: An approach based on system identification. In: International Conference on Software Engineering (ICSE). arXiv (2020)
Nejati, S., Gaaloul, K., Menghi, C., Briand, L.C., Foster, S., Wolfe, D.: Evaluating model testing and model checking for finding requirements violations in Simulink models. In: Dumas, M., Pfahl, D., Apel, S., Russo, A. (eds.) Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2019, Tallinn, Estonia, 26–30 August 2019, pp. 1015–1025. ACM (2019)
Zeller, A.: Search-based testing and system testing: a marriage in heaven. In: 10th IEEE/ACM International Workshop on Search-Based Software Testing, SBST@ICSE 2017, Buenos Aires, Argentina, 22–23 May 2017, pp. 49–50. IEEE (2017). https://doi.org/10.1109/SBST.2017.3
Acknowledgment
This work is supported by NSERC of Canada under the Discovery program.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Nejati, S. (2020). Search-Based Software Testing for Formal Software Verification – and Vice Versa. In: Aleti, A., Panichella, A. (eds) Search-Based Software Engineering. SSBSE 2020. Lecture Notes in Computer Science(), vol 12420. Springer, Cham. https://doi.org/10.1007/978-3-030-59762-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-59762-7_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-59761-0
Online ISBN: 978-3-030-59762-7
eBook Packages: Computer ScienceComputer Science (R0)