Formulating Requirements with FRET for PLCVerif

This report describes two months work on integrating PLCVerif and FRET. PLCVerif is a tool developed at CERN to formally verify PLC programs, while FRET is a tool for specification, formalization and validation of requirements in a user friendly way. PLCVerif already offers several user friendly possibilities, but these have their own limits and lack useful features, such as simulation of the requirement. I added the possibility of using FRET for the specification and formalization of requirement, integrated into the user interface of PLCVerif. This enables requirement engineers to write requirements more freely and also to better understand and validate their requirements.