publication . Preprint . 2017

Modular Verification of Interrupt-Driven Software

Sung, Chungha; Kusano, Markus; Wang, Chao;
Open Access English
  • Published: 28 Sep 2017
Abstract
Interrupts have been widely used in safety-critical computer systems to handle outside stimuli and interact with the hardware, but reasoning about interrupt-driven software remains a difficult task. Although a number of static verification techniques have been proposed for interrupt-driven software, they often rely on constructing a monolithic verification model. Furthermore, they do not precisely capture the complete execution semantics of interrupts such as nested invocations of interrupt handlers. To overcome these limitations, we propose an abstract interpretation framework for static verification of interrupt-driven software that first analyzes each interru...
Subjects
free text keywords: Computer Science - Programming Languages, Computer Science - Software Engineering
Funded by
NSF| SHF: Small: Program Analysis-based Makeover for HPC Application Resilience
Project
  • Funder: National Science Foundation (NSF)
  • Project Code: 1722710
  • Funding stream: Directorate for Computer & Information Science & Engineering | Division of Computing and Communication Foundations
,
NSF| CAREER: Automated Concurrency Debugging ? An Essential Ingredient for Safety-Critical Software Assurance and Security
Project
  • Funder: National Science Foundation (NSF)
  • Project Code: 1149454
  • Funding stream: Directorate for Computer & Information Science & Engineering | Division of Computing and Communication Foundations
Download from
45 references, page 1 of 3

[1] Vikram Adve, Chris Lattner, Michael Brukman, Anand Shukla, and Brian Gaeke. LLVA: A Low-level Virtual Instruction Set Architecture. In ACM/IEEE international symposium on Microarchitecture, 2003.

[2] Martin Bravenboer and Yannis Smaragdakis. Strictly declarative specification of sophisticated points-to analyses. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages, and Applications, pages 243-262, 2009. [OpenAIRE]

[3] Doina Bucur and Marta Kwiatkowska. On software verification for sensor nodes. Journal of Systems and Software, 84(10):1693-1707, 2011.

[4] E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 168-176, 2004. [OpenAIRE]

[5] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 238-252, 1977.

[6] Patrick Cousot, Radhia Cousot, Je´r oˆme Feret, Laurent Mauborgne, Antoine Mine´, David Monniaux, and Xavier Rival. The ASTRE E´ analyzer. In European Symposium on Programming Languages and Systems, pages 21-30, 2005.

[7] Azadeh Farzan and Zachary Kincaid. Verification of parameterized concurrent programs by modular reasoning about data and control. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 297-308, 2012. [OpenAIRE]

[8] Jeanne Ferrante, Karl J. Ottenstein, and Joe D. Warren. The program dependence graph and its use in optimization. ACM Transactions on Programming Languages and Systems, 9(3):319-349, July 1987. [OpenAIRE]

[9] Shengjian Guo, Markus Kusano, and Chao Wang. Conc-iSE: Incremental symbolic execution of concurrent software. In IEEE/ACM International Conference On Automated Software Engineering, 2016. [OpenAIRE]

[10] Shengjian Guo, Markus Kusano, Chao Wang, Zijiang Yang, and Aarti Gupta. Assertion guided symbolic execution of multithreaded programs. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 854-865, 2015.

[11] Shengjian Guo, Meng Wu, and Chao Wang. Symbolic execution of programmable logic controller code. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 326-336, 2017.

[12] Makoto Higashi, Tetsuo Yamamoto, Yasuhiro Hayase, Takashi Ishio, and Katsuro Inoue. An effective method to control interrupt handler for data race detection. In Proceedings of the 5th Workshop on Automation of Software Test, pages 79-86, 2010.

[13] Krystof Hoder, Nikolaj Bjørner, and Leonardo de Moura. muZ - an efficient engine for fixed points with constraints. In International Conference on Computer Aided Verification, pages 457-462, 2011. [OpenAIRE]

[14] The intAbs tool and benchmark programs for evaluating intAbs. URL: https://github.com/sch8906/intAbs.

[15] Franjo Ivancˇic´, I. Shlyakhter, Aarti Gupta, M.K. Ganai, V. Kahlon, Chao Wang, and Z. Yang. Model checking C program using F-Soft. In International Conference on Computer Design, pages 297-308, 2005.

45 references, page 1 of 3
Related research
Abstract
Interrupts have been widely used in safety-critical computer systems to handle outside stimuli and interact with the hardware, but reasoning about interrupt-driven software remains a difficult task. Although a number of static verification techniques have been proposed for interrupt-driven software, they often rely on constructing a monolithic verification model. Furthermore, they do not precisely capture the complete execution semantics of interrupts such as nested invocations of interrupt handlers. To overcome these limitations, we propose an abstract interpretation framework for static verification of interrupt-driven software that first analyzes each interru...
Subjects
free text keywords: Computer Science - Programming Languages, Computer Science - Software Engineering
Funded by
NSF| SHF: Small: Program Analysis-based Makeover for HPC Application Resilience
Project
  • Funder: National Science Foundation (NSF)
  • Project Code: 1722710
  • Funding stream: Directorate for Computer & Information Science & Engineering | Division of Computing and Communication Foundations
,
NSF| CAREER: Automated Concurrency Debugging ? An Essential Ingredient for Safety-Critical Software Assurance and Security
Project
  • Funder: National Science Foundation (NSF)
  • Project Code: 1149454
  • Funding stream: Directorate for Computer & Information Science & Engineering | Division of Computing and Communication Foundations
Download from
45 references, page 1 of 3

[1] Vikram Adve, Chris Lattner, Michael Brukman, Anand Shukla, and Brian Gaeke. LLVA: A Low-level Virtual Instruction Set Architecture. In ACM/IEEE international symposium on Microarchitecture, 2003.

[2] Martin Bravenboer and Yannis Smaragdakis. Strictly declarative specification of sophisticated points-to analyses. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages, and Applications, pages 243-262, 2009. [OpenAIRE]

[3] Doina Bucur and Marta Kwiatkowska. On software verification for sensor nodes. Journal of Systems and Software, 84(10):1693-1707, 2011.

[4] E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 168-176, 2004. [OpenAIRE]

[5] Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 238-252, 1977.

[6] Patrick Cousot, Radhia Cousot, Je´r oˆme Feret, Laurent Mauborgne, Antoine Mine´, David Monniaux, and Xavier Rival. The ASTRE E´ analyzer. In European Symposium on Programming Languages and Systems, pages 21-30, 2005.

[7] Azadeh Farzan and Zachary Kincaid. Verification of parameterized concurrent programs by modular reasoning about data and control. In ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 297-308, 2012. [OpenAIRE]

[8] Jeanne Ferrante, Karl J. Ottenstein, and Joe D. Warren. The program dependence graph and its use in optimization. ACM Transactions on Programming Languages and Systems, 9(3):319-349, July 1987. [OpenAIRE]

[9] Shengjian Guo, Markus Kusano, and Chao Wang. Conc-iSE: Incremental symbolic execution of concurrent software. In IEEE/ACM International Conference On Automated Software Engineering, 2016. [OpenAIRE]

[10] Shengjian Guo, Markus Kusano, Chao Wang, Zijiang Yang, and Aarti Gupta. Assertion guided symbolic execution of multithreaded programs. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 854-865, 2015.

[11] Shengjian Guo, Meng Wu, and Chao Wang. Symbolic execution of programmable logic controller code. In ACM SIGSOFT Symposium on Foundations of Software Engineering, pages 326-336, 2017.

[12] Makoto Higashi, Tetsuo Yamamoto, Yasuhiro Hayase, Takashi Ishio, and Katsuro Inoue. An effective method to control interrupt handler for data race detection. In Proceedings of the 5th Workshop on Automation of Software Test, pages 79-86, 2010.

[13] Krystof Hoder, Nikolaj Bjørner, and Leonardo de Moura. muZ - an efficient engine for fixed points with constraints. In International Conference on Computer Aided Verification, pages 457-462, 2011. [OpenAIRE]

[14] The intAbs tool and benchmark programs for evaluating intAbs. URL: https://github.com/sch8906/intAbs.

[15] Franjo Ivancˇic´, I. Shlyakhter, Aarti Gupta, M.K. Ganai, V. Kahlon, Chao Wang, and Z. Yang. Model checking C program using F-Soft. In International Conference on Computer Design, pages 297-308, 2005.

45 references, page 1 of 3
Related research
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue