版权所有:内蒙古大学图书馆 技术提供:维普资讯• 智图
内蒙古自治区呼和浩特市赛罕区大学西街235号 邮编: 010021
作者机构:Univ Malaga GISUM Campus Teatinos S-N E-29071 Malaga Spain
出 版 物:《ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE》 (理论计算机科学电子札记)
年 卷 期:2007年第190卷第4期
页 面:33-48页
核心收录:
学科分类:08[工学] 0812[工学-计算机科学与技术(可授工学、理学学位)]
基 金:Spanish MEC [TIN2004-7943-C04] French Ministry of Foreign Affairs
主 题:data flow analysis model checking labeled transition system boolean equation system
摘 要:The combination of static and dynamic software analysis, such as data flow analysis (DFA) and model checking, provides benefits for both disciplines. On the one hand, the information extracted by DFAS about program data may be utilized by model checkers to optimize the state space representation. On the other hand, the expressiveness of logic formulas allows us to consider model checkers as generic data flow analyzers. Following this second approach, we propose in this paper an algorithm to calculate DFAS using on-the-fly resolution of boolean equation systems (BESS). The overall framework includes the abstraction of the input program into an implicit labeled transition system (LTS), independent of the program specification language. Moreover, using BESS as an intermediate representation allowed us to reformulate classical DFAS encountered in the literature, which were previously encoded in terms of mu-calculus formulas with forward and backward modalities. Our work was implemented and integrated into the widespread verification platform CADP, and experimented on real examples.