Checking Sanity of Software Requirements

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BARNAT Jiří BAUCH Petr BRIM Luboš

Year of publication 2012
Type Article in Proceedings
Conference Proceedings of the 10th International Conference on Software Engineering and Formal Methods
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.1007/978-3-642-33826-7_4
Doi http://dx.doi.org/10.1007/978-3-642-33826-7_4
Field Informatics
Keywords model checking; sanity checking; consistency; vacuity; completeness
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.