刘静

作品数：12被引量：46H指数：3
导出分析报告
供职机构：华东师范大学更多>>
发文主题：太极拳运动译码ML校验方法系统模型更多>>
发文领域：文化科学自动化与计算机技术经济管理医药卫生更多>>
发文期刊：《软件学报》《航空工程进展》《系统科学与数学》《学校管理》更多>>
所获基金：国家自然科学基金中国博士后科学基金国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
面向航电软件的Safety_SysML一致性验证器设计与实现
《航空工程进展》2023年第4期177-188,共12页尹伟 王辉 孙海英 丁郭欢 康介祥 刘静 
工信部民机预研项目(MJ-2018-S-29)。
民用飞机航空电子系统的高度综合化导致机载安全关键软件规模的成倍增加,带来航电系统软件需求的来源众多且不一致,航电系统软件各层次需求传递存在二义性等问题,因此,如何确保航电软件的一致性成为系统研发过程中亟待解决的核心问题之...
关键词：Safety_SysML状态机 一致性验证器 动态数据检测 功能测试 
基于SMT的区域控制器同步反应式模型的形式化验证
《软件学报》2023年第7期3080-3098,共19页李腾飞 孙军峰 吕新军 陈祥 刘静 孙海英 何积丰 
国家重点研发计划(2019YFA0706404);国家自然科学基金(61972150);上海市超级博士后基金(2021146)。
在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶...
关键词：形式化验证 安全关键系统 同步反应式模型 高阶迭代 程序转换 
有理数域上一类多项式可约性的一个判别法
《系统科学与数学》2021年第12期3351-3362,共12页赵世忠 符红光 秦小林 刘静 刘云浩 
国家自然科学基金(12171159,61972150,61876034);国家“863”计划课题(2018YFB1005100,2018YFB1005104);国家重点研发计划(2019YFA0706404);中国科学院“西部青年学者”项目(201899);四川省委组织部人才专项资助课题。
任给一个m次的整系数多项式∑_(i=0)^(m)aix^(i),其中首项系数am=1,以及对应的下列不动点迭代算法{u1=u^(~)1,u2=u^(~)2,…u_(m-1)=u^(~)_(m-1),u_(n)=-(a_(m-1)+a_(m-2)/u_(n-1)+a_(m-3)/u_(n-1)u_(n-2)+…+a0/u_(n-1)u_(n-2)…u_(n-(m...
关键词：可约 不可约 多项式 迭代 零点 根 初始值 
不确定环境下hCPS系统的形式化建模与动态验证被引量：2
《软件学报》2021年第7期1999-2015,共17页安冬冬 刘静 陈小红 孙海英 
国家重点研发计划(2019YFA0706404);国家自然科学基金(61972150);上海市知识服务平台(ZF1213);上海市科技计划(20ZR1416000);上海市青年科技英才杨帆计划(21YF1432900)。
随着科技的进步,新型复杂系统,例如人机物融合系统(human cyber-physical systems,简称hCPS),已与人类社会生活越来越密不可分.软件系统所处的信息空间与人们日常生活所处的物理空间日渐融合.物理空间内环境的复杂多变、时空数据的爆发...
关键词：人机物融合系统 机器学习 不确定性建模 形式化验证 统计模型检测 
循环迭代程序的一种可信计算算法被引量：2
《软件学报》2020年第12期3685-3699,共15页赵世忠 陈冬火 刘静 
国家重点研发项目(2017YFB1001800);国家自然科学基金(61772203,61972150,61876034)。
循环迭代程序作为软件的基本组成部分,其正确运行具有重要意义.然而,有时(比如其相关错数大于0时)计算时的舍入误差(或表示误差)会导致循环迭代的计算结果不稳定.基于“中间计算精度自动动态调整”的计算技术,给出了循环迭代程序的一种...
关键词：循环迭代 误差可控计算 可信计算 可靠计算 错数 
基于Coq的Paxos形式化建模与验证被引量：6
《软件学报》2020年第8期2362-2374,共13页李亚男 邓玉欣 刘静 
国家自然科学基金(61672229,61832015)。
Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用,比如区块链系统以及谷歌文件系统等,其安全性证明越来越重要.在...
关键词：分布式系统 Basic Paxos 定理证明工具 COQ 验证 
轨道交通联锁领域特定语言的形式化被引量：7
《软件学报》2020年第6期1638-1653,共16页赵梦瑶 陈小红 孙海英 刘静 陈良育 周庭梁 
国家重点研发计划(2018YFB2101300);国家自然科学基金(61332008,91418203,61672230,61572195,11471209,61802251);上海市经济和信息化委员会专项资金(160306)。
作为轨道交通系统的核心子系统之一,对联锁系统进行形式化建模与分析,是保证其安全性的重要手段.形式化建模需要领域知识和形式化知识的结合,由于形式化知识难以掌握,领域专家在建模整个过程中都需要形式化专家的帮助.为了解决这个问题...
关键词：联锁系统 模板重用 形式化建模 随机混成自动机 领域特定语言 
区域控制器的安全需求建模与自动验证被引量：3
《软件学报》2020年第5期1374-1391,共18页刘筱珊 袁正恒 陈小红 陈铭松 刘静 周庭梁 
国家重点研发计划(2018YFB2101300);国家自然科学基金(61332008,61872147,61572195,61802251);上海市经济和信息化委员会专项资金(160306)。
轨道交通区域控制器是我国轨道交通信号系统选型的主流制式--基于通信的列车控制系统的核心子系统,其突出的安全性使得安全需求的形式化验证成为一个非常重要的问题.但是区域控制器自身的复杂性以及领域知识的繁杂难以掌握,使得形式化...
关键词：区域控制器 安全需求建模 自动验证 需求分解 组合验证 
论我国的宪法司法化被引量：1
《法制与社会》2008年第14期13-14,共2页刘静 
本文介绍了宪法司法化的起源、含义,分析了我国宪法司法化的现状,从宪法的法律性、最高权威性、保障公民基本权利、"依法治国,建设社会主义法治国家"的要求等方面,阐述了宪法司法化的必要性。
关键词：宪法司法化 宪法的法律性 建设社会主义 公民基本权利 依法治国 法治国家 权威性 必要性 现状 起源 保障 
全球化视野下的道德教育:普遍性与特殊性被引量：2
《教学与管理（中学版）》2003年第08M期3-4,共2页刘静 
关键词：道德教育 普遍性 特殊性 全球化 全球伦理 学校德育 传统文化 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部