基于Tecton的验证系统Violet

来源 :华东理工大学学报：自然科学版 | 被引量 : 0次 | 上传用户：monzad

【摘要】

：

在Tecton语言对面向概念的构件进行形式化规范的基础上,创建了Viokt验证系统对构件的性质进行自动验证.Viokt系统是基于重写技术的验证工具,其主要目的是辅助用户发现和理解

【作者】

：

翟洁邵志清

【机构】

：

华东理工大学计算机科学与工程系,华东理工大学计算机科学与工程系

【出处】

：

华东理工大学学报：自然科学版

【发表日期】

：

2005年2期

【关键词】

：

规范验证重写归纳 specification verfication rewrite induction

【基金项目】

：

中国科学院资助项目，重庆市应用基础研究基金，教育部优秀青年教师资助计划

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

在Tecton语言对面向概念的构件进行形式化规范的基础上,创建了Viokt验证系统对构件的性质进行自动验证.Viokt系统是基于重写技术的验证工具,其主要目的是辅助用户发现和理解构件规范的验证,并建立经过验证的软硬件的构件库.描述了系统在可视化和自动化方面的主要特性,并实现了位交换协议的Tecton规范和系统验证.

其他文献

基于启发式规则的新型进化算法在流水车间调度中的应用

针对流水车间调度这一典型的NP难问题，采用了一种新型进化算法——DNA进化算法进行求解，并对算法做了改进。改进的DNA进化算法中引入了交换操作以更好地搜索解空间，并采用黄金分

期刊

FLOWshop调度DNA进化算法启发式规则黄金分割率Flow shop DNA evolutionary algorithm heuristic

可光聚混合聚酸酐的合成与降解

采用甲基丙烯酸酐(或甲基丙烯酰氯)与无毒二元酸反应合成了混合酸酐:甲基丙烯酸酐化癸二酸(MSA)和甲基丙烯酸酐化的1,6-二(对羧基苯氧基)己烷(MCPH).并用1H-NMR、IR表征其结

期刊

聚酸酐光聚合合成降解共聚polyanhydride photopolymerization synthesis degradation cop

基于DNA进化算法的车辆调度问题

在建立一种物流配送车辆调度模型的基础上，针对传统启发式算法对复杂问题搜索效率低、易陷入局部最优的缺点，构造了DNA进化算法求解该问题。将其在个体变异操作中进行了一些改

期刊

车辆调度DNA进化算法优化分裂算子变异算子vehicle scheduling problem DNA evolutionary algorithm

入侵容忍技术在身份认证系统中的应用

结合SITAR分布式入侵容忍体系结构和ITPAS密码认证体系统的特点,提出了一个具有入侵容忍功能的分布式密码认证系统模型,并在设计中考虑了冗余、多样性、代理、共享秘密和分布

期刊

认证密码代理冗余入侵容忍authentication password proxy redundancy intrusion toleranc

基于Tecton的验证系统Violet

其他学术论文