TY - GEN
T1 - Generalised test tables
T2 - 13th International Conference on Integrated Formal Methods, IFM 2017
AU - Beckert, Bernhard
AU - Cha, Suhyun
AU - Ulbrich, Mattias
AU - Vogel-Heuser, Birgit
AU - Weigl, Alexander
N1 - Publisher Copyright:
© Springer International Publishing AG 2017.
PY - 2017
Y1 - 2017
N2 - In industrial practice today, correctness of software is rarely verified using formal techniques. One reason is the lack of specification languages for this application area that are both comprehensible and sufficiently expressive. We present the concepts and logical foundations of generalised test tables – a specification language for reactive systems accessible for practitioners. Generalised test tables extend the concept of test tables, which are already frequently used in quality management of reactive systems. The main idea is to allow more general table entries, thus enabling a table to capture not just a single test case but a family of similar behavioural cases. The semantics of generalised test tables is based on a two-party game over infinite words. We show how generalised test tables can be encoded into verification conditions for state-of-the-art model checkers. And we demonstrate the applicability of the language by an example in which a function block in a programmable logic controller as used in automation industry is specified and verified.
AB - In industrial practice today, correctness of software is rarely verified using formal techniques. One reason is the lack of specification languages for this application area that are both comprehensible and sufficiently expressive. We present the concepts and logical foundations of generalised test tables – a specification language for reactive systems accessible for practitioners. Generalised test tables extend the concept of test tables, which are already frequently used in quality management of reactive systems. The main idea is to allow more general table entries, thus enabling a table to capture not just a single test case but a family of similar behavioural cases. The semantics of generalised test tables is based on a two-party game over infinite words. We show how generalised test tables can be encoded into verification conditions for state-of-the-art model checkers. And we demonstrate the applicability of the language by an example in which a function block in a programmable logic controller as used in automation industry is specified and verified.
UR - http://www.scopus.com/inward/record.url?scp=85030183070&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-66845-1_9
DO - 10.1007/978-3-319-66845-1_9
M3 - Conference contribution
AN - SCOPUS:85030183070
SN - 9783319668444
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 129
EP - 144
BT - Integrated Formal Methods - 13th International Conference, IFM 2017, Proceedings
A2 - Schneider, Steve
A2 - Polikarpova, Nadia
PB - Springer Verlag
Y2 - 20 September 2017 through 22 September 2017
ER -