Identifikační kód | RIV/00216224:14330/12:00057623 |
Název v anglickém jazyce | Checking Sanity of Software Requirements |
Druh | D - Článek ve sborníku |
Jazyk | eng - angličtina |
Obor - skupina | I - Informatika |
Obor | IN - Informatika |
Rok uplatnění | 2012 |
Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
Počet výskytů výsledku | 2 |
Počet tvůrců celkem | 3 |
Počet domácích tvůrců | 3 |
Výčet všech uvedených jednotlivých tvůrců | Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792) Petr Bauch (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5736935) Luboš Brim (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6500773) |
Popis výsledku v anglickém jazyce | 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. Theusefulness of our completeness evaluation is demonstrated in a case study of an aeroplane control system. |
Klíčová slova oddělená středníkem | model checking; sanity checking; consistency; vacuity; completeness |
Stránka www, na které se nachází výsledek | - |
DOI výsledku | 10.1007/978-3-642-33826-7_4 |