Toward automatic generation of promela models from SDL specification
Boštjan Vlaovič, Aleksander Vreže, Zmago Brezočnik, Tatjana Kapus · Proceedings of the 8th International Conference on Telecommunications, 2005. ConTEL 2005. · 2005
Abstract — This paper presents our research in the domain of mechanical extraction of a model from an SDL (Specification and Description Language) specification of a system. We use formal verification tool Spin (Simple Promela Interpreter) and Promela (Process Meta-Language) language for the description of the model. With the model checking technique the model’s accordance with the system correctness requirements can be established with mathematical accuracy. The model can be generated manually or mechanically. If it is to be prepared manually, we will need an expert with the detailed knowledge of the system and both languages. The quality of the model is directly influenced by the expert. The process is prone to the incorrect modelling of the system’s properties. In this paper we present the most critical parts of mechanical creation of the models in Promela. Additionally, we present challenges, research directions and some solutions for the automatic generation of models from an SDL specification. I.