TY - GEN
T1 - Relational test tables
T2 - 2020 IEEE/ACM 8th International Conference on Formal Methods in Software Engineering, FormaliSE 2020
AU - Weigl, Alexander
AU - Ulbrich, Mattias
AU - Cha, Suhyun
AU - Beckert, Bernhard
AU - Vogel-Heuser, Birgit
N1 - Publisher Copyright:
© 2020 Copyright held by the owner/author(s). Publication rights licensed to ACM.
PY - 2020/10/7
Y1 - 2020/10/7
N2 - A wide range of interesting program properties are relational, i.e., they described a relation between two program runs. Two prominent relational properties are the regression verification (proving conditional program equivalence), and non-interference (proving the absence of information flow). The verification of relational properties is hardly accessible to engineers due to the lack of appropriate specification languages for relational properties. In previous work, we introduced the concept of generalized test tables: a table-based specification language, which allows the tight temporal specification of functional (nonrelational) properties for reactive systems. We introduce relational test tables an extension of generalized test tables for the specification of relational properties. Relational test tables support specification of κ-safety properties (a super set of relational properties) between κ = 2 program runs. We show the applicability of relational test tables by specifying and verifying change scenarios and information flow of reactive systems. We provide an implementation of the verification pipeline for programs following the IEC 61131-3 coding standard under http://github.com/ VerifAPS/verifaps-lib.
AB - A wide range of interesting program properties are relational, i.e., they described a relation between two program runs. Two prominent relational properties are the regression verification (proving conditional program equivalence), and non-interference (proving the absence of information flow). The verification of relational properties is hardly accessible to engineers due to the lack of appropriate specification languages for relational properties. In previous work, we introduced the concept of generalized test tables: a table-based specification language, which allows the tight temporal specification of functional (nonrelational) properties for reactive systems. We introduce relational test tables an extension of generalized test tables for the specification of relational properties. Relational test tables support specification of κ-safety properties (a super set of relational properties) between κ = 2 program runs. We show the applicability of relational test tables by specifying and verifying change scenarios and information flow of reactive systems. We provide an implementation of the verification pipeline for programs following the IEC 61131-3 coding standard under http://github.com/ VerifAPS/verifaps-lib.
KW - Change specification
KW - Formal software verification
KW - Information flow
KW - Relational verification
KW - Software evolution
UR - http://www.scopus.com/inward/record.url?scp=85092774051&partnerID=8YFLogxK
U2 - 10.1145/3372020.3391566
DO - 10.1145/3372020.3391566
M3 - Conference contribution
AN - SCOPUS:85092774051
T3 - Proceedings - 2020 IEEE/ACM 8th International Conference on Formal Methods in Software Engineering, FormaliSE 2020
SP - 77
EP - 86
BT - Proceedings - 2020 IEEE/ACM 8th International Conference on Formal Methods in Software Engineering, FormaliSE 2020
PB - Association for Computing Machinery
Y2 - 13 July 2020
ER -