BARNAT, Jiří, Petr BAUCH, Nikola BENEŠ, Luboš BRIM, Jan BERAN a Tomáš KRATOCHVÍLA. Analysing Sanity of Requirements for Avionics Systems. Formal Aspects of Computing. 2016, roč. 28, č. 1, s. 45-63. ISSN 0934-5043. Dostupné z: https://dx.doi.org/10.1007/s00165-015-0348-9. |
Další formáty:
BibTeX
LaTeX
RIS
@article{1317538, author = {Barnat, Jiří and Bauch, Petr and Beneš, Nikola and Brim, Luboš and Beran, Jan and Kratochvíla, Tomáš}, article_number = {1}, doi = {http://dx.doi.org/10.1007/s00165-015-0348-9}, keywords = {Requirement engineering; Linear temporal logic; Sanity checking}, language = {eng}, issn = {0934-5043}, journal = {Formal Aspects of Computing}, title = {Analysing Sanity of Requirements for Avionics Systems}, volume = {28}, year = {2016} }
TY - JOUR ID - 1317538 AU - Barnat, Jiří - Bauch, Petr - Beneš, Nikola - Brim, Luboš - Beran, Jan - Kratochvíla, Tomáš PY - 2016 TI - Analysing Sanity of Requirements for Avionics Systems JF - Formal Aspects of Computing VL - 28 IS - 1 SP - 45-63 EP - 45-63 SN - 09345043 KW - Requirement engineering KW - Linear temporal logic KW - Sanity checking N2 - In the last decade it became a common practice to formalise software requirements to improve the clarity of users' expectations. In this work we build on the fact that functional requirements can be expressed in temporal logic and we propose new sanity checking techniques that automatically detect flaws and suggest improvements of given requirements. Specifically, we describe and experimentally evaluate approaches to consistency and redundancy checking that identify all inconsistencies and pinpoint their exact source (the smallest inconsistent set). We further report on the experience obtained from employing the consistency and redundancy checking in an industrial environment. To complete the sanity checking we also describe a semi-automatic completeness evaluation that can assess the coverage of user requirements and suggest missing properties the user might have wanted to formulate. The usefulness of our completeness evaluation is demonstrated in a case study of an aeroplane control system. ER -
BARNAT, Jiří, Petr BAUCH, Nikola BENEŠ, Luboš BRIM, Jan BERAN a Tomáš KRATOCHVÍLA. Analysing Sanity of Requirements for Avionics Systems. \textit{Formal Aspects of Computing}. 2016, roč.~28, č.~1, s.~45-63. ISSN~0934-5043. Dostupné z: https://dx.doi.org/10.1007/s00165-015-0348-9.
|