Abstract
Firmware verification for small and medium industries is a challenging task; as a matter of fact, they generally do not have personnel dedicated to such activity. In this context, verification is executed very late in the design flow, and it is usually carried on by the same engineers involved in coding and testing. The specifications initially discussed with the customers are generally not formalised, leading to ambiguity in the expected functionalities. The adoption of a more formal design flow would require the recruitment of people with expertise in formal and semi-formal verification, which is not often compatible with the budget resources of small and medium industries. The alternative is helping the existing engineers with tools and methodologies they can easily adopt without being experts in formal methods.
The paper follows this direction by presenting MIST, a framework for the automatic generation of an assertion-based verification environment and its integrated execution inside an off-the-shelf industrial design tool. In particular, MIST allows generating a complete environment to verify C/C++ firmware starting from informal specifications.
Given a set of specifications written in natural language, the tool guides the user in translating each specification into an XML formal description, capturing a temporal behaviour that must hold in the design. Our XML format guarantees the same expressiveness of linear temporal logic, but it is designed to be used by designers that are not familiar with formal methods. Once each behaviour is formalised, MIST automatically generates the corresponding testbench and checker to stimulate and verify the design. To guide the verification process, MIST employs a clustering procedure that classifies the internal states of the firmware. Such classification aims at finding an effective ordering to check the expected behaviours and to advise for possible specification holes.
MIST has been fully integrated into the IAR System EmbeddedWorkbench. Its effectiveness and efficiency have been evaluated to formalise and check a complex test plan for industrial firmware.
The research has been partially supported by the project “Dipartimenti di Eccellenza 2018–2022” funded by the Italian Ministry of Education, Universities and Research (MIUR); and with the collaboration of IDEA S.p.a.
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
Shamal, P.K., Rahamathulla, K., Akbar, A.: A study on software vulnerability prediction model. In: 2017 International Conference on Wireless Communications, Signal Processing and Networking (WiSPNET), pp. 703–706 (2017)
Nagappan, N., Ball, T.: Static analysis tools as early indicators of pre-release defect density, pp. 580–586, June 2005
Dawson, M., Burrell, D., Rahim, E., Brewster, S.: Integrating software assurance into the software development life cycle (SDLC). J. Inf. Syst. Technol. Plann. 3, 49–53 (2010)
Zhivich, M., Cunningham, R.K.: The real cost of software errors. IEEE Secur. Priv. 7(2), 87–90 (2009)
Jørgensen, M., Teigen, K., Moløkken-Østvold, K.: Better sure than safe? Over-confidence in judgement based software development effort prediction intervals. J. Syst. Softw. 70, 79–93 (2004)
Oyetoyan, T.D., Milosheska, B., Grini, M., Soares Cruzes, D.: Myths and facts about static application security testing tools: an action research at Telenor digital. In: Garbajosa, J., Wang, X., Aguiar, A. (eds.) XP 2018. LNBIP, vol. 314, pp. 86–103. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91602-6_6
Osman, M.H., Zaharin, M.F.: Ambiguous software requirement specification detection: an automated approach. In: 2018 IEEE/ACM 5th International Workshop on Requirements Engineering and Testing (RET), pp. 33–40 (2018)
Moketar, N.A., Kamalrudin, M., Sidek, S., Robinson, M., Grundy, J.: An automated collaborative requirements engineering tool for better validation of requirements. In: 2016 31st IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 864–869 (2016)
Kakiuchi, Y., Kitajima, A., Hamaguchi, K., Kashiwabara, T.: Automatic monitor generation from regular expression based specifications for module interface verification. In: 2005 IEEE International Symposium on Circuits and Systems, vol. 4, pp. 3555–3558 (2005)
Subramanyan, P., Malik, S., Khattri, H., Maiti, A., Fung, J.: Architecture of a tool for automated testing the worst-case execution time of real-time embedded systems firmware. In: 2016 Design Automation & Test in Europe Conference & Exhibition (DATE), pp. 337–342 (2016)
Buzhinsky, I.: Formalization of natural language requirements into temporal logics: a survey. In: 2019 IEEE 17th International Conference on Industrial Informatics (INDIN), pp. 400–406 (2019)
IEEE standard for property specification language (PSL). IEEE Std. 1850-2010 (Revision of IEEE Std. 1850-2005), pp. 1–182 (2010)
IEEE standard for systemverilog-unified hardware design, specification, and verification language - redline. IEEE Std. 1800-2009 (Revision of IEEE Std. 1800-2005) - Redline, pp. 1–1346 (2009)
Yang, S., Wille, R., Drechsler, R.: Improving coverage of simulation-based verification by dedicated stimuli generation. In: Formal Methods in Computer Aided Design, pp. 599–606 (2014)
Zhao, Y., Bian, J., Deng, S., Kong, Z.: Random stimulus generation with self-tuning. In: 13th International Conference on Computer Supported Cooperative Work in Design, pp. 62–65 (2009)
Cadar, C., Dunbar, D., Engler, D.R., et al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, vol. 8, pp. 209–224 (2008)
Agbaria, S., Carmi, D., Cohen, O., Korchemny, D., Lifshits, M., Nadel, A.: SAT-based semiformal verification of hardware. In: Formal Methods in Computer Aided Design, pp. 25–32 (2010)
Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0—a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_8
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 IFIP International Federation for Information Processing
About this paper
Cite this paper
Germiniani, S., Bragaglio, M., Pravadelli, G. (2021). From Informal Specifications to an ABV Framework for Industrial Firmware Verification. In: Calimera, A., Gaillardon, PE., Korgaonkar, K., Kvatinsky, S., Reis, R. (eds) VLSI-SoC: Design Trends. VLSI-SoC 2020. IFIP Advances in Information and Communication Technology, vol 621. Springer, Cham. https://doi.org/10.1007/978-3-030-81641-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-81641-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-81640-7
Online ISBN: 978-3-030-81641-4
eBook Packages: Computer ScienceComputer Science (R0)
