采用经典一阶逻辑的混合系统仿真逻辑验证法  

Simulation Logic Validation Method of Hybrid Systems Applying Classical First-Order Logic

作　　者：卢中宁[1] 付金华[2] 张志锋[1] 

机构地区：[1]郑州轻工业学院软件学院,中国郑州450002 [2]郑州轻工业学院计算机与通信工程学院,中国郑州450002

出　　处：《湖南师范大学自然科学学报》2015年第2期84-89,共6页Journal of Natural Science of Hunan Normal University

基　　金：国家自然科学基金资助项目(61201447);河南省教育厅科学技术研究重点项目(12A520048)

摘　　要：针对混合系统难以分析和验证的问题,提出了一种采用经典一阶逻辑的混合系统仿真逻辑验证法.首先给出了混合程序、混合系统仿真逻辑公式、仿真逻辑的命题形式和含义、混合仿真、混合程序仿真语义、仿真逻辑公式的值等定义,然后在经典一阶逻辑、混合程序仿真语义和仿真逻辑公式的值的基础上给出仿真逻辑形式推演规则.最后通过煮鸡蛋的例子验证了混合系统的活性.To analyze and verify hybrid systems,a simulation logic verifies method of hybrid systems by applying the classical first-order logic is proposed. Hybrid programs,simulation logic formulas of hybrid systems,simulation logic notation form and meaning,hybrid simulation,simulation semantics of hybrid programs,valuation of simulation logic formulas are firstly proposed. And then,formal deduction rules for simulation logic based on classical first-order logic,simulation semantics of hybrid programs,valuation of simulation logic formulas were put forward. Finally,the liveness of hybrid systems is verified through an example of boiling eggs.

关 键 词：混合程序 仿真逻辑公式 仿真语义 形式推演规则 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术]