Analysing Sanity of Requirements for Avionics Systems

J 2016

Analysing Sanity of Requirements for Avionics Systems

BARNAT, Jiří, Petr BAUCH, Nikola BENEŠ, Luboš BRIM, Jan BERAN et. al.

Basic information

Original name

Analysing Sanity of Requirements for Avionics Systems

Authors

BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution), Petr BAUCH (203 Czech Republic, belonging to the institution), Nikola BENEŠ (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Jan BERAN (203 Czech Republic) and Tomáš KRATOCHVÍLA (203 Czech Republic)

Edition

Formal Aspects of Computing, 2016, 0934-5043

Other information

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

Impact factor

Impact factor: 1.041

RIV identification code

RIV/00216224:14330/16:00089171

Organization unit

Faculty of Informatics

DOI

http://dx.doi.org/10.1007/s00165-015-0348-9

UT WoS

000372262000003

Keywords in English

Requirement engineering; Linear temporal logic; Sanity checking

Abstract

V originále

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.

Links

MUNI/A/1159/2014, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.

Investor: Masaryk University, Category A

7H13001, research and development project

Name: Critical System Engineering Acceleration (Acronym: CRYSTAL (MSMT))

Investor: Ministry of Education, Youth and Sports of the CR

Citovat

BARNAT, Jiří, Petr BAUCH, Nikola BENEŠ, Luboš BRIM, Jan BERAN and Tomáš KRATOCHVÍLA. Analysing Sanity of Requirements for Avionics Systems. Formal Aspects of Computing. 2016, vol. 28, No 1, p. 45-63. ISSN 0934-5043. Available from: https://dx.doi.org/10.1007/s00165-015-0348-9.

@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 and Tomáš KRATOCHVÍLA. Analysing Sanity of Requirements for Avionics Systems. \textit{Formal Aspects of Computing}. 2016, vol.~28, No~1, p.~45-63. ISSN~0934-5043. Available from: https://dx.doi.org/10.1007/s00165-015-0348-9.

Detailed Information on Publication Record