From Haskell to PRES+ Basic Translation Procedures
Luis-Alejandro Cortes, Petru Eles, Zebo Peng · 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 representation 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 electronic systems. 1.