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.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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"
WWW 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 0302-9743
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ěnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 23. 4. 2013 13:25.
Anotace
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 VaVNá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 VaVNá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 MUNá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
VytisknoutZobrazeno: 26. 4. 2024 11:17