Transforming ASN.1 Specifications into CafeOBJ to assist with Property Checking

TL;DR

This paper presents a method to convert ASN.1 protocol specifications into CafeOBJ algebraic specifications, enabling early property checking and validation of network systems.

Contribution

It introduces a translation approach from ASN.1 to CafeOBJ and demonstrates its potential through initial implementation and a case study.

Findings

Successful translation of ASN.1 to CafeOBJ demonstrated

Enables early validation of system properties before coding

Lays groundwork for automated protocol verification tools

Abstract

The adoption of algebraic specification/formal method techniques by the networks' research community is happening slowly but steadily. We work towards a software environment that can translate a protocol's specification, from Abstract Syntax Notation One (ASN.1 - a very popular specification language with many applications), into the powerful algebraic specification language CafeOBJ. The resulting code can be used to check, validate and falsify critical properties of systems, at the pre-coding stage of development. In this paper, we introduce some key elements of ASN.1 and CafeOBJ and sketch some first steps towards the implementation of such a tool including a case study.