Translating HCL Programs into Petri Nets - Lima, Ricardo Massa Ferreira; Lins, Rafael Dueire (Anais do Simpósio Brasileiro de Engenharia de Software (SBES); 2000: Anais do XIV Simpósio Brasileiro de Engenharia de SoftwareDO - 10.5753/sbes.2000.25926, 2000)
Haskell# is a parallel extension to lazy functional language Haskell. The sequential part of programs is declared using standard Haskell. This reduces code development costs and increases its reliability by reusing existing and previously tested (or formally verified) Haskell modules. The structure of a process network (of possibly heterogeneous processors) is defined by Haskell# Coordination Language (HCL), also used for task-to-processor allocation. ln this work, we present an environment for analyzing formal properties of the communication structure of Haskell# programs. This environment contains a compiler that translates an HCL program into Petri nets, a well established family of formal specification techniques for modelling non-deterministic concurrent systems. Petri nets allow the analysis of a wide spectrum of properties, such as liveness, boundedness, and deadlock-trap.