Checking Sanity of Software Requirements

D 2012

Checking Sanity of Software Requirements

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

Basic information

Original name

Checking Sanity of Software Requirements

Authors

BARNAT, Jiří (203 Czech Republic, belonging to the institution), Petr BAUCH (203 Czech Republic, guarantor, belonging to the institution) and Luboš BRIM (203 Czech Republic, belonging to the institution)

Edition

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

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Greece

Confidentiality degree

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

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/12:00057623

Organization unit

Faculty of Informatics

ISBN

978-3-642-33825-0

ISSN

DOI

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

Keywords in English

model checking; sanity checking; consistency; vacuity; completeness

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

Links

GAP202/11/0312, research and development project

Name: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)

Investor: Czech Science Foundation

GD102/09/H042, research and development project

Name: 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: Czech Science Foundation

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

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

Investor: Masaryk University, Category A

Citovat

BARNAT, Jiří, Petr BAUCH and 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, p. 48-62. ISBN 978-3-642-33825-0. Available from: 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 and 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, p.~48-62. ISBN~978-3-642-33825-0. Available from: https://dx.doi.org/10.1007/978-3-642-33826-7\_{}4.

Detailed Information on Publication Record