论文部分内容阅读
信息物理融合系统的网络化、系统化和信息化等特性使得软件系统的复杂程度不断增加。为此，引入实时系统的规范语言STeC，用于刻画具有时空一致性要求的实时系统。对于STeC语言的自动逻辑推理问题，通过拓展Maude中的关系等式和重写规则，将STeC语言转化为可执行的基于Maude的形式化描述，使用Maude自动推导功能，自动推导出系统的时间正确性。实例结果表明，该形式化描述语言Maude可有效对实时系统进行安全性验证。