期刊文献+

有限构模器的扩展及其在形式化方法中的应用 被引量:1

Extensions to a Finite Model Generator and Application to Formal Methods
下载PDF
导出
摘要 规约在软件开发和验证中占有重要地位 .对于以一阶逻辑为基础的规约 ,可以利用有限模型构造技术对其执行并测试 .文中研究规约中某些特性的处理 ,包括存在量词以及二元关系的传递闭包 .对已有的一个构模工具进行扩充 。 Specifications play an important role in software development and verification. Logic based specifications can be executed and tested by finite model generation techniques. In this paper, some features of specifications are studied,including existential quantifiers and transitive closures of binary relations. An existing model generator is extended, and a few mistakes in the literature are identified.
作者 张健
出处 《计算机学报》 EI CSCD 北大核心 2000年第2期190-194,共5页 Chinese Journal of Computers
基金 国家自然科学基金!( 6970 3 0 14 ) 国家重点基础研究发展规划 (九七三 )( G19980 3 0 60 0 )
关键词 形式规约 软件开发 形式化方法 有限构模器 formal specifications, first order predicate logic, finite model construction, existential quantifiers, transitive closure
  • 引文网络
  • 相关文献

参考文献3

  • 1Zhang J,Proceedings 10th International Conference on Software En-gineering and Knowledge,1998年,90页
  • 2Zhang J,Proceedings14 th International Joint Conference on ArtificalIntelligence( IJCAI,1995年,298页
  • 3张健,博士学位论文,1994年

同被引文献3

引证文献1

二级引证文献1

;
使用帮助 返回顶部