• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Embedded Software and Systems(ICESS 2005); 20051216-18; Xi'an(CN) >Formalization of fFSM Model and Its Verification
【24h】

Formalization of fFSM Model and Its Verification

机译：fFSM模型的形式化及其验证

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

PeaCE(Ptolemy extension as a Codesign Environment) was developed for the hardware and software codesign framework which allows us to express both data flow and control flow. The fFSM is a model for describing the control flow aspects in PeaCE, but it has difficulties in verifying their specifications due to lack of their formality. Thus we propose the formal semantics of the model based on its execution steps. To verify an fFSM model, it is translated into SMV input language with properties to be checked, automatically. As a result, some important bugs such as race condition, ambiguous transition, and circular transition can be formally detected in the model.
机译：PeaCE（作为协同设计环境的Ptolemy扩展）是为硬件和软件代码签名框架开发的，它使我们能够表达数据流和控制流。 fFSM是用于描述PeaCE中的控制流方面的模型，但是由于缺乏形式化，因此难以验证其规格。因此，我们根据模型的执行步骤提出了模型的形式语义。为了验证fFSM模型，将其自动转换为具有要检查的属性的SMV输入语言。结果，可以在模型中正式检测到一些重要的错误，例如竞态条件，模糊转换和循环转换。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号