• 主题
高级搜索  >
历史搜索 清空历史
首页> 美国政府科技报告 >Formalizing, Validating, and Verifying Real-Time System Requirements with Reactoand VHDL
【24h】

Formalizing, Validating, and Verifying Real-Time System Requirements with Reactoand VHDL

机译：使用Reactoand VHDL对实时系统要求进行形式化，验证和验证

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

摘要

We develop a methodology for formalizing, verifying, and validating therequirements specification of real-time systems based on a graphical and formal hierarchical Finite State Machine (FSM) language Reacto. We define a means to quantify time and express real-time constraints in Reacto and a transformation from Reacto to the Very High Speed Integrated Circuit (VHSIC) Hardware Description Language (VHDL). Reacto's high level abstractions, graphical nature, and theorem prover produce efficient, accurate, and easily understood specifications. We use VHDL's event driven simulation capability, concurrency, and temporal operators to thoroughly examine temporal dependencies between the state machine transitions, and to increase simulation power by simulating multiple communicating FSMs. We apply the methodology to two example problems, a cruise control, and a lift (elevator) controller. We verify that the state machine specification is consistent and validate the specification using executable simulations in both Reacto and VHDL. We evaluate the methodology against criteria for real-time specification languages and conclude that Reacto and VHDL complement each other well. Together, they abstract the real world well, are clearly understood, verify that the specification and implementation are consistent, axe easy to modify, allow requirements tracing, and finally, support specification of concurrency and timing constraints.... Requirements Analysis, Real Time, System Specification, Reacto, VHDL, Software

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号