CAJ | 학술논문

信息物理融合系统的网络化、系统化和信息化等特性使得软件系统的复杂程度不断增加。为此，引入实时系统的规范语言STeC，用于刻画具有时空一致性要求的实时系统。对于STeC语言的自动逻辑推理问题，通过拓展Maude中的关系等式和重写规则，将STeC语言转化为可执行的基于Maude的形式化描述，使用Maude自动推导功能，自动推导出系统的时间正确性。实例结果表明，该形式化描述语言Maude可有效对实时系统进行安全性验证。
신식물리융합계통적망락화、계통화화신식화등특성사득연건계통적복잡정도불단증가。위차，인입실시계통적규범어언STeC，용우각화구유시공일치성요구적실시계통。대우STeC어언적자동라집추리문제，통과탁전Maude중적관계등식화중사규칙，장STeC어언전화위가집행적기우Maude적형식화묘술，사용Maude자동추도공능，자동추도출계통적시간정학성。실례결과표명，해형식화묘술어언Maude가유효대실시계통진행안전성험증。
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.