From Haskell to PRES+ Basic Translation Procedures
2001 (English)Report (Other academic)
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.
Place, publisher, year, edition, pages
Linköping, Sweden: IDA, Linköpings Universitet , 2001.
, SAVE Project Report
Haskell descriptions, PRES+ model, formal verification, model checking, temporal logics, embedded systems, real-time systems
IdentifiersURN: urn:nbn:se:liu:diva-23379Local ID: 2818OAI: oai:DiVA.org:liu-23379DiVA: diva2:243693