A Lesson on Verification of IoT Software with Frama-C
2018 International Conference on High Performance Computing & Simulation (HPCS)（2018）
摘要
This paper is a tutorial introduction to Frama- C, a framework for analysis and verification of C programs. We present value analysis, deductive verification and runtime verification of software using Frama-C and in particular its Eva, Wp, and E-Acsl plugins. These techniques are illustrated on examples coming from real-life verification case studies for different modules of Contiki, a lightweight operating system for the Internet of Things.
更多查看译文
关键词
IoT software,Frama- C,C programs,value analysis,deductive verification,E-Acsl plugins,runtime verification,internet of things,operating system,Eva plugins,Wp plugins
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要