Z语言

作品数:93被引量:191H指数:7
导出分析报告
相关领域:自动化与计算机技术更多>>
相关作者:缪淮扣朱关铭庄毅郑国梁彭展更多>>
相关机构:上海大学南京航空航天大学广东工业大学山东大学更多>>
相关期刊:更多>>
相关基金:国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划上海市高等学校科学技术发展基金更多>>
-

检索结果分析

结果分析中...
选择条件:
  • 基金=国家重点基础研究发展计划x
条 记 录,以下是1-5
视图:
排序:
一种形式化组合式建模方法的研究
《计算机技术与发展》2017年第11期106-109,共4页李勇 李揭阳 曹子宁 
国家"973"重点基础研究发展计划项目(2014CB744900);航空科学基金(20150652008)
构件式系统是一种采用构件组合技术实现的结构系统,即在采用单个构件封装简单的业务功能基础上,通过集成多个构件逐步构造新的组合构件来实现比较复杂的业务功能。在开发构件式系统软件的过程中,正确的子构件模型组合方式才有可能构建...
关键词:体系结构分析设计语言 构件式系统 计算树逻辑 Z语言 模型检测 
基于构件交互自动机的AADL模型转换方法研究被引量:2
《计算机技术与发展》2017年第7期68-71,共4页李揭阳 李勇 张福高 
国家"973"重点基础研究发展计划项目(2014CB744900);航空科学基金(20150652008)
构件交互自动机(Component-Interaction Automata,Co-IA)是扩展了构件之间交互描述的自动机。体系结构分析设计语言(Architecture Analysis and Design Language,AADL)是一种基于构件的半形式化体系结构分析和设计语言,是嵌入式系统体...
关键词:体系结构分析设计语言 构件交互自动机 Z语言 模型转换 
基于带数据约束实时系统的互模拟检测方法被引量:1
《计算机技术与发展》2016年第1期6-9,17,共5页李国拯 高正 
航空科学基金(20128052064);中央高校基本科研业务费专项资金(NZ2013306);国家"973"重点基础研究发展计划项目(2014CB744903)
带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统,其广泛存在于航空航天、工业控制、国防等安全攸关系统,并发挥着至关重要的作用。针对这类系统的形式化建模与验证是确保其正确性和可靠性的重要途径。文中首...
关键词:实时系统 接口自动机 Z语言 时间自动机 互模拟检测 
对一类多级安全模型安全性的形式化分析被引量:10
《计算机学报》2006年第8期1468-1479,共12页何建波 卿斯汉 王超 
北京市自然科学基金(4052016);国家自然科学基金(60573042);国家"九七三"重点基础研究发展规划项目基金(G1999035802)资助.
深入分析了MLS的核心思想,给出了MLS在包含多级客体的系统中的表述形式,分析了安全不变式(in-variant)在系统安全定义中的作用.为了保证模型的安全,必须验证模型的不变式满足MLS策略.为了说明不变式验证的重要性,借助Z语言和形式验证工...
关键词:BLP模型 MLS策略 安全不变式 Z语言 Z/EVES定理证明器 
具有冲突约束的RBAC模型的形式化规范与证明被引量:2
《计算机研究与发展》2006年第z2期498-508,共11页袁春阳 贺也平 何建波 周洲仪 
国家"九七三"重点基础研究发展规划基金项目(G1999035802);国家"八六三"高技术研究发展计划基金项目(2002AA141080);国家自然科学基金项目(60073022,60373054)
在实际应用"基于角色的访问控制"(RBAC)模型时,经常遇到由于责任分离等策略而引起的冲突问题,如权限间的互斥等.访问控制操作应满足某些约束条件,以避免冲突的存在.但这些冲突关系相当复杂,如何检测出冲突问题是模型安全实施的重要保证...
关键词:基于角色的访问控制 形式化规范和证明 责任分离 冲突约束 Z语言 
检索报告 对象比较 聚类工具 使用帮助 返回顶部