From Haskell to PRES+ Basic Translation Procedures
SAVE Project Report, Dept. of Computer and Information Science, Linköping University, April 2001.
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.
|SAVE01.pdf||Adobe Acrobat portable document|
|SAVE01.ps.gz||postscript 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.