Trace semantics and refinement patterns for real-time properties in event-B models

Chenyang Zhu,Michael Butler,Corina Cirstea

Science of Computer Programming（2020）

引用 6|浏览26

暂无评分

摘要

•Formal trace semantics and refinement semantics of timed Event-B models.•Prove infinite state trace simulation with Zorn's Lemma.•Formal definition of hiding operator of infinite traces.•Provide generic refinement semantics with proofs.

查看译文

关键词

Event-B,Trace semantics,Refinement semantics,Discrete time modeling,Hiding operator

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要