徐蔚文

作品数：4被引量：7H指数：1
导出分析报告
供职机构：上海交通大学电子信息与电气工程学院计算机科学与工程系更多>>
发文主题：通信协议身份认证协议参数化系统伪随机函数CTL更多>>
发文领域：自动化与计算机技术电子电信理学更多>>
发文期刊：《计算机学报》《计算机工程》更多>>
所获基金：国家自然科学基金更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-4
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
自动验证参数化Leader Election 协议
《计算机工程》2003年第18期14-15,153,共3页徐蔚文 陆鑫达 
国家自然科学基金资助项目(60173103)
讨论了一类Leader Election （LE）协议，该类协议通常运行在允许进程随时加入或崩溃的动态环境中，给出了LE协议的参数化版本，即考虑分布式系统中的进程数目任意多的情况。并提出了一种自动验证参数化LE协议的方法，用线性算数约束来...
关键词：LE协议 参数化系统 形式验证 符号模型检测工具 
具有公平性约束的CTL部分状态空间模型检测被引量：1
《计算机工程》2003年第5期10-12,共3页徐蔚文 陆鑫达 
国家自然科学基金资助项目 (60173103)
检测部分状态空间是近年来出现的有效解决状态爆炸的模型检测技术，部分Kripke 结构是描述部分状态空间的形式框架。文章主要讨论一类具有公平性约束条件的CTL（计算树逻辑）模型检测问题。定义了部分公平Kripke结构和公平序，分别来表...
关键词：公平性约束 CTL 部分状态空间 模型检测 部分Kripke结构 计算树逻辑 命题逻辑 
身份认证协议的模型检测分析被引量：6
《计算机学报》2003年第2期195-201,共7页徐蔚文 陆鑫达 
国家自然科学基金 ( 6 0 17310 3)资助 .
提出一个直观、易用的模型来模拟和验证身份认证协议 ,并给出基于Spin(模型检测工具 )的实现 ,它不仅可以模拟多对参与者同时进行会话 ,而且还有效缩减了状态空间 ,从而避免了以前文献中提到的状态爆炸现象 .同时该文用Needham Schroede...
关键词：身份认证协议 模型检测 分析 伪随机函数 通信协议 
通信延迟对机器选择的影响
《计算机工程》2001年第9期11-13,共3页曾志勇 徐蔚文 陆鑫达 
国家自然科学基金项目(69773014)
讨论了工作站网络“ＮＯＷ”系统在高性能计算方面的应用，指出通信延迟对计算性能具有重要的影响，并给出了实验作出经验分析。
关键词：工作站网络 高性能计算 通信延迟 网络计算 通信协议 计算机网络 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部