More Web Proxy on the site http://driver.im/

short-paper

Consistency checking in requirements analysis

Author:

Jaroslav BendíkAuthors Info & Claims

ISSTA 2017: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis

Pages 408 - 411

https://doi.org/10.1145/3092703.3098239

Published: 10 July 2017 Publication History

Abstract

In the last decade it became a common practise to formalise software requirements using a mathematical language of temporal logics, e.g., LTL. The formalisation removes ambiguity and improves understanding. Formal description also enables various model-based techniques, like formal verification. Moreover, we get the opportunity to check the requirements earlier, even before any system model is built. This so called requirements sanity checking aims to assure that a given set of requirements is consistent, i.e., that a product satisfying all the requirements can be developed. If inconsistencies are found, it is desirable to present them to the user in a minimal fashion, exposing the core problems among the requirements. Such cores are called minimal inconsistent subsets (MISes). In this work, we present a framework for online MISes enumeration in the domain of temporal logics.

References

[1]

James Bailey and Peter J Stuckey. 2005. Discovery of minimal unsatisfiable subsets of constraints using hitting set dualization. In Practical Aspects of Declarative Languages. Springer, 174–186.

Digital Library

[2]

Jiří Barnat, Petr Bauch, Nikola Beneš, Luboš Brim, Jan Beran, and Tomáš Kratochvíla. 2016. Analysing sanity of requirements for avionics systems. Formal Aspects of Computing (2016). //dx.

Digital Library

[3]

Jiri Barnat, Petr Bauch, and Lubos Brim. 2012. Checking Sanity of Software Requirements. In SEFM (Lecture Notes in Computer Science), Vol. 7504. Springer, 48–62.

Digital Library

[4]

Jiri Barnat, Jan Beran, Lubos Brim, Tomas Kratochvila, and Petr Rockai. 2012. Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. In FMICS (Lecture Notes in Computer Science), Vol. 7437. Springer, 78–92.

[5]

Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlícek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimír Still, and Jirí Weiser. 2013. DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. In CAV (Lecture Notes in Computer Science), Vol. 8044. Springer, 863–868.

[6]

Ilan Beer, Shoham Ben-David, Cindy Eisner, and Yoav Rodeh. 2001. Efficient Detection of Vacuity in Temporal Model Checking. Formal Methods in System Design 18, 2 (2001), 141–163.

Digital Library

[7]

Anton Belov and João Marques-Silva. 2012. MUSer2: An Efficient MUS Extractor. JSAT 8, 3/4 (2012), 123–128.

[8]

Jaroslav Bendík, Nikola Beneš, Jiří Barnat, and Ivana Černá. 2016. Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis. In SEFM (Lecture Notes in Computer Science), Vol. 9763. Springer, 121– 136.

[9]

Jaroslav Bendík, Nikola Benes, Ivana Cerná, and Jiri Barnat. 2016. Tunable Online MUS/MSS Enumeration. In FSTTCS (LIPIcs), Vol. 65. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 50:1–50:13.

[10]

Matteo Bertello, Nicola Gigante, Angelo Montanari, and Mark Reynolds. 2016. Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau. In IJCAI. IJCAI/AAAI Press, 950–956.

Digital Library

[11]

Stefan Blom, Wan Fokkink, Jan Friso Groote, Izak van Langevelde, Bert Lisser, and Jaco van de Pol. 2001.

[12]

µCRL: A Toolset for Analysing Algebraic Specifications. In CAV (Lecture Notes in Computer Science), Vol. 2102. Springer, 250–254.

[13]

Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. 2002.

[14]

NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In CAV (Lecture Notes in Computer Science), Vol. 2404. Springer, 359–364.

[15]

Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2001. Model checking. MIT Press.

[16]

Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. 2016. Spot 2.0 - A Framework for LTL and ω -Automata Manipulation. In ATVA (Lecture Notes in Computer Science), Vol. 9938. 122–129.

[17]

François Hantry and Mohand-Said Hacid. 2011. Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based Languages. In FLACOS (EPTCS), Vol. 68. 39–53.

[18]

Mike Hinchey, Michael Jackson, Patrick Cousot, Byron Cook, Jonathan P. Bowen, and Tiziana Margaria. 2008. Software engineering and formal methods. Commun. ACM 51, 9 (2008), 54–59.

Digital Library

[19]

Jianwen Li, Shufang Zhu, Geguang Pu, and Moshe Y. Vardi. 2015. SAT-Based Explicit LTL Reasoning. In Haifa Verification Conference (Lecture Notes in Computer Science), Vol. 9434. Springer, 209–224.

[20]

Mark H. Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva. 2015. Fast, flexible MUS enumeration. Constraints (2015), 1–28.

Digital Library

[21]

Alexander Nadel, Vadim Ryvchin, and Ofer Strichman. 2014. Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores. JSAT 9 (2014), 27–51.

[22]

Amir Pnueli. 1977. The Temporal Logic of Programs. In FOCS. IEEE Computer Society, 46–57.

Digital Library

[23]

Kristin Y. Rozier and Moshe Y. Vardi. 2011. A Multi-encoding Approach for LTL Symbolic Satisfiability Checking. In FM (Lecture Notes in Computer Science), Vol. 6664. Springer, 417–431.

Digital Library

[24]

Viktor Schuppan. 2012. Towards a notion of unsatisfiable and unrealizable cores for LTL. Sci. Comput. Program. 77, 7-8 (2012), 908–939.

Digital Library

[25]

Viktor Schuppan and Luthfi Darmawan. 2011. Evaluating LTL Satisfiability Solvers. In ATVA (Lecture Notes in Computer Science), Vol. 6996. Springer, 397– 413. Abstract 1 Introduction 2 Related Work 3 Research questions and Contributions 4 Methodology and Evaluation 4.1 Methodology 4.2 Evaluation 5 Research Status 6 Conclusion References

Digital Library

Cited By

Getir Yaman SRibeiro PCavalcanti ACalinescu RPaterson CTownsend B(2025)Specification, validation and verification of social, legal, ethical, empathetic and cultural requirements for autonomous agentsJournal of Systems and Software10.1016/j.jss.2024.112229220(112229)Online publication date: Feb-2025
https://doi.org/10.1016/j.jss.2024.112229
Luo WLiang PQiu JChen PWan HDu JFang WChristakis MPradel M(2024)Learning to Check LTL Satisfiability and to Generate Traces via Differentiable Trace CheckingProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3680337(996-1008)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3680337
Bendík JMeel K(2023)Hashing-based approximate counting of minimal unsatisfiable subsetsFormal Methods in System Design10.1007/s10703-023-00419-w63:1-3(5-39)Online publication date: 19-Apr-2023
https://doi.org/10.1007/s10703-023-00419-w
Show More Cited By

Index Terms

Consistency checking in requirements analysis
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
    2. Software verification and validation
      1. Formal software verification

Recommendations

Model Checking Process with Goal Oriented Requirements Analysis
APSEC '08: Proceedings of the 2008 15th Asia-Pacific Software Engineering Conference

Model checking is a powerful technique for verifying the correctness of a system’s specification. But even when the specification has been verified to be correct, there is still the question of whether the specification covers all the expected ...
Process patterns for requirement consistency analysis
EuroPlop '16: Proceedings of the 21st European Conference on Pattern Languages of Programs

In the requirement space, patterns are gaining prominence to capture the requirement knowledge for reuse and help identify requirements. The quality of requirement specification is critical for effective understanding and implementation of requirements. ...
Quality Requirements Analysis Using Requirements Frames
QSIC '11: Proceedings of the 2011 11th International Conference on Quality Software

Defining quality requirements completely and correctly is more difficult than defining functional requirements because stakeholders do not state most of quality requirements explicitly. We thus propose a method to measure a requirements specification ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA 2017: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis

July 2017

447 pages

ISBN:9781450350761

DOI:10.1145/3092703

General Chair:
Tevfik Bultan
University of California at Santa Barbara, USA
,
Program Chair:
Koushik Sen
University of California at Berkeley, USA

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 July 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Short-paper

Conference

ISSTA '17

Sponsor:

SIGSOFT

ISSTA '17: International Symposium on Software Testing and Analysis

July 10 - 14, 2017

CA, Santa Barbara, USA

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
421
Total Downloads

Downloads (Last 12 months)49
Downloads (Last 6 weeks)1

Reflects downloads up to 20 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Getir Yaman SRibeiro PCavalcanti ACalinescu RPaterson CTownsend B(2025)Specification, validation and verification of social, legal, ethical, empathetic and cultural requirements for autonomous agentsJournal of Systems and Software10.1016/j.jss.2024.112229220(112229)Online publication date: Feb-2025
https://doi.org/10.1016/j.jss.2024.112229
Luo WLiang PQiu JChen PWan HDu JFang WChristakis MPradel M(2024)Learning to Check LTL Satisfiability and to Generate Traces via Differentiable Trace CheckingProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3680337(996-1008)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3680337
Bendík JMeel K(2023)Hashing-based approximate counting of minimal unsatisfiable subsetsFormal Methods in System Design10.1007/s10703-023-00419-w63:1-3(5-39)Online publication date: 19-Apr-2023
https://doi.org/10.1007/s10703-023-00419-w
Iqtidar KAzam FAnwar MAmjad A(2019)Model-Driven approach to Integrate Requirements for Safety-Critical SystemsProceedings of the 7th International Conference on Computer and Communications Management10.1145/3348445.3351305(58-62)Online publication date: 27-Jul-2019
https://dl.acm.org/doi/10.1145/3348445.3351305
Wu ZLiu JChen XZimmermann TLawall JMarinov D(2019)Better development of safety critical systemsProceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2019.00143(1216-1217)Online publication date: 10-Nov-2019
https://dl.acm.org/doi/10.1109/ASE.2019.00143
Narizzano MPulina LTacchella AVuotto S(2019)Property specification patterns at work: verification and inconsistency explanationInnovations in Systems and Software Engineering10.1007/s11334-019-00339-1Online publication date: 3-May-2019
https://doi.org/10.1007/s11334-019-00339-1
Bendík JČerná IBeneš N(2018)Recursive Online Enumeration of All Minimal Unsatisfiable SubsetsAutomated Technology for Verification and Analysis10.1007/978-3-030-01090-4_9(143-159)Online publication date: 30-Sep-2018
https://doi.org/10.1007/978-3-030-01090-4_9

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents