Abstract
Testing and Bounded Model Checking (BMC) are two techniques used in Software Verification for bug-hunting. They are expression of two different philosophies: testing is used on the compiled code and it is more suited to find errors in common behaviors, while BMC is used on the source code to find errors in uncommon behaviors of the system. Nowadays, testing is by far the most used technique for software verification in industry: it is easy to use and even when no error is found, it can release a set of tests certifying the (partial) correctness of the compiled system. In the case of safety critical software, in order to increase the confidence of the correctness of the compiled system, it is often required that the provided set of tests covers 100% of the code. This requirement, however, substantially increases the costs associated to the testing phase, since it often involves the manual generation of tests. In this paper we show how BMC can be productively applied to the Software Verification process in industry. In particular, we show how to productively use a Bounded Model Checker for C programs (CBMC) as an automatic test generator for the Coverage Analysis of Safety Critical Software. In particular, we experimented CBMC on a subset of the modules of the European Train Control System (ETCS) of the European Rail Traffic Management System (ERTMS) source code, an industrial system for the control of the traffic railway, provided by Ansaldo STS. The Code of the ERTMS/ETCS, with thousands of lines, has been used as trial application with CBMC obtaining a set of tests satisfying the target 100% code coverage, requested by the CENELEC EN50128 guidelines for software development of safety critical systems. The use of CBMC for test generation led to a dramatic increase in the productivity of the entire Software Development process by substantially reducing the costs of the testing phase. To the best of our knowledge, this is the first time that BMC techniques have been used in an industrial setting for automatically generating tests achieving full coverage of Safety-Critical Software. The positive results demonstrate the maturity of Bounded Model Checking techniques for automatic test generation in industry.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating Tests from Counterexamples. In: ICSE, pp. 326–335. IEEE Computer Society (2004)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 118–149 (2003)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, R. (ed.) TACAS. Lecture Notes in Computer Science, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Black, P.E., Ammann, P., Ding, W., N. I. of Standards, T. (U.S.): Model checkers in software testing. U.S. Dept. of Commerce, Technology Administration, National Institute of Standards and Technology, Gaithersburg (2002)
Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) OSDI, pp. 209–224. USENIX Association (2008)
Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M.Y.: A practical approach to coverage in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer aided verification. 13th international conference, CAV 2001, Paris, France, 18–22 July 2001, Proceedings. Lecture Notes in Computer Science, vol. 2102, pp. 66–78. Springer, Heidelberg (2001)
Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and Complexity of Bounded Model Checking. In: Steffen, B., Levi, G. (eds.) VMCAI. Lecture Notes in Computer Science, vol. 2937, pp. 85–96. Springer (2004)
Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: DAC, pp. 368–371. ACM (2003)
Cooper, D.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds) Machine Intelligence, vol. 7. Edinburgh University Press, Edinburgh (1972)
Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer aided verification. 13th international conference, CAV 2001, Paris, France, 18–22 July 2001, Proceedings. Lecture Notes in Computer Science, vol. 2102, pp. 436–453. Springer, Heidelberg (2001)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)
de Halleux, J., Tillmann, N.: Parameterized unit testing with Pex. In: Beckert, B., Hähnle, R. (eds.) Tests and proofs, second international conference, TAP 2008, Prato, Italy, 9–11 April 2008. Proceedings. In: Lecture Notes in Computer Science, vol. 4966, pp. 171–181. Springer, Heidelberg (2008)
de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R. Rehof, J. (eds.) TACAS. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Deason, W.H., Brown, D.B., Chang, K.-H., Cross, J.H.: A rule-based software test data generator. IEEE Trans. Knowl. Data Eng. 3(1), 108–117 (1991)
EC: European committee for electrotechnical standardization. In: Railway Applications—Communication, Signalling and Processing Systems - Software for Railway Control and Protection Systems (2008)
Edvardsson, J.: A survey on automatic test data generation. In: Proceedings of the Second Conference on Computer Science and Engineering in Linköping. pp. 21–28 (1999)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT. Lecture Notes in Computer Science, vol. 2919, pp. 502–518. Springer, Heidelberg (2003)
ERTMS: The official Website: http://www.ertms.com/
Ferguson, R., Korel, B.: The chaining approach for software test data generation. ACM Trans. Softw. Eng. Methodol. 5(1), 63–86 (1996)
Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) PLDI, pp. 213–223. ACM (2005)
Jackson, D., Shlyakhter, I., Sridharan, M.: A micromodularity mechanism. In: ESEC/SIGSOFT FSE, pp. 62–73 (2001)
Khurshid, S., Marinov, D.: TestEra: specification-based testing of java programs using SAT. Autom. Softw. Eng. 11(4), 403–434 (2004)
Meudec, C.: ATGen: automatic test data generation using constraint logic programming and symbolic execution. Softw. Test., Verif. Reliab. 11(2), 81–96 (2001)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC, pp. 530–535. ACM (2001)
Offutt, A.J., Hayes, J.H.: A semantic model of program faults. In: ISSTA, pp. 195–200 (1996)
Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293–304 (1986)
Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 263–272 (2005)
Tillmann, N., de Halleux, J.: Pex-White box test generation for .NET. In: Beckert, B., Hähnle, R. (eds.) Tests and proofs, second international conference, TAP 2008, Prato, Italy, 9–11 April 2008. Proceedings. In: Lecture Notes in Computer Science, vol. 4966, pp. 134–153. Springer, Heidelberg (2008)
Tillmann, N., Schulte, W.: Parameterized unit tests. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 253–262 (2005)
Tracey, N., Clark, J.A., Mander, K.: Automated program flaw finding using simulated annealing. In: ISSTA, pp. 73–81 (1998)
Vedula, V.M., Abraham, J.A., Ambler, T.P., Aziz, A., Chase, C.M., Tupuri, R.S., Vedula, M.A., Tech, B.: HDL slicing for verification and test (2003)
Author information
Authors and Affiliations
Corresponding author
Additional information
Partially supported by a Ph.D. grant (2007–2009) financed by Ansaldo STS.
Rights and permissions
About this article
Cite this article
Angeletti, D., Giunchiglia, E., Narizzano, M. et al. Using Bounded Model Checking for Coverage Analysis of Safety-Critical Software in an Industrial Setting. J Autom Reasoning 45, 397–414 (2010). https://doi.org/10.1007/s10817-010-9172-3
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-010-9172-3