research-article

Open access

Minimal strongly unsatisfiable subsets of reactive system specifications

Authors:

Shigeki Hagihara,

Naoki Egawa,

Masaya Shimakawa,

Naoki YonezakiAuthors Info & Claims

ASE '14: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering

Pages 629 - 634

https://doi.org/10.1145/2642937.2642968

Published: 15 September 2014 Publication History

PDF eReader

Abstract

Verifying realizability in the specification phase is expected to reduce the development costs of safety-critical reactive systems. If a specification is not realizable, we must correct the specification. However, it is not always obvious what part of a specification should be modified. In this paper, we propose a method for obtaining the location of flaws. Rather than realizability, we use strong satisfiability, due to the fact that many practical unrealizable specifications are also strongly unsatisfiable. Using strong satisfiability, the process of analyzing realizability becomes less complex. We define minimal strongly unsatisfiable subsets (MSUSs) to locate flaws, and construct a procedure to compute them. We also show correctness properties of our method, and clarify the time complexity of our method. Furthermore, we implement the procedure, and confirm that MSUSs are computable for specifications of reactive systems at non-trivial scales.

References

[1]

M. Abadi, L. Lamport, and P. Wolper. Realizable and unrealizable specifications of reactive systems. In ICALP89, vol. 372 of LNCS, pages 1--17. 1989.

Digital Library

Google Scholar

[2]

T. Aoshima and N. Yonezaki. Verification of reactive system specification with outer event conditional formula. In International Symposium on Principles of Software Evolution (ISPSE2000), pages 195--199, 2000.

Crossref

Google Scholar

[3]

T. Babiak, M. Kretínskÿ, V. Rehák, and J. Strejcek. LTL to Büchi automata translation: Fast and more deterministic. In TACAS2012, vol. 7214 of LNCS, pages 95--109, 2012.

Digital Library

Google Scholar

[4]

A. Cimatti, M. Roveri, V. Schuppan, and A. Tchaltsev. Diagnostic information for realizability. In VMCAI2008, vol. 4905 of LNCS, pages 52--67. 2008.

Digital Library

Google Scholar

[5]

S. Hagihara, Y. Kitamura, M. Shimakawa, and N. Yonezaki. Extracting environmental constraints to make reactive system specifications realizable. In 16th Asia-Pacific Software Engineering Conference, APSEC '09, pages 61--68, 2009.

Digital Library

Google Scholar

[6]

S. Hagihara and N. Yonezaki. Completeness of verification methods for approaching to realizable reactive specifications. In AWCVS'06, vol. 348 of UNU-IIST Technical Report, pages 242--257, 2006.

Google Scholar

[7]

R. Konighofer, G. Hofferek, and R. Bloem. Debugging formal specifications using simple counterstrategies. In FMCAD2009, pages 152--159, 2009.

Crossref

Google Scholar

[8]

W. Li, L. Dworkin, and S. A. Seshia. Mining assumptions for synthesis. In MEMOCODE, pages 43--50, 2011.

Digital Library

Google Scholar

[9]

M. H. Liffiton and K. A. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 40(1):1--33, 2008.

Digital Library

Google Scholar

[10]

R. Mori and N. Yonezaki. Several realizability concepts in reactive objects. In Information Modeling and Knowledge Bases, 1993.

Google Scholar

[11]

A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL89, pages 179--190, 1989.

Digital Library

Google Scholar

[12]

R. Rosner. Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science, 1992.

Google Scholar

[13]

M. Shimakawa, S. Hagihara, and N. Yonezaki. Complexity of strong satisfiability problems for reactive system specifications. IEICE Transactions on Information and Systems, E96-D(10):2187--2193, 2013.

Google Scholar

[14]

Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, and W.-C. Chan. GOAL: A graphical tool for manipulating Büchi automata and temporal formulae. In TACAS2007, vol. 4424 of LNCS, pages 466--471. 2007.

Digital Library

Google Scholar

Cited By

View all

TOMITA THAGIHARA SSHIMAKAWA MYONEZAKI N(2022)A Characterization on Necessary Conditions of Realizability for Reactive System SpecificationsIEICE Transactions on Information and Systems10.1587/transinf.2021FOP0005E105.D:10(1665-1677)Online publication date: 1-Oct-2022
https://doi.org/10.1587/transinf.2021FOP0005
Shimakawa MHayashi KHagihara SYonezaki N(2020)Towards Interpretation of Abstract Instructions Using Declarative Constraints in Temporal LogicProceedings of the 2020 9th International Conference on Software and Computer Applications10.1145/3384544.3384572(17-20)Online publication date: 18-Feb-2020
https://dl.acm.org/doi/10.1145/3384544.3384572
Gaber LHussein AMahmoud HMabrook MMoness M(2020)Computation of minimal unsatisfiable subformulas for SAT-based digital circuit error diagnosisJournal of Ambient Intelligence and Humanized Computing10.1007/s12652-020-02247-w13:7(3693-3711)Online publication date: 29-Jun-2020
https://doi.org/10.1007/s12652-020-02247-w
Show More Cited By

Index Terms

Minimal strongly unsatisfiable subsets of reactive system specifications
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program specifications

Recommendations

Formalized structured analysis specifications
Hashing-based approximate counting of minimal unsatisfiable subsets
Abstract
In many areas of computer science, we are given an unsatisfiable Boolean formula F in CNF, i.e. a set of clauses, with the goal to analyse the unsatisfiability. Examination of minimal unsatisfiable subsets (MUSes) of F is a kind of such analysis. ...
A power-set construction for reducing Büchi automata to non-determinism degree two

Buchi automata are finite automata that accept languages of infinitely long strings, so-called @w-languages. It is well known that, unlike in the finite-string case, deterministic and non-deterministic Buchi automata accept different @w-language classes,...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ASE '14: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering

September 2014

934 pages

ISBN:9781450330138

DOI:10.1145/2642937

General Chair:
Ivica Crnkovic
Mälardalen University, Sweden
,
Program Chairs:
Marsha Chechik
University of Toronto, Canada
,
Paul Grünbacher
Johannes Kepler Universität Linz, Austria

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 September 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Japan Society for the Promotion of Science

Conference

ASE '14

Sponsor:

SIGAI
SIGSOFT
Mälardalen University

ASE '14: ACM/IEEE International Conference on Automated Software Engineering

September 15 - 19, 2014

Vasteras, Sweden

Acceptance Rates

ASE '14 Paper Acceptance Rate 82 of 337 submissions, 24%;

Overall Acceptance Rate 82 of 337 submissions, 24%

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
407
Total Downloads

Downloads (Last 12 months)50
Downloads (Last 6 weeks)7

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

TOMITA THAGIHARA SSHIMAKAWA MYONEZAKI N(2022)A Characterization on Necessary Conditions of Realizability for Reactive System SpecificationsIEICE Transactions on Information and Systems10.1587/transinf.2021FOP0005E105.D:10(1665-1677)Online publication date: 1-Oct-2022
https://doi.org/10.1587/transinf.2021FOP0005
Shimakawa MHayashi KHagihara SYonezaki N(2020)Towards Interpretation of Abstract Instructions Using Declarative Constraints in Temporal LogicProceedings of the 2020 9th International Conference on Software and Computer Applications10.1145/3384544.3384572(17-20)Online publication date: 18-Feb-2020
https://dl.acm.org/doi/10.1145/3384544.3384572
Gaber LHussein AMahmoud HMabrook MMoness M(2020)Computation of minimal unsatisfiable subformulas for SAT-based digital circuit error diagnosisJournal of Ambient Intelligence and Humanized Computing10.1007/s12652-020-02247-w13:7(3693-3711)Online publication date: 29-Jun-2020
https://doi.org/10.1007/s12652-020-02247-w
Shimakawa MUeno AMochizuki STomita THagihara SYonezaki N(2019)Towards Efficient Implementation of Realizability Checking for Reactive System SpecificationsProceedings of the 2019 8th International Conference on Software and Computer Applications10.1145/3316615.3316634(347-352)Online publication date: 19-Feb-2019
https://dl.acm.org/doi/10.1145/3316615.3316634
Shimakawa MHagihara SYonezaki N(2018)Efficiency of the strong satisfiability checking procedure for reactive system specifications10.1063/1.5033715(040051)Online publication date: 2018
https://doi.org/10.1063/1.5033715
Shimakawa MOsari KHagihara SYonezaki NMezhuyev VBenedicenti L(2017)Modularization of formal specifications or efficient synthesis of reactive systemsProceedings of the 6th International Conference on Software and Computer Applications10.1145/3056662.3056702(208-213)Online publication date: 26-Feb-2017
https://dl.acm.org/doi/10.1145/3056662.3056702
Hagihara SFushihara YShimakawa MTomoishi MYonezaki NMezhuyev VBenedicenti L(2017)Web server access trend analysis based on the Poisson distributionProceedings of the 6th International Conference on Software and Computer Applications10.1145/3056662.3056701(256-261)Online publication date: 26-Feb-2017
https://dl.acm.org/doi/10.1145/3056662.3056701
Tomita TUeno AShimakawa MHagihara SYonezaki N(2017)Safraless LTL synthesis considering maximal realizabilityActa Informatica10.1007/s00236-016-0280-354:7(655-692)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.1007/s00236-016-0280-3
Hagihara SUeno ATomita TShimakawa MYonezaki N(2016)Simple synthesis of reactive systems with tolerance for unexpected environmental behaviorProceedings of the 4th FME Workshop on Formal Methods in Software Engineering10.1145/2897667.2897672(15-21)Online publication date: 14-May-2016
https://dl.acm.org/doi/10.1145/2897667.2897672

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Cited By

Index Terms

Recommendations

Formalized structured analysis specifications

Hashing-based approximate counting of minimal unsatisfiable subsets

A power-set construction for reducing Büchi automata to non-determinism degree two