Abstract:
The characteristics of cyber physical systems such as cyberization, systematization and informationization make the software systems more and more complex. Because the classic modeling methods cannot satisfy the needs of Cyber-physical System(CPS), the Spatio-Temporal Consistence(STeC) language for real-time systems whose core property is the consistence of time and location is introduced to model the real-time systems. In order to achieve the automatic logical reasoning in STeC, the equation and rewriting rule in Maude are applied to convert the STeC system to an executable specification description, it can analyze the result of computation and check the correctness of time in the system. Instance results show that the formal description language Maude can effective for real-time system for security verification.
Key words:
real-time system,
specification language for real-time system,
rewriting logic,
formal analysis,
Spatio-Temporal Consistence (STeC),
operational semantics
摘要： 信息物理融合系统的网络化、系统化和信息化等特性使得软件系统的复杂程度不断增加。为此，引入实时系统的规范语言STeC，用于刻画具有时空一致性要求的实时系统。对于STeC语言的自动逻辑推理问题，通过拓展Maude中的关系等式和重写规则，将STeC语言转化为可执行的基于Maude的形式化描述，使用Maude自动推导功能，自动推导出系统的时间正确性。实例结果表明，该形式化描述语言Maude可有效对实时系统进行安全性验证。
关键词:
实时系统,
实时系统的规范语言,
重写逻辑,
形式化分析,
时空一致性,
操作语义
CLC Number: