A proof-based method of hybrid systems development using differential invariants
作者：
Liu, Jie;Liu, Jing* ;Zhang, Miaomiao* ;Sun, Haiying;Chen, Xiaohong;...
期刊：
计算机科学前沿(英文) ,2018年12(5):1026-1028 ISSN：2095-2228
通讯作者：
Liu, Jing;Zhang, Miaomiao
作者机构：
[Liu, Jie; Chen, Mingsong; Liu, Jing; Sun, Haiying; Chen, Xiaohong; Du, Dehui] East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China.;[Liu, Jie] Univ South China, Sch Comp Sci & Technol, Hengyang 421001, Peoples R China.;[Zhang, Miaomiao] Tongji Univ, Sch Software Engn, Shanghai 201804, Peoples R China.
通讯机构：
[Liu, Jing] E;[Zhang, Miaomiao] T;East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China.;Tongji Univ, Sch Software Engn, Shanghai 201804, Peoples R China.
关键词：
混合系统;开发;证明;微分;分离控制;建模语言;研究人员;精炼
摘要：
Event-B is a widely applied and proof-based language for incremental development via refinement [1]. Hybrid systems exhibit hybrid characteristics of discrete control and real-time continuous behaviors. However, Event-B is a discrete modeling language. It does not support the development of hybrid systems. So, the researchers are currently trying to make the extension of Event-B for the refinement development of hybrid systems [2, 3].
语种：
英文
展开
An Approach to Proving Proof Obligation of Hybrid Event B Based on Differential Invariants
作者：
Liu, Jie;Liu, Jing* ;Zhang, Miaomiao;Sun, Haiying;Chen, Xiaohong;...
期刊：
Proceedings - IEEE Computer Society's International Computer Software and Applications Conference ,2017年1:138-143 ISSN：0730-3157
通讯作者：
Liu, Jing
作者机构：
[Liu, Jie; Chen, Mingsong; Liu, Jing; Sun, Haiying; Chen, Xiaohong; Du, Dehui] East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China.;[Liu, Jie] Univ South China, Sch Comp Sci & Technol, Hengyang 421001, Peoples R China.;[Zhang, Miaomiao] Tongji Univ, Sch Software Engn, Shanghai 200062, Peoples R China.
通讯机构：
[Liu, Jing] E;East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China.
会议名称：
41st IEEE Annual Computer Software and Applications Conference (COMPSAC)
会议时间：
JUL 04-08, 2017
会议地点：
Torino, ITALY
会议主办单位：
[Liu, Jie;Liu, Jing;Sun, Haiying;Chen, Xiaohong;Du, Dehui;Chen, Mingsong] East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai 200062, Peoples R China.^[Liu, Jie] Univ South China, Sch Comp Sci & Technol, Hengyang 421001, Peoples R China.^[Zhang, Miaomiao] Tongji Univ, Sch Software Engn, Shanghai 200062, Peoples R China.
会议论文集名称：
Proceedings International Computer Software and Applications Conference
关键词：
hybrid system;Hybrid Event B;differential event;differential invariant;proof obligation
摘要：
For modelling hybrid systems, we have extended Event B based on its framework with the differential event. The differential event describes continuous behaviors of hybrid systems by differential equations and evolution constraint, whose proof obligations provide dynamical properties of a model. In order to ensure the safety and reliability of a model, proof obligations should be proved. It is difficult to prove proof obligation in state space, because there is no a complete method to solve differential equations in the field of mathematics. Thus we proposed an approach to proving proof obligation based on differential invariants. It is to avoid uncontrollable computation on solving differential equation. The main result is that we prove some theorems for proving proof obligations involving differential events within the framework of refinement calculus. Lastly, through the case of the Train Control System, we further show that the approach is well suited. ©2017 IEEE.
语种：
英文
展开
A Formal Framework for Hybrid Event B
作者：
Jie Liu;Jing Liu*
期刊：
Electronic Notes in Theoretical Computer Science ,2014年309:3-12 ISSN：1571-0661
通讯作者：
Jing Liu
作者机构：
[Jing Liu] Shanghai Key Laboratory of Trustworthy Computing, Software Engineering Institute, East China Normal University, 3663 Zhongshan Road (North), Shanghai, China, 200062;School of Computer Science and Technology, University of South China, 28 Changsheng (West), HengYang, China, 421001;[Jie Liu] Shanghai Key Laboratory of Trustworthy Computing, Software Engineering Institute, East China Normal University, 3663 Zhongshan Road (North), Shanghai, China, 200062<&wdkj&>School of Computer Science and Technology, University of South China, 28 Changsheng (West), HengYang, China, 421001
通讯机构：
[Jing Liu] S;Shanghai Key Laboratory of Trustworthy Computing, Software Engineering Institute, East China Normal University, 3663 Zhongshan Road (North), Shanghai, China, 200062
关键词：
Event B;differential dynamic logic;continuous refinement;hybrid systems
摘要：
In this paper, we present Hybrid Event B, a formal language for modeling hybrid systems. Specifically, Hybrid Event B is an extension of Event B associating with differential dynamic logic. The main contribution of this paper is that we give the definition of a differential event in Hybrid Event B, which makes it possible using differential dynamic logic in modeling continuous dynamical systems and discrete dynamical systems. In addition, we show the proof obligations of each refinements on differential events, which supports the stepwise development of refinement. We also show the transformer semantics of the differential events and the weakest precondition refinement approach applied to hybrid systems, both of which support our stepwise development of hybrid systems. © 2014 The Authors. Published by Elsevier B.V.
语种：
英文
展开
Elimination of Redundant Invariants
作者：
Yu Tong-lan;Yang Xiao-hua* ;Liu Jie;Luo Yang;Wu Qu-jin
期刊：
Advances in Intelligent and Soft Computing ,2011年112:275-279 ISSN：1867-5662
通讯作者：
Yang Xiao-hua
作者机构：
[Luo Yang; Liu Jie; Yu Tong-lan; Wu Qu-jin; Yang Xiao-hua] Univ S China, Sch Comp Sci & Technol, Hengyang, Hunan, Peoples R China.
通讯机构：
[Yang Xiao-hua] U;Univ S China, Sch Comp Sci & Technol, Hengyang, Hunan, Peoples R China.
会议名称：
The 2011 International Conference on Informatics,Cybernetics,and Computer Engineering(ICCE 2011)
会议时间：
2011-11-19
会议地点：
Melbourne,Australia
关键词：
Equivalence redundancy;Implication redundancy;Invariant;Invariant Redundancy;Transitivity redundancy
摘要：
Redundant invariants increase processing time and memory consumption, which make serious effect on the application of invariants. The elimination of invariant redundancy is an important part in the invariant study. Now most methods of invariant redundancy elimination are based on optimization of invariants detecting tool which lack the principles analyse and system solutions of redundant invariants themselves. This paper first analyses the theory about classification and forming reasons of redundant invariant and then discusses the judgement of three kinds of invariant redundancy: equivalent redundancy, transitivity redundancy and implicating redundancy. Finally, the paper proposes the algorithms of eliminating invariant redundancy. The study has great value to the application of invariants which can significantly improves the efficiency by saving the time and space in processing. ©Springer-Verlag Berlin Heidelberg 2011.
语种：
英文
展开
基于Web Services的教学系统开发模型研究
作者：
杨星;刘军;罗晨晖
期刊：
福建电脑 ,2007年(4):15-16 ISSN：1673-2782
作者机构：
南华大学图书馆信息室,湖南,衡阳,421001;南华大学计算机科学与技术学院,湖南,衡阳,421001;[罗晨晖; 刘军; 杨星] 南华大学
关键词：
教学系统;Web课件;开发模型
摘要：
基于Web Services的教学系统开发实际上是以XML数据为基础，通过SOAP协议集成互联网上的各种web课件资源，使之协同完成一个特定教学任务的过程。本文在分析了Web课件集成和运行管理机制与实现方法的基础上提出了一种新的基于Web Services的教学系统体系结构．并探讨了开发Web课件所涉及的一些关键性任务及其具体的实现步骤。
语种：
中文
展开
从选课方式的改进看我国高校教学管理的信息化
作者：
阳小华;刘军;罗晨晖
期刊：
高等理科教育 ,2007年(4):59-62 ISSN：1000-4076
作者机构：
南华大学,教务处,湖南,衡阳,421001;南华大学,计算机科学与技术学院,湖南,衡阳,421001;[罗晨晖; 刘军; 阳小华] 南华大学
关键词：
选课;高等学校;教学管理;信息化
摘要：
文章就高校选课方式从传统的手工选课到基于WEB环境的网上选课的改进,比较了两者在流程与效率方面的差异,比较客观地分析了我国高校教学管理信息化的必要性。
语种：
中文
展开
基于消息中间件的智能元搜索引擎设计
作者：
魏振达;阳小华;刘军
期刊：
淮阴师范学院学报(自然科学版) ,2006年5(1):78-82 ISSN：1671-6876
作者机构：
南华大学,计算机科学与技术学院,湖南,衡阳,421001;南华大学,教务处,湖南,衡阳,421001;[刘军; 阳小华; 魏振达] 南华大学
关键词：
元搜索引擎;消息中间件
摘要：
消息中间件作为当前的主流技术,在企业级计算中发挥了巨大作用,在企业事务处理等领域有着广泛而深入的应用前景.本文通过在元搜索引擎的开发上引入消息中间件使元搜索引擎呈现出模块型结构,达到异步的设计效果,形成分布式系统的元搜索引擎.
语种：
中文
展开
基于．NET组件技术的教学信息发布与管理系统的设计与实现
作者：
刘军;阳小华;杨星
期刊：
微型电脑应用 ,2006年22(4):24-27+30+69 ISSN：1007-757X
作者机构：
南华大学计算机科学与技术学院硕士研究生;南华大学计算机科学与技术学院教授、博士;南华大学图书馆信息室;[刘军; 杨星; 阳小华] 南华大学
关键词：
.NET组件;B/S模式;教学管理;信息发布
摘要：
基于组件技术的软件技术开发模式是实现大规模的代码复用的一条切实可行的途径，是面向对象技术的发展，本文介绍了基于组件的软件复用的基本概念及4种组件技术，着重阐述了B／S模式下的．NET组件开发的一般方法，并在此基础上完成了教学信息发布与管理系统的功能描述、设计与实现。
语种：
中文
展开
一种新的基于B/S模式的权限管理方案
作者：
刘军;阳小华;杨星
期刊：
微计算机信息 ,2006年22(01X):83-85+177 ISSN：1008-0570
作者机构：
[刘军; 阳小华] 421001,衡阳,南华大学计算机科学与技术学院;421001,衡阳 南华大学图书馆信息室;[杨星] 南华大学
关键词：
B/S模式;页面指纹;权限管理
摘要：
本文分析了RBAC模型存在的局限性,结合高校教务系统权限管理的特点,在给出了WEB页面权限指纹概念的基础上提出了一种基于用户功能、分组式授权的新的权限管理方案.该方案应用于B/S模式的MIS系统中能够很大程度上降低应用服务器用于权限管理的运行代价.
语种：
中文
展开
基于B/S模式的通用型组合查询组件的设计
作者：
刘军;阳小华;杨星
期刊：
测控自动化 ,2006年22(02X):256-258,85 ISSN：1008-0570
作者机构：
[刘军; 阳小华] 421001,衡阳南华大学计算机科学与技术学院;421001,衡阳南华大学图书馆信息室;[杨星] 南华大学
关键词：
.NET组件;组合查询;数据视图
摘要：
通过分析组合查询的一般性设计原则,结合数据视图和.NET技术的特点,设计了一个基于B/S模式的通用型类汉语组合查询组件,并就实现中的几个关键问题进行了探讨。
语种：
中文
展开
教学信息发布与管理系统的设计与实现——基于.NET组件技术
作者：
刘军;阳小华;杨星
期刊：
计算机工程与应用 ,2006年42(2): 99-102,166 ISSN：1002-8331
作者机构：
南华大学计算机科学与技术学院硕士研究生;南华大学计算机科学与技术学院教授、博士;南华大学图书馆信息室;[刘军; 杨星; 阳小华] 南华大学
关键词：
.NET组件;B/S模式;教学管理;信息发布
摘要：
基于组件技术的软件技术开发模式是实现大规模的代码复用的一条切实可行的途径，是面向对象技术的发展，该文介绍了基于组件的软件复用的基本概念及4种组件技术，着重阐述了B／S模式下的.NET组件开发的一般方法，并在此基础上完成了教学信息发布与管理系统的功能描述、设计与实现。
语种：
中文
展开
基于ASP.NET页面指纹的分组式权限管理方案
作者：
刘军;阳小华;黄洁
期刊：
计算机工程与应用 ,2006年42(10):178-180,232 ISSN：1002-8331
作者机构：
[刘军; 阳小华; 黄洁] 南华大学计算机科学与技术学院;南华大学计算机科学与技术学院 湖南衡阳421001
会议名称：
第二届全国Web信息系统及其应用会议(WISA2005')
会议时间：
2005-09-01
会议地点：
沈阳
会议论文集名称：
Web信息系统与技术
关键词：
页面指纹;权限管理
摘要：
论文分析了RBAC模型存在的局限性,结合高校教务系统权限管理的特点,在给出了Web页面权限指纹概念的基础上提出了一种基于用户功能、分组式授权的新的权限管理方案.该方案应用于B/S模式的MIS系统中能够很大程度上降低应用服务器用于权限管理的运行代价.
语种：
中文
展开
成员搜索引擎的查询参数表达能力的建模设计
作者：
魏振达;阳小华;刘军
期刊：
南华大学学报(自然科学版) ,2005年19(4):83-85,89 ISSN：1673-0062
作者机构：
[刘军; 阳小华; 魏振达] 南华大学
关键词：
元搜索引擎;成员搜索引擎;查询变量;表达能力;布尔模型;向量模型
摘要：
讨论了元搜索引擎中成员搜索引擎的查询变量的表达能力的问题来源,并给出了布尔和向量两种模型的定义、计算方法,对成员搜索引擎的查询变量的表达能力的计算方法进行了深入探讨.
语种：
中文
展开
用于非接触式核测量的红外通信接口的设计
作者：
刘军;周剑良
期刊：
核电子学与探测技术 ,2004年24(2):193-195 ISSN：0258-0934
作者机构：
[刘军] 南华大学计算机科学与应用学院;[周剑良] 核科学技术学院
关键词：
非接触方式
摘要：
介绍了一种简易、低成本的PC机与单片机进行红外通信方式，并介绍了相应的接口电路。该方法可用于多机通信。
语种：
中文
展开
PC机与单片机的红外通信接口设计
作者：
颜拥军;刘军
期刊：
东莞理工学院学报 ,2003年10(2):7-9,17 ISSN：1009-0312
作者机构：
南华大学计算机科学与技术学院,湖南衡阳,421001;[刘军; 颜拥军] 南华大学
关键词：
PC机;单片机;红外通信接口;串行通信;接口电路;红外遥控;红外传输原理;设计方法
摘要：
文章提出了一种简易、成本低的PC机与单片机(也称为微控制器MCU)应用系统进行红外通信方法,并介绍了相应的接口电路,该方法可用于多机通信.
语种：
中文
展开
实现PASCAL语言对UCDOS特显功能调用的方法
作者：
刘军;成湘豫
期刊：
微型电脑应用 ,1998年(05):86-89 ISSN：1007-757X
作者机构：
衡阳医学院计算中心!衡阳;421001
关键词：
PASCAL语言;特殊显示;程序设计
摘要：
本文通过对UCDOS特显原理的分析，结合TurboPASCAL语言的输入输出特点，给出了在PASCAL语言环境下调用UCDOS特显功能的具体方法，以及相应API程序的设计思路。
语种：
中文
展开
限制DOS命令对文件的操作权限
作者：
刘军;成湘豫;徐志文
期刊：
电脑编程技巧与维护 ,1998年(1):6-8 ISSN：1006-4052
作者机构：
衡阳医学院计算中心;[刘军; 成湘豫; 徐志文] 衡阳医学院
关键词：
DOS命令;文件属性;访问权限
摘要：
本文通过对ＤＯＳ文件属性的分析，在局部修改ＤＯＳ内核ＭＳＤＯＳ．ＳＹＳ的基础上，提出了一种利用设置特殊文件属性的方法来限制ＤＯＳ内部命令及部分外部命令对文件的操作权限。从而达到了保护文件系统的正确性和完整性的目的。同时给出了设置特殊文件属性的工作程序。
语种：
中文
展开
利用处在定义属性实现文件的保护
作者：
刘军
期刊：
计算机时代 ,1998年(3):23-25 ISSN：1006-8228
作者机构：
衡阳医学院计算中心;[刘军] 衡阳医学院
关键词：
文件保护;自定义属性;文件操作
摘要：
本文在局部修改DOS内核MSDOS.SYS的基础上,提出了一种利用设置自定义文件属性的方法来限制DOS内部命令及部分外部命令对文件的操作权限,从而达到保护文件系统的正确性和完整性的目的。
语种：
中文
展开
