Checking Sanity of Software Requirements

D 2012

Checking Sanity of Software Requirements

BARNAT, Jiří, Petr BAUCH a Luboš BRIM

Základní údaje

Originální název

Checking Sanity of Software Requirements

Autoři

BARNAT, Jiří (203 Česká republika, domácí), Petr BAUCH (203 Česká republika, garant, domácí) a Luboš BRIM (203 Česká republika, domácí)

Vydání

Thessaloniki, Proceedings of the 10th International Conference on Software Engineering and Formal Methods, od s. 48-62, 15 s. 2012

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Řecko

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/12:00057623

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-33825-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-33826-7_4

Klíčová slova anglicky

model checking; sanity checking; consistency; vacuity; completeness

Štítky

best

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 23. 4. 2013 13:25, RNDr. Pavel Šmerk, Ph.D.

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 techniques that automatically detect flaws and suggest improvements of given requirements. Specifically, we describe and experimentally evaluate new approaches to consistency and vacuity checking that identify all inconsistencies and pinpoint their exact source (the smallest inconsistent set). To complete the sanity checking we also deliver a novel 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

GAP202/11/0312, projekt VaV

Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)

Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification

GD102/09/H042, projekt VaV

Název: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů

Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů

MUNI/A/0914/2009, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)

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

Citovat

BARNAT, Jiří, Petr BAUCH a Luboš BRIM. Checking Sanity of Software Requirements. In George Eleftherakis , Mike Hinchey and Mike Holcombe. Proceedings of the 10th International Conference on Software Engineering and Formal Methods. Thessaloniki: Springer, 2012, s. 48-62. ISBN 978-3-642-33825-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-33826-7_4.

@inproceedings{1066876,
   author = {Barnat, Jiří and Bauch, Petr and Brim, Luboš},
   address = {Thessaloniki},
   booktitle = {Proceedings of the 10th International Conference on Software Engineering and Formal Methods},
   doi = {http://dx.doi.org/10.1007/978-3-642-33826-7_4},
   editor = {George Eleftherakis , Mike Hinchey and Mike Holcombe},
   keywords = {model checking; sanity checking; consistency; vacuity; completeness},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Thessaloniki},
   isbn = {978-3-642-33825-0},
   pages = {48-62},
   publisher = {Springer},
   title = {Checking Sanity of Software Requirements},
   url = {http://dx.doi.org/10.1007/978-3-642-33826-7_4},
   year = {2012}
}

TY  - JOUR
ID  - 1066876
AU  - Barnat, Jiří - Bauch, Petr - Brim, Luboš
PY  - 2012
TI  - Checking Sanity of Software Requirements
PB  - Springer
CY  - Thessaloniki
SN  - 9783642338250
KW  - model checking
KW  - sanity checking
KW  - consistency
KW  - vacuity
KW  - completeness
UR  - http://dx.doi.org/10.1007/978-3-642-33826-7_4
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 techniques that automatically detect flaws and suggest improvements of given requirements. Specifically, we describe and experimentally evaluate new approaches to consistency and vacuity checking that identify all inconsistencies and pinpoint their exact source (the smallest inconsistent set). To complete the sanity checking we also deliver a novel 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 a Luboš BRIM. Checking Sanity of Software Requirements. In George Eleftherakis , Mike Hinchey and Mike Holcombe. \textit{Proceedings of the 10th International Conference on Software Engineering and Formal Methods}. Thessaloniki: Springer, 2012, s.~48-62. ISBN~978-3-642-33825-0. Dostupné z: https://dx.doi.org/10.1007/978-3-642-33826-7\_{}4.

Podrobný výpis o publikaci