将 ASN.1 规约转换为 CafeOBJ 以辅助性质检验
软件工程
2011-03-16 v1 计算机科学中的逻辑
摘要
网络研究界对代数规约/形式化方法技术的采用正在缓慢但稳步地推进。我们致力于开发一种软件环境，能够将协议规约从抽象语法记法一（ASN.1——一种具有众多应用的流行规约语言）翻译为强大的代数规约语言 CafeOBJ。生成的代码可用于在开发的前编码阶段检查、验证和证伪系统的关键性质。在本文中，我们介绍了 ASN.1 和 CafeOBJ 的一些关键要素，并概述了实现此类工具的初步步骤，包括一个案例研究。
引用
@article{arxiv.1103.2787,
title = {Transforming ASN.1 Specifications into CafeOBJ to assist with Property Checking},
author = {Konstantinos Barlas and George Koletsos and Petros Stefaneas},
journal= {arXiv preprint arXiv:1103.2787},
year = {2011}
}
备注
8 pages, 12 figures