Topological Proofs; Iterative Design; Model Checking; Theorem Proving; Unsatisfiable Core
Abstract :
[en] System development is not a linear, one-shot process. It proceeds through refinements and revisions. To support assurance that the system satisfies its requirements, it is desirable that continuous verification can be performed after each refinement or revision step. To achieve practical adoption, formal verification must accommodate continuous verification efficiently and effectively. Model checking provides developers with information useful to improve their models only when a property is not satisfied, i.e., when a counterexample is returned. However, it is desirable to have some useful information also when a property is instead satisfied. To address this problem we propose TOrPEDO, an approach that supports verification in two complementary forms: model checking and proofs. While model checking is typically used to pinpoint model behaviors that violate requirements, proofs can instead explain why requirements are satisfied. In our work, we introduce a specific notion of proof, called Topological Proof. A topological proof produces a slice of the original model that justifies the property satisfaction. Because models can be incomplete, TOrPEDO supports reasoning on requirements satisfaction, violation, and possible satisfaction (in the case where satisfaction depends on unknown parts of the model). Evaluation is performed by checking how topological proofs support software development on 12 modeling scenarios and 15 different properties obtained from 3 examples from literature. Results show that: (i) topological proofs are ≈60% smaller than the original models; (ii) after a revision, in ≈78% of cases, the property can be re-verified by relying on a simple syntactic check.
Disciplines :
Computer science
Author, co-author :
Menghi, Claudio ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Rizzi, Alessandro Maria; Politecnico di Milano
Bernasconi, Anna; Politecnico di Milano
External co-authors :
yes
Language :
English
Title :
Integrating Topological Proofs with Model Checking to Instrument Iterative Design
Publication date :
April 2020
Event name :
Fundamental Approaches to Software Engineering
Event date :
from 25-04-2019 to 30-04-2019
Main work title :
Proceedings of the 23rd International Conference on Fundamental Approaches to Software Engineering, FASE 2020
Pages :
53-74
Peer reviewed :
Peer reviewed
Focus Area :
Security, Reliability and Trust
European Projects :
H2020 - 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems
A. Albarghouthi, A. Gurfinkel, and M. Chechik. From under-approximations to over-approximations and back. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2012.
R. Alur, S. Moarref, and U. Topcu. Counter-strategy guided refinement of GR(1) temporal logic specifications. In Formal Methods in Computer-Aided Design, pages 26–33, Oct 2013.
C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.
A. Bernasconi, C. Menghi, P. Spoletini, L. D. Zuck, and C. Ghezzi. From model checking to a temporal proof for partial models. In International Conference on Software Engineering and Formal Methods. Springer, 2017.
A. Bernasconi, C. Menghi, P. Spoletini, L. D. Zuck, and C. Ghezzi. From model checking to a temporal proof for partial models: preliminary example. arXiv preprint arXiv:1706.02701, 2017.
D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker blast. International Journal on Software Tools for Technology Transfer, 9(5-6):505–525, 2007.
A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using sat procedures instead of bdds. In Design Automation Conference. ACM, 1999.
G. Brunet, M. Chechik, S. Easterbrook, S. Nejati, N. Niu, and M. Sabetzadeh. A manifesto for model merging. In International workshop on Global integrated model management. ACM, 2006.
G. Bruns and P. Godefroid. Model checking partial state spaces with 3-valued temporal logics. In International Conference on Computer Aided Verification. Springer, 1999.
G. Bruns and P. Godefroid. Generalized model checking: Reasoning about partial state spaces. In International Conference on Concurrency Theory. Springer, 2000.
G. Bruns and P. Godefroid. Model checking with multi-valued logics. In International Colloquium on Automata, Languages and Programming. Springer, 2004.
M. Chechik, B. Devereux, S. Easterbrook, and A. Gurfinkel. Multi-valued symbolic model-checking. Transactions on Software Engineering and Methodology, 12(4):1– 38, 2004.
M. Chechik, R. Salay, T. Viger, S. Kokaly, and M. Rahimi. Software assurance in an uncertain world. In R. Hähnle and W. van der Aalst, editors, Fundamental Approaches to Software Engineering, pages 3–21, Cham, 2019. Springer.
A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In International Conference on Computer Aided Verification. Springer, 2002.
P. Daca, T. A. Henzinger, W. Krenn, and D. Nickovic. Compositional specifications for ioco testing. In International Conference on Software Testing, Verification and Validation, pages 373–382. IEEE, 2014.
C. Deng and K. S. Namjoshi. Witnessing network transformations. In International Conference on Runtime Verification. Springer, 2017.
N. Dershowitz, Z. Hanna, and A. Nadel. A scalable algorithm for minimal unsatisfiable core extraction. In International Conference on Theory and Applications of Satisfiability Testing, pages 36–41. Springer, 2006.
M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In International Conference on Software engineering. ACM, 1999.
S. Easterbrook and M. Chechik. A framework for multi-valued reasoning over inconsistent viewpoints. In International conference on software engineering. IEEE, 2001.
S. Easterbrook, M. Chechik, B. Devereux, A. Gurfinkel, A. Lai, V. Petrovykh, A. Tafliovich, and C. Thompson-Walsh. χChek: A model checker for multi-valued reasoning. In International Conference on Software Engineering, pages 804–805, 2003.
N. Een, A. Mishchenko, and N. Amla. A single-instance incremental SAT formulation of proof-and counterexample-based abstraction. In Conference on Formal Methods in Computer-Aided Design, FMCAD, pages 181–188. FMCAD Inc, 2010.
M. Famelis, R. Salay, and M. Chechik. Partial models: Towards modeling and reasoning with uncertainty. In International Conference on Software Engineering. IEEE, 2012.
H. Foster, S. Uchitel, J. Magee, and J. Kramer. Ltsa-ws: a tool for model-based verification of web service compositions and choreography. In International conference on Software engineering. ACM, 2006.
P. Godefroid and M. Huth. Model checking vs. generalized model checking: Semantic minimizations for temporal logics. In Logic in Computer Science. IEEE, 2005.
P. Godefroid, M. Huth, and R. Jagadeesan. Abstraction-based model checking using modal transition systems. In International Conference on Concurrency Theory. Springer, 2001.
P. Godefroid and R. Jagadeesan. On the expressiveness of 3-valued models. In International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 2003.
P. Godefroid and N. Piterman. LTL generalized model checking revisited. In Verification, Model Checking, and Abstract Interpretation, pages 89–104. Springer, 2009.
P. Godefroid and N. Piterman. LTL generalized model checking revisited. International journal on software tools for technology transfer, 13(6):571–584, 2011.
A. Griggio, M. Roveri, and S. Tonetta. Certifying proofs for LTL model checking. In Formal Methods in Computer Aided Design (FMCAD), pages 1–9. IEEE, 2018.
A. Gurfinkel and M. Chechik. Multi-valued model checking via classical model checking. In International Conference on Concurrency Theory. Springer, 2003.
A. Gurfinkel and M. Chechik. Proof-like counter-examples. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 160–175. Springer, 2003.
O. Guthmann, O. Strichman, and A. Trostanetski. Minimal unsatisfiable core extraction for SMT. In Formal Methods in Computer-Aided Design (FMCAD), pages 57–64. IEEE, 2016.
T. A. Henzinger, R. Jhala, R. Majumdar, and M. A. Sanvido. Extreme model checking. In Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. Springer, 2003.
H. S. Hong, I. Lee, O. Sokolsky, and H. Ural. A temporal logic based theory of test coverage and generation. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2002.
S. A. Kripke. Semantical considerations on modal logic. Acta Philosophica Fennica, 16(1963):83–94, 1963.
O. Kupferman and M. Y. Vardi. From complementation to certification. Theoretical computer science, 345(1):83–100, 2005.
K. G. Larsen and B. Thomsen. A modal process logic. In Logic in Computer Science. IEEE, 1988.
E. Letier, J. Kramer, J. Magee, and S. Uchitel. Deriving event-based transition systems from goal-oriented requirements models. Automated Software Engineering, 2008.
M. H. Liffiton and K. A. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 40(1):1–33, 2008.
C. Menghi, S. Garcia, P. Pelliccione, and J. Tumova. Multi-robot LTL planning under uncertainty. In Formal Methods. Springer, 2018.
C. Menghi, S. García, P. Pelliccione, and J. Tumova. Towards multi-robot applications planning under uncertainty. In International Conference on Software Engineering: Companion Proceeedings. ACM, 2018.
C. Menghi, P. Spoletini, M. Chechik, and C. Ghezzi. Supporting verificationdriven incremental distributed design of components. In Fundamental Approaches to Software Engineering. Springer, 2018.
C. Menghi, P. Spoletini, M. Chechik, and C. Ghezzi. A verification-driven framework for iterative design of controllers. Formal Aspects of Computing, Jun 2019.
C. Menghi, P. Spoletini, and C. Ghezzi. Dealing with incompleteness in automatabased model checking. In Formal Methods. Springer, 2016.
C. Menghi, P. Spoletini, and C. Ghezzi. COVER: Change-based Goal Verifier and Reasoner. In International Conference on Requirements Engineering: Foundation for Software Quality: Companion Proceeedings. Springer, 2017.
C. Menghi, P. Spoletini, and C. Ghezzi. Integrating goal model analysis with iterative design. In International Working Conference on Requirements Engineering: Foundation for Software Quality. Springer, 2017.
A. Nadel. Boosting minimal unsatisfiable core extraction. In Conference on Formal Methods in Computer-Aided Design, pages 221–229. FMCAD Inc, 2010.
K. S. Namjoshi. Certifying model checkers. In Computer Aided Verification. Springer, 2001.
D. Peled, A. Pnueli, and L. Zuck. From falsification to verification. In Foundations of Software Technology and Theoretical Computer Science. Springer, 2001.
D. Peled and L. Zuck. From model checking to a temporal proof. In International SPIN Workshop on Model Checking of Software. Springer, 2001.
Y. Pencolé, G. Steinbauer, C. Mühlbacher, and L. Travé-Massuyès. Diagnosing discrete event systems using nominal models only. In DX, pages 169–183, 2017.
I. Pill and T. Quaritsch. Behavioral diagnosis of LTL specifications at operator level. In Twenty-Third International Joint Conference on Artificial Intelligence, 2013.
S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated proof checking. In Computer Aided Verification. Springer, 1995.
V. Raman, C. Lignos, C. Finucane, K. C. Lee, M. P. Marcus, and H. Kress-Gazit. Sorry Dave, I’m Afraid I Can’t Do That: Explaining Unachievable Robot Tasks Using Natural Language. In Robotics: Science and Systems, volume 2, pages 2–1, 2013.
L. Saïs, M. Hacid, and F. Hantry. On the complexity of computing minimal unsatisfiable LTL formulas. Electronic Colloquium on Computational Complexity (ECCC), 19:69, 2012.
V. Schuppan. Enhancing unsatisfiable cores for LTL with information on temporal relevance. Theoretical Computer Science, 655(Part B):155 – 192, 2016. Quantitative Aspects of Programming Languages and Systems (2013-14).
V. Schuppan. Enhanced unsatisfiable cores for QBF: Weakening universal to existential quantifiers. In International Conference on Tools with Artificial Intelligence (ICTAI), pages 81–89. IEEE, 2018.
T. Sergeant, S. R. Goré, and J. Thomson. Finding minimal unsatisfiable subsets in linear temporal logic using BDDs, 2013.
S. Shoham and O. Grumberg. A game-based framework for ctl counterexamples and 3-valued abstraction-refinement. In International Conference on Computer Aided Verification, pages 275–287. Springer, 2003.
L. Tan and R. Cleaveland. Evidence-based model checking. In International Conference on Computer Aided Verification, pages 455–470. Springer, 2002.
X. Tao and G. Li. The complexity of linear-time temporal logic model repair. In International Workshop on Structured Object-Oriented Formal Language and Method, pages 69–87. Springer, 2017.
J. Tretmans. Testing concurrent systems: A formal approach. In International Conference on Concurrency Theory, pages 46–65. Springer, 1999.
S. Uchitel. Partial behaviour modelling: Foundations for incremental and iterative model-based software engineering. In M. V. M. Oliveira and J. Woodcock, editors, Formal Methods: Foundations and Applications. Springer, 2009.
S. Uchitel, D. Alrajeh, S. Ben-David, V. Braberman, M. Chechik, G. De Caso, N. D’Ippolito, D. Fischbein, D. Garbervetsky, J. Kramer, et al. Supporting incremental behaviour model elaboration. Computer Science-Research and Development, 28(4):279–293, 2013.
S. Uchitel, G. Brunet, and M. Chechik. Synthesis of partial behavior models from properties and scenarios. Transactions on Software Engineering, 35(3):384–406, 2009.
M. van der Bijl, A. Rensink, and J. Tretmans. Compositional testing with ioco. In Formal Approaches to Software Testing, pages 86–100. Springer, 2004.
