Abstract
This paper describes how static analyses can be applied to microcontroller assembly code to tackle the state explosion problem arising from explicit state model checking. It presents difficulties, which occur when trying to apply static analyses to microcontroller assembly code, caused by, for example, interrupts, hardware dependency, recursions, and indirect control. Enhancements of two reduction techniques (namely Dead Variable Reduction and Path Reduction) and their underlying static analyses are detailed, which make these techniques applicable to microcontroller assembly code. A short case study is presented in which five programs are used to demonstrate the state space reductions that can be achieved using these two techniques.
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
Preview
Unable to display preview. Download preview PDF.
References
Mehler, T.: Challenges and Applications of Assembly-Level Software Model Checking. PhD thesis, Universität Dortmund (2005)
Mercer, E.G., Jones, M.D.: Model checking machine code with the gnu debugger. In: SPIN Workshop on Model Checking of Software, San Francisco, USA (August 2005)
Schlich, B., Kowalewski, S.: [mc]square: A model checker for microcontroller code. In: Margaria, T., Philippou, A., Steffen, B. (eds.) Proc. 2nd Int’l Symp. Leveraging Applications of Formal Methods, Verification and Validation (IEEE-ISoLA 2006) (2006); To appear in: IEEE proceedings
Schlich, B., Rohrbach, M., Weber, M., Kowalewski, S.: Model checking software for microcontrollers. Technical Report AIB-2006-11, RWTH Aachen University (August 2006)
Balakrishnan, G., Reps, T., Melski, D., Teitelbaum, T.: Wysinwyx: What you see is not what you execute. In: Verified Software: Theories, Tools, Experiments. Springer, Heidelberg (to appear, 2007)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Schlich, B., Kowalewski, S.: An extendable architecture for model checking hardware-specific automotive microcontroller code. In: Schnieder, E., Tarnai, G. (eds.) Proc. 6th Symp. Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2007), Braunschweig, Germany, GZVB, pp. 202–212 (2007)
Schlich, B., Kowalewski, S.: Model checking c source code for embedded systems. In: Margaria, T., Steffen, B., Hinchey, M.G. (eds.) Proc. IEEE/NASA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation (IEEE/NASA ISoLA 2005), Maryland, USA, NASA, September 2005, pp. 65–77 (2005); NASA/CP-2005-212788
Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structure and state-space reduction. In: Proc. 18th IEEE Real-Time Systems Symposium (RTSS 1997), pp. 14–24. IEEE Computer Society, Washington, DC, USA (1997)
Heljanko, K.: Model checking the branching time temporal logic ctl. Research Report A45, Helsinki University of Technology (May 1997)
Vergauwen, B., Lewi, J.: A linear local model checking algorithm for ctl. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 447–461. Springer, Heidelberg (1993)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)
Yorav, K., Grumberg, O.: Static analysis for state-space reductions preserving temporal logics. Form. Methods Syst. Des. 25(1), 67–96 (2004)
Quirós, G.: Static byte-code analysis for state space reduction. Master’s thesis, RWTH Aachen University (March 2006)
Holzmann, G.J.: The engineering of a model checker: The gnu i-protocol case study revisited. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 232–244. Springer, Heidelberg (1999)
Lewis, M., Jones, M.: A dead variable analysis for explicit model checking. In: Proc. 2006 ACM SIGPLAN Symp. Partial evaluation and semantics-based program manipulation (PEPM 2006), pp. 48–57. ACM Press, New York (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schlich, B., Löll, J., Kowalewski, S. (2008). Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code. In: Leue, S., Merino, P. (eds) Formal Methods for Industrial Critical Systems. FMICS 2007. Lecture Notes in Computer Science, vol 4916. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79707-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-79707-4_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79706-7
Online ISBN: 978-3-540-79707-4
eBook Packages: Computer ScienceComputer Science (R0)