...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>The Journal of Systems and Software >Heterogeneous formal specification based on Object-Z and statecharts: semantics and verification
【24h】

Heterogeneous formal specification based on Object-Z and statecharts: semantics and verification

机译：基于Object-Z和状态图的异构形式规范：语义和验证

获取原文
获取原文并翻译 | 示例
   

获取外文期刊封面封底 >>

       
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This work presents a specification language, called OZS, based on two formalisms: Object-Z and the statecharts. Such a specification style facilitates the modeling of systems with both reactive and functional aspects. The accent is placed on OZS semantics so as to give formal foundations to verification and simulation of OZS models. Every OZS model has a transition system as its semantic interpretation. Untimed and timed versions of the OZS semantics are presented. Both transition system models of an OZS class can be used for verification purposes by model checking. In this work, a real-word example is treated and the resulting specification is model-checked by using the Stanford Temporal Prover environment from Stanford.
机译：这项工作基于两种形式主义提出了一种称为OZS的规范语言：Object-Z和状态图。这种规范样式有助于对具有反应性和功能性方面的系统进行建模。重音放在OZS语义上，以便为OZS模型的验证和仿真提供正式的基础。每个OZS模型都有一个过渡系统作为其语义解释。介绍了OZS语义的未定时版本和定时版本。 OZS类的两个转换系统模型都可以通过模型检查用于验证目的。在这项工作中，将使用Stanford的Stanford Temporal Prover环境来处理一个真实单词的示例，并对所得到的规范进行模型检查。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号