形式化设计

作品数：24被引量：44H指数：4
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：钱振江黄皓宋方敏李康杰刘苇更多>>
相关机构：南京大学常熟理工学院解放军信息工程大学伦敦大学更多>>
相关期刊：《电子机械工程》《控制理论与应用》《湖南包装》《小型微型计算机系统》更多>>
相关基金：国家自然科学基金江苏省高校自然科学研究项目江苏省“六大人才高峰”高层次人才项目国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
多序列比对算法族的形式化设计与生成被引量：3
《计算机工程与科学》2020年第8期1383-1392,共10页张旭初 石海鹤 
国家自然科学基金(61662035,61762049,61862033)。
多序列比对问题是生物信息学研究的重要部分,是解决物种进化关系、基因组序列分析等问题的基础。多序列比对算法具有很高的专用性,不同的算法适用于不同的研究环境。目前常用的多序列比对软件是在生物信息学理论指导下利用多个子算法装...
关键词：多序列比对算法 特征模型 产生式编程 算法构件 PAR平台 
机器人形式化验证方法综述
《信息记录材料》2019年第12期1-4,共4页刘永梅 
国家自然科学基金项目面向机器人的几何代数高阶逻辑形式化理论(61572331)资助
机器人的形式化验证方法通常很复杂,目前还没有一种通用的方法。本文对机器人的形式化设计和验证的概念进行介绍,描述其框架和基本方法。调查多个设计和验证项目,阐述项目的验证目标、方法、优缺点和进展情况。在总结研究现状的基础上,...
关键词：机器人 形式化设计 形式化验证 定理证明 模型检验 
典型安全网关的形式化设计与证明
《计算机科学》2017年第9期142-147,共6页王瑞云 赵国磊 常朝稳 王雪健 
面向用户的可信云计算环境安全研究(61572517)资助
传统上依靠经验设计的安全网关侧重于功能实现,缺少严格的安全模型。对此,针对一种典型安全网关,首先根据其安全需求给出相应的安全策略,然后利用BLP模型对给出的安全策略进行形式化建模并对安全模型的内部一致性进行证明,最后对安全网...
关键词：典型安全网关 形式化设计 BLP模型 功能规约 一致性验证 Isabelle/HOL 
微内核架构内存管理的形式化设计和验证方法研究被引量：4
《电子学报》2017年第1期251-256,共6页钱振江 刘永俊 姚宇峰 汤力 黄皓 宋方敏 
国家自然科学基金(No.61402057);江苏省科技计划自然科学研究项目(No.BK20140418);中国博士后科学基金(No.2015M571737);江苏省"六大人才高峰"高层次人才项目(No.2011-DZXX-035);江苏省高校自然科学研究项目(No.12KJB520001)
由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条...
关键词：操作系统 内存管理 形式化设计 形式化验证 定理证明 
操作系统汇编级形式化设计和验证方法被引量：3
《软件学报》2016年第12期3143-3157,共15页钱振江 黄皓 宋方敏 
国家自然科学基金(61402057);江苏省科技计划自然科学研究项目(BK20140418);中国博士后科学基金(2015M571737);江苏省“六大人才高峰”高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)~~
由于系统的巨大规模,操作系统设计和实现的正确性很难用传统的方法进行描述和验证.在汇编层形式化地对系统模块的功能语义进行建模,提出一种汇编级的系统状态模型,作为汇编语言层设计和验证的纽带.通过定义系统状态模型的合法状态和状...
关键词：操作系统 正确性验证 形式化方法 系统状态模型 
“技上计” 2014 威尼斯双年展中国馆大型特展“共谋·共生”展览空间设计
《建筑技艺》2015年第5期12-17,共6页郭馨 高岩 
威尼斯建筑双年展一直以来都受到世界各界的广泛关注,9月20日在威尼斯建筑双年展的中国国家馆中举办的大型特展"共谋·共生"是本届中国馆最大规模的展中展,特针对本次特展的展览空间设计、节点设计及施工过程进行全面的梳理和解读。
关键词：中国传统“基本原则” 中国“现代性” 系统性设计 系统性构造设计 去形式化设计 
带扰动控制系统的形式化设计
《控制理论与应用》2015年第2期178-186,共9页张晋津 张严 朱朝晖 
国家自然科学基金项目(11426136;60973045);江苏省自然科学基金项目(BK20130735);江苏省高校自然科学基金项目(13KJB520012;13KJB520011)资助~~
利用有限抽象进行控制系统的形式化分析与设计是目前研究较多的一类控制系统分析与设计方法.本文提出两种方法,使用有限抽象,构造出两种控制器,使带扰动的控制系统满足时序逻辑规范.为此,首先在时序逻辑规范上引入"弱化"转换函数和"强化...
关键词：反馈控制 控制系统设计 带扰动控制系统 时序逻辑 有限抽象 
操作系统形式化设计与安全需求的一致性验证研究被引量：6
《计算机学报》2014年第5期1082-1099,共18页钱振江 黄皓 宋方敏 
国家自然科学基金创新研究群体基金(60721002);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001);CSLG科研项目(QT1312)资助~~
采用数学形式化方法对操作系统进行设计和验证可以保证系统的高度安全性.目前已有的操作系统形式化研究工作主要是验证系统的实现在代码级的程序正确性.提出一种操作系统形式化设计和验证的方法,采用操作系统对象语义模型(OSOSM)对系统...
关键词：操作系统 形式化设计 安全需求 一致性验证 定理证明 信息安全 网络安全 
微内核架构文件系统的形式化设计与验证方法研究被引量：4
《小型微型计算机系统》2013年第10期2261-2266,共6页钱振江 唐洪英 李康杰 黄皓 宋方敏 
国家"八六三"高技术研究发展计划项目(2011AA01A202)资助;国家自然科学基金创新研究群体基金项目(60721002)资助;江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035)资助;江苏省高校自然科学基金项目(12KJB520001)资助
文件系统作为数据存储和管理的功能模块,其正确性是操作系统安全性的重要方面.采用形式化方法对微内核架构文件系统进行设计,使用操作系统对象语义模型(OSOSM)框架提出微内核架构文件系统的状态自动机模型,并依此描述系统调用的功能语...
关键词：文件系统 微内核架构 形式化设计 形式化验证 正确性断言 ISABELLE HOL 
PLC程序形式化的设计与验证被引量：3
《华侨大学学报（自然科学版）》2013年第3期241-246,共6页齐鹏飞 罗继亮 陈雪琨 
国家青年自然科学基金资助项目(60904018);福建省高等学校新世纪优秀人才支持计划项目(11FJRC01);福建省自然科学基金资助项目(2010J01339;2011J01352);福建省高校杰出青年科研人才培育计划项目(JA10004);中央高校基本科研业务费专项基金资助项目(JB-SJ1006)
从形式化方法的角度出发,阐述可编程逻辑控制器(PLC)程序的形式化设计和验证方法的相关研究.在形式化设计方面,分析了根据Petri网和自动机模型判断程序正确性和可靠性的研究成果;在形式化验证方面,分析了PLC语言与形式化模型的转换和基...
关键词：可编程逻辑控制器 形式化设计 PETRI网 自动机 定理证明 模型验证 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部