-
题名形式化方法概貌
被引量:74
- 1
-
-
作者
王戟
詹乃军
冯新宇
刘志明
-
机构
国防科技大学计算机学院
高性能计算国家重点实验室(国防科技大学)
中国科学院软件研究所
天基综合信息系统重点实验室(中国科学院软件研究所)
南京大学计算机科学与技术系
计算机软件新技术国家重点实验室(南京大学)
西南大学计算机与信息科学学院
西南大学软件研究与创新中心
-
出处
《软件学报》
EI
CSCD
北大核心
2019年第1期33-61,共29页
-
基金
国家自然科学基金(61532007
61632005
+1 种基金
61672435
61732019)~~
-
文摘
形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.
-
关键词
形式化方法
形式规约
形式验证
程序设计方法学
软件开发
-
Keywords
formal method
formal specification
formal verification
programming methodology
software development
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名面向新兴系统的形式化建模与验证方法专题前言
- 2
-
-
作者
陈振邦
冯新宇
刘志明
-
机构
国防科技大学计算机学院
南京大学计算机科学与技术系
南京大学计算机软件新技术国家重点实验室
西南大学计算机与信息科学学院
西南大学软件研究与创新中心
-
出处
《软件学报》
EI
CSCD
北大核心
2020年第8期2283-2284,共2页
-
文摘
形式化方法是计算机科学的重要理论基础.它以严格的数学化和机械化方法为基础来规约、构建和验证计算系统,是改善和确保计算系统质量的重要方法.近年来,随着相关技术的发展,形式化方法已经在越来越多的新兴系统中得到应用并取得显著效果.为了记录中国学者在新兴系统的形式化建模与验证理论、方法、工具和应用等方面的最新研究成果,特设立此专题.
-
关键词
形式化方法
计算机科学
最新研究成果
数学化
验证计算
规约
新兴
专题
-
分类号
TP311.52
[自动化与计算机技术—计算机软件与理论]
-
-
题名安全强化学习算法及其在CPS智能控制中的应用
被引量:2
- 3
-
-
作者
赵恒军
李权忠
曾霞
刘志明
-
机构
西南大学计算机与信息科学学院软件学院
西北工业大学智能嵌入式软件研究中心
西南大学软件研究与创新中心
-
出处
《软件学报》
EI
CSCD
北大核心
2022年第7期2538-2561,共24页
-
基金
国家自然科学基金(61902325,62032019,61972385,61732019,61702425)
西南大学国家人才建设项目(SWU116007)
-
文摘
信息物理系统(cyber-physical system,CPS)的安全控制器设计是一个热门研究方向,现有基于形式化方法的安全控制器设计存在过度依赖模型、可扩展性差等问题.基于深度强化学习的智能控制可处理高维非线性复杂系统和不确定性系统,正成为非常有前景的CPS控制技术,但是缺乏对安全性的保障.针对强化学习控制在安全性方面的不足,围绕一个工业油泵控制系统典型案例,开展安全强化学习算法和智能控制应用研究.首先,形式化了工业油泵控制的安全强化学习问题,搭建了工业油泵仿真环境;随后,通过设计输出层结构和激活函数,构造了神经网络形式的油泵控制器,使得油泵开关时间的线性不等式约束得到满足;最后,为了更好地权衡安全性和最优性控制目标,基于增广拉格朗日乘子法设计实现了新型安全强化学习算法.在工业油泵案例上的对比实验表明,该算法生成的控制器在安全性和最优性上均超越了现有同类算法.在进一步评估中,所生成神经网络控制器以90%的概率通过了严格形式化验证;同时,与理论最优控制器相比实现了低至2%的最优目标值损失.所提方法有望推广至更多应用场景,实例研究的方案有望为安全智能控制和形式化验证领域其他学者提供借鉴.
-
关键词
强化学习
智能控制
信息物理系统
安全验证
工业油泵
-
Keywords
reinforcement learning
intelligent control
cyber-physical system
safety verification
industrial oil pump
-
分类号
TP273
[自动化与计算机技术—检测技术与自动化装置]
TP181
[自动化与计算机技术—控制理论与控制工程]
-