文献类型：期刊文献

中文题名：基于Tecton的验证系统Violet

英文题名：Proof System Violet Based on Tecton

作者：翟洁[1];邵志清[1]

机构：[1]华东理工大学计算机科学与工程系,上海200237

年份：2005

卷号：31

期号：2

起止页码：198

中文期刊名：华东理工大学学报（自然科学版）

外文期刊名：Journal of East China University of Science and Technology

收录：CSTPCD;;EI(收录号：2005209110091);Scopus;北大核心:【北大核心2004】；CSCD:【CSCD2011_2012】；

基金：国家自然科学基金(60373075);教育部科学技术研究重点项目(01077);教育部优秀青年教师资助计划项目

语种：中文

中文关键词：规范;验证;重写;归纳

外文关键词：specification; verfication; rewrite; induction

摘要：在Tecton语言对面向概念的构件进行形式化规范的基础上,创建了Violet验证系统对构件的性质进行自动验证。Violet系统是基于重写技术的验证工具,其主要目的是辅助用户发现和理解构件规范的验证,并建立经过验证的软硬件的构件库。描述了系统在可视化和自动化方面的主要特性,并实现了位交换协议的Tecton规范和系统验证。
On the basis of Tecton specifications of component concepts, we build verification system Violet to prove properties of components automatically. Violet is a proof tool based on rewriting techniques. Its main goal is to help the user find proofs and understand proofs and build libraries of verified software or hardware components. We describe the novel features of Violet in the aspects of proof visualization and proof automation. At last we present the Tecton specification and Violet verification of the alternating bit protocol.