杨红丽

作品数：5被引量：5H指数：2
导出分析报告
供职机构：西安邮电学院计算机学院计算机系更多>>
发文主题：形式化方法形式化验证FM形式逻辑离散数学更多>>
发文领域：自动化与计算机技术交通运输工程更多>>
发文期刊：《计算机应用》《西北工业大学学报》更多>>
所获基金：国家自然科学基金青年科技基金国家高技术研究发展计划更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-5
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于PVS的飞机订票系统的形式化描述与验证被引量：1
《西安邮电学院学报》2001年第3期1-5,共5页杨红丽 刘建元 韩俊刚 
国家 8 6 3资助项目
形式化方法主要应用于安全性第一的系统的规范与形式验证。原型证明系统PVS为开发和分析形式化规范和验证提供了一个集成化环境。本文介绍PVS系统的证明方法和特点 ,并利用PVS系统对飞机订票系统的需求给出了形式化规范 ,对部分关键属...
关键词：PVS 形式化规范 形式化证明 
实时系统状态空间分析的一种算法
《计算机应用》2000年第S1期62-65,共4页杜慧敏 杨红丽 韩俊刚 
自然科学基金!(694730 1 7)
提出了一种生成实时系统可达状态的算法 ,该算法生成一个较小的状态空间 ,但仍然保留了足够的时间信息用于分析。同时给出一个实例来说明算法的有效性 ,并与其它方法进行了比较。
关键词：形式化验证 互模拟 实时自动机 区域图 可达图 
基于形式化的面向对象开发方法(FMOO)
《计算机应用》2000年第5期24-27,共4页杨红丽 王曙燕 韩俊刚 
原邮电部高等院校中青年教师科学基金
主要讨论如何把形式化方法应用于面向对象的软件开发过程中 ,以提高软件的安全性和可靠性 ,并给出一个小型交通控制系统的形式化规范和验证实例。
关键词：面向对象 形式化方法 软件开发 交通控制 
一种基于时态逻辑的有限状态系统验证方法被引量：2
《西北工业大学学报》2000年第1期111-115,共5页杜慧敏 杨红丽 高德远 韩俊刚 
国家自然科学基金!694 73 0 17
LPTL ( Linear Proposition Temporal Logic)与自动机之间有着紧密的联系 ,结合 LPTL语义和语法 ,提出一种从 LPTL公式导出 Büchi自动机的方法。导出的 Büchi自动机所接受的语言准确地表达了 LPTL公式所描述的特性。从而把由 LPTL公...
关键词：命题时态逻辑 形式化验证 有限状态系统 自动机 
形式化方法(FM)被引量：2
《西安邮电学院学报》1999年第2期4-7,47,共5页杨红丽 
原邮电部中青年科技基金
传统的开发方法一般基于自然语言的描述，不能表达明确的语义；本文介绍的形式化方法（ＦＭ）是基于形式逻辑和离散数学的，特别适用于安全重要性系统的说明、设计和构造。
关键词：形式化方法 形式逻辑 离散数学 FM 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部