Resumen:
PROMELA (Process Meta Language) is a high-level specification language designed for modeling interactions in distributed systems. PROMELA is used as the input language for the model checker SPIN (Simple Promela INterpreter). The main characteristics of PROMELA are non-determinism, process communication through synchronous as well as asynchronous channels, and the possibility to dynamically create instances of processes.In this paper, we introduce a bottom-up, fixpoint semantics that models the behavior of PROMELA programs. This work is the first step for a more ambitious goal where analysis and verification techniques based on abstract interpretation would be defined on top of such semantics.
Descargas:
Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)
Descarga el artículo haciendo click aquí.
Ver la referencia en formato Bibtex
@inproceedings{prole:2019:023,
title={{Towards a bottom-up fixpoint semantics that models the behavior of PROMELA programs}},
author={Marco Comini and Francesco Saverio Comisso and Alicia Villanueva},
url={http://hdl.handle.net/11705/PROLE/2019/023},
booktitle={PROLE2019},
year={2019},
publisher={SISTEDES},
crossref={prole2019caceres}
}
@proceedings{prole2019caceres,
title={{Actas de las XIX Jornadas de Programaci{\'o}n y Lenguajes (PROLE 2019)}},
editor={Alpuente, M., Sapi{\~n}a, J. y Rodr{\'i}guez Echeverr{\'i}a, R.},
booktitle={PROLE2019},
year={2019},
publisher={SISTEDES}
}
Copiar al portapapeles |
Cerrar