Abstract
Verification of embedded systems is challenging whenever control programs rely on black-box hardware components. Unless precise specifications of such components are fully available, learning their structured models is a powerful enabler for verification, but it can be inefficient when the system to be learned is data-intensive rather than control-intensive. We contribute a methodology to attack this problem based on a specific class of automata which are well suited to model systems wherein data paths are known to be decoupled from control paths. We test our approach by combining learning and verification to assess the correctness of grey-box programs relying on FIFO register circuitry to control an elevator system.
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
Notes
- 1.
- 2.
Notice that we consider only input and output symbols of arity one. This can be extended for arbitrary, but fixed a priori, number of parameters.
- 3.
All the experiments reported in this paper ran on an Intel i7 3.4Â GHz PC equipped with 32Â GB of RAM and running Ubuntu 14.04. The inference of the FIFO queue models is performed by AIDE using a simulator.
References
Howar, F., Steffen, B.: Learning models for verification and testing — special track at ISoLA 2014 track introduction. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8802, pp. 199–201. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45234-9_14
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)
Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineering and Distributed Systems. IFIP, vol. 28, pp. 225–240. Springer, Heidelberg (1999). doi:10.1007/978-0-387-35578-8_13
Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. Logic J. IGPL 14(5), 729–744 (2006)
Raffelt, H., Steffen, B., Berg, T., Margaria, T.: LearnLib: a framework for extrapolating behavioral models. Int. J. Softw. Tools Technol. Transfer (STTT) 11(5), 393–407 (2009)
Howar, F., Isberner, M., Steffen, B., Bauer, O., Jonsson, B.: Inferring semantic interfaces of data structures. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 554–571. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34026-0_41
Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)
Khalili, A., Tacchella, A.: Learning nondeterministic Mealy machines. In: Proceedings of the 12th International Conference on Grammatical Inference (ICGI), pp. 109–123 (2014)
Aarts, F.: Tomte: Bridging the Gap between Active Learning and Real-World Systems. Ph.D. thesis, Radboud University Nijmegen (2014)
Holzmann, G.J.: The model checker Spin. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)
Nagafuji, K., Yamaguchi, S.: Éclair: An elevator group controller model checking system based on s-ring and spin. In: 2014 IEEE 3rd Global Conference on Consumer Electronics (GCCE), pp. 178–181. IEEE (2014)
Attie, P.C., Lorenz, D.H., Portnova, A., Chockler, H.: Behavioral compatibility without state explosion: design and verification of a component-based elevator control system. In: Gorton, I., Heineman, G.T., Crnković, I., Schmidt, H.W., Stafford, J.A., Szyperski, C., Wallnau, K. (eds.) CBSE 2006. LNCS, vol. 4063, pp. 33–49. Springer, Heidelberg (2006). doi:10.1007/11783565_3
Gold, E.M.: System identification via state characterization. Automatica 8(5), 621–636 (1972)
Niese, O.: An Integrated Approach to Testing Complex Systems. Ph.D. thesis, Universität Dortmund, Dortmund, Germany (2003)
Shahbaz, M.: Reverse Engineering Enhanced State Models of Black Box Software Components to Support Integration Testing. Ph.D. thesis, Institut Polytechnique de Grenoble, Grenoble, France (2008)
Steffen, B., Howar, F., Merten, M.: Introduction to active automata learning from a practical perspective. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 256–296. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21455-4_8
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT press, Cambridge (1999)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, vol. 1003. Addison-Wesley, Reading (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Khalili, A., Narizzano, M., Tacchella, A. (2016). Learning for Verification in Embedded Systems: A Case Study. In: Adorni, G., Cagnoni, S., Gori, M., Maratea, M. (eds) AI*IA 2016 Advances in Artificial Intelligence. AI*IA 2016. Lecture Notes in Computer Science(), vol 10037. Springer, Cham. https://doi.org/10.1007/978-3-319-49130-1_38
Download citation
DOI: https://doi.org/10.1007/978-3-319-49130-1_38
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-49129-5
Online ISBN: 978-3-319-49130-1
eBook Packages: Computer ScienceComputer Science (R0)