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