TAV-CPS/IoT 2019 – Proceedings

2019 ACM SIGSOFT International Workshop on Testing, Analysis, and Verification of Cyber-Physical Systems and Internet of Things (TAV-CPS/IoT 2019)

Symbolic Execution-Based Approach to Extracting a Micro State Transition Table
Takahiro Shimizu, Norihiro Yoshida, Ryota Yamamoto, and Hiroaki Takada
(Nagoya University, Japan)
During embedded system development, developers frequently change and reuse the existing C source code for the development of a new but behaviorally similar product. Such frequent changes generally decrease the understandability of C source code although the developers have to understand how it behaves and how to reuse it. So far, much research has been done on symbolic execution techniques that statically analyze the behavioral aspect of given source code. In this paper, we propose a symbolic execution-based approach to extracting a Micro State Transition Table (MSTT) that helps developers understanding the behavioral aspect of embedded C source code based on a fine-grained state transition model. As a case study, we applied the proposed approach to a collection of source files and then confirmed the correctness of the extracted MSTTs.

@InProceedings{TAV-CPS/IoT19p1, author = {Takahiro Shimizu and Norihiro Yoshida and Ryota Yamamoto and Hiroaki Takada}, title = {Symbolic Execution-Based Approach to Extracting a Micro State Transition Table}, booktitle = {Proc.\ TAV-CPS/IoT}, publisher = {ACM}, pages = {1--6}, doi = {10.1145/3341108.3342244}, year = {2019}, } Publisher's Version

proc time: 0.3