Model generation by the exhaustive search for embedded assembly programs and application to model checking
Model generation by the exhaustive search for embedded assembly programs and application to model checking
复制标题
DOI：
10.1109/gcce.2014.7031136
复制
发表时间：
2014-10
期刊：
影响因子：
--
通讯作者：
Ryosuke Konoshita;K. Sakurai;S. Yamane
中科院分区：
文献类型：
--
作者：
Ryosuke Konoshita;K. Sakurai;S. Yamane
嵌入式系统得到了广泛的应用。因此，确保安全性非常重要。模型检验是保证系统安全性的有效手段。我们已经开发了行为提取器来自动建模嵌入式汇编程序的行为。该模型用于模型检查。此外，我们还引入了undefined值来减少状态的数量。
Embedded systems have been widely used. Therefore, it is important to ensure the safety. Model checking is effective to ensure the safety for systems. We have developed Behavior Extractor to model the behavior of embedded assembly programs automatically. The model is used for model checking. In addition, we have introduced the undefined value to reduce the number of states.