Title: Towards a correct translation from ASN.1 into CafeOBJ

Authors: Konstantinos Barlas, George Koletsos, Petros Stefaneas, Iakovos Ouranos

Addresses: School of Electrical and Computer Engineering, National Technical University of Athens, Polytexneioupoli Zografou, Iroon Polytexneiou 9, 15780, Athens, Greece. ' School of Electrical and Computer Engineering, Polytexneioupoli Zografou, Iroon Polytexneiou 9, 15780, Athens, Greece. ' Department of Mathematics, School of Applied Mathematical and Physical Sciences, Polytexneioupoli Zografou, Iroon Polytexneiou 9, 15780, Athens, Greece. ' Hellenic Civil Aviation Authority, Heraklion Airport, Kalamatas 18, 71409, Heraklion, Crete, Greece; School of Electrical and Computer Engineering, National Technical University of Athens, Iroon Polytexneiou 9, 15780, Athens, Greece

Abstract: The adoption of algebraic specification techniques by the networks| research community is happening slowly but steadily. We present a software environment that can translate a protocol|s specification, from Abstract Syntax Notation One (ASN.1), into the powerful algebraic specification language CafeOBJ. The resulting code can be used to check critical properties of systems. In this paper, we sketch some first steps towards the implementation of such a tool including a case study.

Keywords: specifications; Abstract Syntax Notation One; ASN.1; CafeOBJ; formal verification; algebraic specification; reasoning-based intelligent systems; correct translation; protocol specification; property check.

DOI: 10.1504/IJRIS.2010.036878

International Journal of Reasoning-based Intelligent Systems, 2010 Vol.2 No.3/4, pp.300 - 309

Published online: 12 Nov 2010 *

Full-text access for editors Access for subscribers Purchase this article Comment on this article