一种安全关键软件系统符号执行优化方法
作者：
戴延军;吴志强;刘杰;刘朝晖;陈智;...
期刊：
计算机与现代化 ,2020年(01):96-99,110 ISSN：1006-2475
作者机构：
[戴延军; 刘杰; 刘朝晖] 南华大学计算机科学与技术学院,湖南 衡阳 421000;中国核动力研究设计院核反应堆系统设计技术国家级重点实验室,四川 成都 610000;[肖安红; 吴志强; 陈智] 中国核动力研究设计院
关键词：
安全关键系统;软件耦合性;带权最小割集;符号执行
摘要：
在航空、核电和国防军工领域当中,安全关键系统(Safety-Critical System,SCS)的软件非常重要,其可靠性必须通过测试或形式化方法来保障.符号执行作为一种高效的测试用例生成方法被广泛使用,然而,SCS软件系统的模块之间的耦合性较高,使得符号执行约束求解困难.本文针对这类软件系统提出一种带权最小割集的解耦方法,为安全关键软件系统的自动化测试提供了一种新思路.
语种：
中文
展开
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.
语种：
英文
展开
基于合约的SCADE测试工具设计与实现
作者：
刘小同;熊梦;阳小华;刘杰
期刊：
电脑知识与技术 ,2017年13(11):222-224 ISSN：1009-3044
作者机构：
南华大学计算机科学与技术学院,湖南衡阳,421001;[熊梦; 刘杰; 阳小华; 刘小同] 南华大学
关键词：
反应堆保护系统;SCADE系统;基于合约的测试平台
摘要：
反应堆保护系统是核电厂中最重要的安全系统,对保证核电设备、工作人员以及周边环境的安全有着至关重要的作用.由于反应堆保护系统所需要的高安全性,因此SCADE平台开发的压水堆反应堆保护系统(以下简称SCADE系统)是近年来重要的研究方向.但是SCADE平台的开发过程基本以图形方式展现,设计与验证工作也都在SCADE系统内部完成,缺少对内部的本质特征的说明.因此需要一种方法来对SCADE系统的内部结构进行解释,并根据此对SCADE系统进行后期的验证工作提供理论支持,确保对SCADE系统的验证工作是有效的.笔者由此提出了基于合约的SCADE测试理论,并根据此理论设计并开发了基于合约的SCADE自动测试平台,用于为SCADE系统的验证工作提供充分的测试用例并进行相关测试工作.
语种：
中文
展开
贯穿不同软件工程职业角色的软件测试课程教学方法的探索
作者：
楚燕婷;欧阳纯萍;阳小华;刘杰
期刊：
高教学刊 ,2017年(11):27-28,31 ISSN：2096-000X
作者机构：
南华大学 计算机科学与技术学院,湖南 衡阳,421001;[欧阳纯萍; 刘杰; 楚燕婷; 阳小华] 南华大学
关键词：
软件测试;课程改革;职业角色
摘要：
为了满足社会对软件工程人才的需求,解决软件测试课程教学中存在的问题,文章根据软件测试贯穿于整个软件生命周期的特性,分析总结了软件人才市场常见的职业角色特点,并根据实际教学情况设立了五个主要的职业角色,分析这些不同职业的角色对于软件测试能力的不同需求,在此基础上提出贯穿不同职业角色的软件测试课程教学模式,并详细介绍了该教学模式设计的实施过程和效果。
语种：
中文
展开
基于K-V模型集成测试工具的设计与实现
作者：
熊梦;刘小同;阳小华;刘杰
期刊：
数字社区&智能家居 ,2017年13(10):230-232,238 ISSN：1009-3044
作者机构：
南华大学计算机科学与技术学院,湖南衡阳,421001;[熊梦; 刘杰; 阳小华; 刘小同] 南华大学
关键词：
软件测试自动化;集成测试工具;K-V模型;非渐增式测试;替换输入卡值
摘要：
随着核电国产化率的不断提高,核电软件的开发也在不断的进行。而软件测试作为软件生命周期中一个必要的环节,对于保证软件的质量与可靠性有着重要的意义。在核电软件中,部分软件系统需要使用包含大量参数名与参数值的文件作为输入卡进行测试。在针对该类软件的集成测试中,主要使用非渐增式测试方法,通过对输入卡进行参数值替换来生成相应的测试用例,从而进行测试。因此存在人工测试时工作量大、效率低、准确性低等问题。对于此类的集成测试工作,由于输入卡中参数多、参数可选值多、系统输出文件对比困难等原因,笔者提出了基于K-V（Key-Value）模型的集成测试工具,以解决测试过程人工测试所面临的问题。
语种：
中文
展开
基于岗位职责的增量式软件工程专业课程体系设计研究
作者：
刘杰;阳小华;徐卓然;刘志明
期刊：
高教学刊 ,2017年(15):95-97 ISSN：2096-000X
作者机构：
南华大学 计算机科学与技术学院,湖南 衡阳,421001;[刘志明; 刘杰; 徐卓然; 阳小华] 南华大学
关键词：
CDIO教育模式;岗位职责;软件工程专业课程;课程体系
摘要：
为了培养优秀的软件工程型人才,迎接以“互联网＋”为特征的新工业革命的到来。我们以CDIO工程教学模式为指导,在工程过程、软件工程知识域、能力培养规律和学校学制等约束条件下,通过分析软件企业核心岗位职责挖掘能力需求和知识需求,提出基于岗位职责的增量式软件工程专业课程体系设计方案,并给出了课程体系的教学设计作为支撑,从而实现学生软件工程的深度职业技能培养。
语种：
中文
展开
基于系统理论的稳压器压力控制器安全性分析
作者：
刘杰;吴志强;阳小华;刘华;吴取劲;...
期刊：
信息技术 ,2016年(2):31-34 ISSN：1009-2552
作者机构：
南华大学计算机科学与技术学院,湖南衡阳,421001;中国核动力研究设计院核反应堆系统设计技术重点实验室,成都,610041;[吴取劲; 刘杰; 阳小华; 闫仕宇; 刘华] 南华大学;[吴志强] 中国核动力研究设计院
关键词：
压水堆;稳压器压力控制器;系统理论;STAMP模型;安全性分析
摘要：
压水堆稳压器压力控制系统通过控制加热或喷淋等方法,维持核电厂压力容器的压力在安全的范围内,属于核设施安全关键设备。压力控制的热工流体力学过程具有高度复杂、非线性等复杂系统特点。针对第三代堆型AP1000堆型数字化稳压器压力控制系统,通过运用基于系统理论的STAMP模型进行安全性分析,发现影响安全的潜在危险因素,强化安全约束,预防危险事故,提出改进建议为提高压水堆稳压器压力控制器的安全性和核电设备国产化做出贡献。
语种：
中文
展开
依托ACM／ICPC的高素质IT人才培养探索与实践
作者：
余颖;欧阳纯萍;刘杰;刘志明
期刊：
计算机教育 ,2015年(16):10-13 ISSN：1672-5913
作者机构：
[刘志明; 欧阳纯萍; 刘杰; 余颖] 南华大学计算机科学与技术学院,湖南衡阳21001
关键词：
IT人才培养;综合素质
摘要：
针对目前IT业求职市场突出的供求矛盾,分析企业对IT人才的素质要求以及ACM/ICPC竞赛活动对学生综合素质培养的积极作用,阐述如何有效地开展竞赛活动.
语种：
中文
展开
基于微分动态逻辑的数字化反应堆控制系统建模与验证方法
作者：
刘杰;阳小华;刘华;吴取劲;陈星
期刊：
中国安全生产科学技术 ,2015年11(5):40-44 ISSN：1673-193X
作者机构：
[刘杰; 阳小华; 刘华; 吴取劲; 陈星] 南华大学计算机科学与技术学院
关键词：
混成系统;微分动态逻辑;数字化反应堆控制系统;建模与安全性验证
摘要：
核电数字化仪系统既涉及反应堆随时间变化的物理动态演化过程,又涉及计算机的离散控制过程,属于典型的实时混成系统。微分动态逻辑是近年在混成系统验证领域的新方法。提出以微分动态逻辑为基础的构建反应堆控制系统安全验证模型方法,验证反应堆控制系统中离散化的逻辑控制与反应堆连续性的物理连续变化过程之间的相互作用能否保证反应堆安全需求,从而提高数字化反应堆控制系统设计的安全性。
语种：
中文
展开
提升计算思维能力的编程游戏设计
作者：
刘杰;阳小华;陈星;刘志明;张慧仁
期刊：
电脑知识与技术 ,2015年(21):55-57 ISSN：1009-3044
作者机构：
南华大学计算机科学与技术学院,湖南衡阳,421001;[陈星; 刘志明; 刘杰; 阳小华; 张慧仁] 南华大学
关键词：
程序设计;计算思维;通用编程游戏
摘要：
针对目前程序设计类课程教学过于强调编程语言语法而忽略编程方法,从培养计算思维能力的角度出发,跨越语法规范,设计一种通用编程游戏,阐述了该游戏的设计理念、设计原则、设计内容和设计目标,最后分析了该游戏的应用原则和教学优势。
语种：
中文
展开
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.
语种：
英文
展开
基于STAMP模型的核动力蒸汽发生器水位控制系统安全性分析
作者：
刘杰;阳小华;余童兰;刘华;刘朝晖
期刊：
中国安全生产科学技术 ,2014年10(5):78-83 ISSN：1673-193X
作者机构：
[刘杰; 阳小华; 余童兰; 刘华; 刘朝晖] 南华大学计算机科学与技术学院
关键词：
蒸汽发生器水位控制系统;安全性分析
摘要：
核电厂蒸汽发生器(SG)水位控制系统的安全可靠运行是保证核电厂安全性和经济性的关键因素,其控制对象具有高度复杂、非线性的特点。由于复杂系统的安全性是特定环境下由系统相关要素交互作用所产生的一种涌现特性,运用系统理论,以STAMP 模型为基础对SG 水位控制系统进行安全性分析,以利于在设计早期阶段发现影响该系统安全运行的潜在风险因素,预防危险事故。该方法将系统理论用于核电厂关键系统和设备安全性分析,为核电厂安全运行提供了新的技术手段支持。
语种：
中文
展开
核电厂数字化仪控系统全状态监测机制
作者：
阳小华;刘朝晖;陈智;刘杰;吴志强
期刊：
核动力工程 ,2014年35(3):138-141 ISSN：0258-0926
通讯作者：
Yang, X.
作者机构：
[阳小华; 刘朝晖; 刘杰] School of Computer Science and Technology, University of South China, Hengyang, 421001, China;[陈智; 吴志强] Science and Technology on Reactor System Design Technology Laboratory, Nuclear Power Institute of China, Chengdu, 610041, China
通讯机构：
School of Computer Science and Technology, University of South China, China
关键词：
核电厂;数字化仪控系统;全状态监测
摘要：
软件失效及软硬件交互故障是核电厂全数字化仪控系统故障的主要来源之一。现有基于硬件的状态监测机制应对这一新型失效模式存在不足。应用系统理论事故建模与处理(STAMP)模型,对核电厂全数字化仪控系统的失效模式进行初步分析,提出将软件、硬件及其交互作为监测对象,建立一种整合软、硬件状态的全状态监测机制,为系统状态监测提供多样性及预警能力,对提高核电厂数字化仪控系统的安全性具有重要意义。
语种：
中文
展开
仪控系统阈值判决及核电站应用
作者：
刘华;黄奇;陈柯;刘朝晖;刘杰
期刊：
自动化仪表 ,2014年35(9):42-45 ISSN：1000-0380
作者机构：
南华大学电气工程学院;[陈柯; 黄奇] 中国核动力研究设计院;南华大学计算机科学技术学院;[刘杰; 刘华; 刘朝晖] 南华大学
关键词：
阈值判决;监测;鲁棒性;数据处理
摘要：
基于物理参数的仪控系统阈值判决是核电站仪控系统的重要功能,但其存在阈值判决固定单一,缺乏与时间、工况的相关性等不足。对已有阈值判决进行改进和优化,通过分析研究,在安全前提下,从多种数据处理算法对比、阈值多级浮动、与具体工况相关联等方面作出改进。改进后的阈值判决有助于提升仪控系统的容错、故障诊断能力,减少不必要的停堆次数,提高了电厂的经济效益。
语种：
中文
展开
Method of Detecting Unary Polynomial Inequality Likely Invariant
作者：
Yu Tonglan;Yang Xiaohua* ;Chen Cai;Liu Jie
期刊：
Applied Mechanics and Materials ,2013年373-375:1894-1899 ISSN：1662-7482
通讯作者：
Yang Xiaohua
作者机构：
[Chen Cai; Yang Xiaohua; Liu Jie; Yu Tonglan] Univ South China, Sch Comp Sci & Technol, Hengyang, Peoples R China.
通讯机构：
[Yang Xiaohua] U;Univ South China, Sch Comp Sci & Technol, Hengyang, Peoples R China.
会议地点：
Guangzhou, PEOPLES R CHINA
会议主办单位：
[Yu Tonglan;Yang Xiaohua;Chen Cai;Liu Jie] Univ South China, Sch Comp Sci & Technol, Hengyang, Peoples R China.
会议论文集名称：
Applied Mechanics and Materials
关键词：
Likely Invariant;Dynamical Detecting;Polynomial Inequality Invariant
摘要：
Many Studies has carried on the technology of detecting invariants, for example, Daikon can detect most of invariant by presetting some types of them. But unary polynomial inequality likely invariants are rarely discovered by traditional tools. An effective method to detect unary polynomial inequality likely invariant was proposed in this paper. Through analyzing the property of value ranges of unary polynomial inequality likely invariants, the algorithm set the threshold value and calculates neighbor distances to determine the form of invariants. Finally, experimental results are given to demonstrate the effectiveness of this method.
语种：
英文
展开
STAMP模型及其在核电厂DCS安全分析中的应用展望
作者：
阳小华;刘杰;刘朝晖;刘华;余童兰
期刊：
核安全 ,2013年12(3):42-47+88 ISSN：1672-5360
作者机构：
南华大学计算机科学与技术学院,衡阳,421001;[刘杰; 阳小华; 刘华; 余童兰; 刘朝晖] 南华大学
关键词：
核电安全分析;展望
摘要：
数字化控制是核电发展的必然趋势，核电厂数字化控制系统（Digital Control System，DCS）的应用在提高核电厂系统控制能力的同时也增加了系统的复杂性，以事件链模型为基础的传统安全分析技术面临挑战。为提高核电厂DCS的安全性能，需要关注安全工程领域的新研究成果，将其引入到核电安全领域并加以研究。本文介绍一种新的基于系统理论的事故模型和过程（Systems-Theoretic Accident Modeling and Processes，STAMP）安全模型，对比分析了其与传统安全模型的优缺点，说明了基于STAMP的风险分析（STAMP-Based Hazard Analysis, STPA）技术的基本步骤，并根据STAMP在国内外的应用情况，对STAMP在我国核电领域的发展前景进行了展望。
语种：
中文
展开
核电站数字化仪控系统的安全预警
作者：
刘华;阳小华;刘杰;刘朝晖;吴取劲
期刊：
湖南工业大学学报 ,2013年27(03):61-64 ISSN：1673-9833
作者机构：
南华大学电气工程学院,湖南衡阳,421001;南华大学计算机科学与技术学院,湖南衡阳,421001;[吴取劲; 刘杰; 阳小华; 刘华; 刘朝晖] 南华大学
关键词：
数字化仪控系统;安全;预警
摘要：
核电站数字化仪控系统存在系统风险.基于安全性理论,风险形成是一个传导过程,针对仪控系统失效这一概率事件,提出一级预警和二级预警的概念.基于特征向量的安全预警,可以合理描述系统风险的各种情况,并提高对DCS仪控系统问题的预警时间裕量,增加核电站的安全及可靠性.
语种：
中文
展开
Timed Behavioral Specification in Globally Asynchronous Locally Synchronous systems
作者：
Yu Tonglan;Liu Jie;Zhang Juan;Wu Qujing
期刊：
Telkomnika (Telecommunication Computing Electronics and Control) ,2013年11(9):5119-5125 ISSN：1693-6930
通讯作者：
Tonglan, Y.(Ytonglan@163.com)
作者机构：
[Liu Jie; Zhang Juan; Wu Qujing; Yu Tonglan] School of Computer Science and Technology, University of South China, HengYang, HuNan, 421001, China
摘要：
In this paper, we propose a PolGALS language for safety critical GALS(Globally Asynchronous Locally Synchronous) systems. The formal syntax and semantics are given and its compilation and implementation are defined. The language is based on timed CSP (communicating sequential process) style rendezvous between clock domains, aiming at modelling the timed behavioral of safety critical GALS systems. PolGALS is used to design timed behavioral pattern to implement timing requirements, e.g. delay, timeout, deadline, timed interrupt, etc. PolGALS provides a mechanism for implementation of timed behavioral pattern and potential for their formal verification because it is based on a PolGALS model of computation and its formal semantics. Keywords: PolGALS language, Semantics, Syntax, Timed behavioral, Globally Asynchronous Locally Synchronous system. ©2013 Universitas Ahmad Dahlan.
语种：
英文
展开
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.
会议名称：
International Conference on Informatics, Cybernetics, and Computer Engineering (ICCE2011)
会议时间：
NOV 19-20, 2011
会议地点：
Melbourne, AUSTRALIA
会议主办单位：
[Yu Tong-lan;Yang Xiao-hua;Liu Jie;Luo Yang;Wu Qu-jin] Univ S China, Sch Comp Sci & Technol, Hengyang, Hunan, Peoples R China.
会议论文集名称：
Advances in Intelligent and Soft Computing
关键词：
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.
语种：
英文
展开
