摘要
作为一个典型的离散计算机控制系统,CNC(数字控制)系统在运行中需要满足可靠性和安全性。因此如何设计出安全可靠的系统软件以及如何有效地对CNC系统的安全性和可靠性进行验证成为一个非常重要的问题。基于此给出一个新的建模方法TTM/ATRTTL(时间转化模型/全时轴实时时态逻辑)来描述和验证CNC系统。TTM/ATRTTL提供了一整套方法用于描述CNC系统建模的硬实时特性和反馈特性,也提供了一个包括一整套验证规则和定理的验证模型并且应用工具STeP和SF2STeP来实现之。这个验证模型可以用于对TTM/ATRTTL表达的系统的可靠性,安全性进行验证。使用该建模和验证方法可以对OAC(开放式体系结构CNC)系统进行分析和验证,并设计出OAC的逻辑控制器,该控制器是OAC系统的核心部分。验证结果表明,该形式化建模与验证方法可以有效地对CNC系统进行分析和建模。在此基础上,可以开发出能够保证系统可靠性和安全性的CNC系统软件。
As a distributed computing system, a CNC system needs to be operated reliably, dependably and safely. How to design reliable and dependable software and perform effective verification for CNC systems becomes an important research problem. A new modeling method called TTM/ATRTTL （Timed Transition Models/All-Time Real-Time Temporal Logics） for specifying CNC systems was proposed TTM/ATRTTL provided full support for specifying hard real-time and feedback that are needed for modeling CNC systems. A verification framework with verification rules and theorems was proposed and it was implemented with STeP and SF2STeP The proposed verification framework could check reliability, dependability and safety of systems specified by the TTM/ATRTTL method The modeling and verification techniques were applied on an open architecture CNC （OAC） system and comprehensive studies were conducted on modeling and verifying a logical controller that is the key part of OAC. The results show that the method can effectively model and verify CNC systems and generate CNC software that can satisfy system requirements in reliability, dependability and safety.
出处
《系统仿真学报》
CAS
CSCD
北大核心
2009年第15期4572-4578,4582,共8页
Journal of System Simulation
基金
国家自然科学基金(60404019)
