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.

Základní údaje

Originální název

Analysing Sanity of Requirements for Avionics Systems

Autoři

BARNAT, Jiří (203 Česká republika, garant, domácí), Petr BAUCH (203 Česká republika, domácí), Nikola BENEŠ (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí), Jan BERAN (203 Česká republika) a Tomáš KRATOCHVÍLA (203 Česká republika)

Vydání

Formal Aspects of Computing, 2016, 0934-5043

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

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

Impakt faktor

Impact factor: 1.041

Kód RIV

RIV/00216224:14330/16:00089171

Organizační jednotka

Fakulta informatiky

DOI

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

UT WoS

000372262000003

Klíčová slova anglicky

Requirement engineering; Linear temporal logic; Sanity checking

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 17. 4. 2018 08:34, prof. RNDr. Luboš Brim, CSc.

Anotace

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.

Návaznosti

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

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

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

7H13001, projekt VaV

Název: Critical System Engineering Acceleration (Akronym: CRYSTAL (MSMT))

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Critical System Engineering Acceleration

Citovat

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.

@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.

Podrobný výpis o publikaci