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.
语种：
英文
展开
能力导向的C语言“团队式”教学模式研究
作者：
罗凌云;陈星;罗江琴;欧阳纯萍
期刊：
计算机时代 ,2015年(9):64-65+68 ISSN：1006-8228
作者机构：
南华大学计算机科学与技术学院,湖南 衡阳,421001;[陈星; 欧阳纯萍; 罗江琴; 罗凌云] 南华大学
关键词：
C语言;能力导向;项目教学法;团队式
摘要：
针对C语言程序设计课程知识点繁琐,学生易陷入枯燥繁琐的语法和语句规则中而无所适从,提出能力导向的C语言＂团队式＂教学模式。采用项目教学法,模拟工业界的项目开发过程,将学生分成各个项目组,利用国际上工业界通用的项目管理软件Rally对每个项目组进行管理,改革传统考核方式,以进一步发挥学生的主观能动性,提高其综合能力。
语种：
中文
展开
基于微分动态逻辑的数字化反应堆控制系统建模与验证方法
作者：
刘杰;阳小华;刘华;吴取劲;陈星
期刊：
中国安全生产科学技术 ,2015年11(5):40-44 ISSN：1673-193X
作者机构：
[刘杰; 阳小华; 刘华; 吴取劲; 陈星] 南华大学计算机科学与技术学院
关键词：
混成系统;微分动态逻辑;数字化反应堆控制系统;建模与安全性验证
摘要：
核电数字化仪系统既涉及反应堆随时间变化的物理动态演化过程,又涉及计算机的离散控制过程,属于典型的实时混成系统。微分动态逻辑是近年在混成系统验证领域的新方法。提出以微分动态逻辑为基础的构建反应堆控制系统安全验证模型方法,验证反应堆控制系统中离散化的逻辑控制与反应堆连续性的物理连续变化过程之间的相互作用能否保证反应堆安全需求,从而提高数字化反应堆控制系统设计的安全性。
语种：
中文
展开
提升计算思维能力的编程游戏设计
作者：
刘杰;阳小华;陈星;刘志明;张慧仁
期刊：
电脑知识与技术 ,2015年(21):55-57 ISSN：1009-3044
作者机构：
南华大学计算机科学与技术学院,湖南衡阳,421001;[陈星; 刘志明; 刘杰; 阳小华; 张慧仁] 南华大学
关键词：
程序设计;计算思维;通用编程游戏
摘要：
针对目前程序设计类课程教学过于强调编程语言语法而忽略编程方法,从培养计算思维能力的角度出发,跨越语法规范,设计一种通用编程游戏,阐述了该游戏的设计理念、设计原则、设计内容和设计目标,最后分析了该游戏的应用原则和教学优势。
语种：
中文
展开
基于数据仓库的钢铁销售统计分析系统
作者：
邓才应;肖基毅;陈星
期刊：
电脑知识与技术 ,2008年4(28):1-3,10 ISSN：1009-3044
作者机构：
南华大学,计算机科学与技术学院,湖南,衡阳,421001;[陈星; 肖基毅; 邓才应] 南华大学
关键词：
数据仓库;联机分析处理;多维表达式;钢铁销售;统计系统
摘要：
分析了数据仓库的特点,并根据钢铁销售统计系统的业务需求给出了其系统结构和数据仓库模型,以交货单为中心,前续包括合同和订单,后续包括结算,以及收发存和库存帐龄,最后指出了其关键技术及实现方法,为管理层在销售决策上提供有力支持.
语种：
中文
展开
Petri网的正向推理算法
作者：
陈星;刘杰;余童兰
期刊：
微计算机信息 ,2006年22(36):154-156+134 ISSN：1008-0570
作者机构：
421001,湖南,衡阳,南华大学计算机学院;[陈星; 刘杰; 余童兰] 南华大学
关键词：
Petri网;知识表示;推理算法
摘要：
提出了一种建立在petri网的基本结构上的形式化正向推理算法,通过建立petri网的关联矩阵、标识向量和激发向量,将petri网与矩阵运算结合,可以在petri网模型中抽取一个子模型,从而把一个大的、复杂的系统转化为一个只与问题相关的小的系统来处理.该算法充分利用了petri网的并行处理能力,缩小了后续应用的范围,加速了后续应用的效率.
语种：
中文
展开
