Formal verification in LabVIEW programs

[EmptyStackExn]

Hi everyone!

My name is Hai Nguyen Van and I work at the Institut de Physique du Globe de Paris. My main work is based on the construction of a ground station for a satellite that will be launched in October, 2012. However as a computer scientist, it has become to me obvious that critical softwares need to be proved by formal methods (cf. NASA Langley Formal Methods Workshop) or checked by static analyzers (cf. new research on static analyzers based on abstract interpretation for Airbus systems).

You moreover may know that current state of LabVIEW programs interoperability is low and graphical interface does not allow any correct formalization. This is the reson why, I wanted to know if there was a way to formalize a LabVIEW code for the popular vi format. Is there a way to get a Dataflow Intermediate Representation (DFIR) translator.

Regards,

Hai Nguyen Van

Department of Mathematics, Universite Paris Diderot

Institut de Physique du Globe de Paris

[Eric.M]

Hello Hai,

At this time, there is no such way as NASA to certify a LabVIEW code. It may come out to National Instruments to create a similar workshop as LabVIEW releay gets standardized.

Concerning the DFIR representation of a code, it's not made public as of now, to preserve the high level representation of the graphical system design. The upcoming versions of LabVIEW will change their LLVM so the DFIR handling might be different but most likely it will still remain a private feature for internal purposes.

https://www.ni.com/en/support/documentation/supplemental/10/ni-labview-compiler--under-the-hood.html

Best regards,

Eric