Linköping University: Students Alumni Trade and Industry/Society Internal Search
SAVE01

From Haskell to PRES+ Basic Translation Procedures

Luis Alejandro Cortes
 
Petru Eles Author homepage
Zebo Peng Author homepage

SAVE Project Report, Dept. of Computer and Information Science, Linköping University, April 2001.

ABSTRACT
We define in this report some basic procedures to translate Haskell descriptions (based on a library of Skeletons) into PRES+ models. In this way, a system initially described in Haskell, may be transformed into a representation that might be formally verified. Thus the representa-tion of the system is verified using formal methods by model-checking the model against a set of required properties expressed by temporal logics. This work has been done in the frame of the SAVE project, which aims to study the specification and verification of heterogeneous elec-tronic systems.


Related files:
SAVE01.pdfAdobe Acrobat portable document
SAVE01.ps.gzpostscript document, compressed (with gzip)


[AEP01] Luis Alejandro Cortes, Petru Eles, Zebo Peng, "From Haskell to PRES+ Basic Translation Procedures", SAVE Project Report, Dept. of Computer and Information Science, Linköping University, April 2001.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)