Companion Page for INDIN'17

This is the companion page for the paper Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive Systems at the INDIN'17 conference. Here, we publish the formal models of both experiments:

feasibility example (first experiment) [tar.bz2]

The feasibility example covers the analog sensor function block, which maps sensor values over one domain to another domain via a learned linear regression. In the archive, you find

• The codesys project (Analogsensor_Reduziert2.project)
• also in OpenPLCXML (Analogsensor_Reduziert2.xml) and plain text (Analogsensor_Reduziert2.st)
• The SMV modules are in Analogsensor_Reduziert2.weigl.smv and are all runnable.

            nuXmv -source ic3.xmv Analogsensor_Reduziert2.weigl.smv
          

expandability example (second experiment) [tar.bz2]

The expandability example covers the previous function block of the analog sensor and combines it with a diagnostic block. The archive is similar to the one above; it also contains the codesys project, PCLOpenXML and the plain text. The SMV model is in System.smv and different scenarios are in the folder testruns/.

More information on generalized test table can be found in the following two papers INDIN'17 and IFM'17. There is also the tool geteta with the graphical interface STVS.