Abstract
Model design is not a linear, one-shot process. It proceeds through refinements and revisions. To effectively support developers in generating model refinements and revisions, it is desirable to have some automated support to verify evolvable models. To address this problem, we recently proposed to adopt topological proofs, which are slices of the original model that witness property satisfaction. We implemented TOrPEDO, a framework that provides automated support for using topological proofs during model design. Our results showed that topological proofs are significantly smaller than the original models, and that, in most of the cases, they allow the property to be re-verified by relying only on a simple syntactic check. However, our results also show that the procedure that computes topological proofs, which requires extracting unsatisfiable cores of LTL formulae, is computationally expensive. For this reason, TOrPEDO currently handles models with a small dimension. With the intent of providing practical and efficient support for flexible model design and wider adoption of our framework, in this paper, we propose an enhanced—re-engineered—version of TOrPEDO. The new version of TOrPEDO relies on a novel procedure to extract topological proofs, which has so far represented the bottleneck of TOrPEDO performances. We implemented our procedure within TOrPEDO by considering Partial Kripke Structures (PKSs) and Linear-time Temporal Logic (LTL): two widely used formalisms to express models with uncertain parts and their properties. To extract topological proofs, the new version of TOrPEDO converts the LTL formulae into an SMT instance and reuses an existing SMT solver (e.g., Microsoft Z3) to compute an unsatisfiable core. Then, the unsatisfiable core returned by the SMT solver is automatically processed to generate the topological proof. We evaluated TOrPEDO by assessing (i) how does the size of the proofs generated by TOrPEDO compares to the size of the models being analyzed; and (ii) how frequently the use of the topological proof returned by TOrPEDO avoids re-executing the model checker. Our results show that TOrPEDO provides proofs that are smaller (\(\approx \) 60%) than their respective initial models effectively supporting designers in creating model revisions. In a significant number of cases (\(\approx \) 79%), the topological proofs returned by TOrPEDO enable assessing the property satisfaction without re-running the model checker. We evaluated our new version of TOrPEDO by assessing (i) how it compares to the previous one; and (ii) how useful it is in supporting the evaluation of alternative design choices of (small) model instances in applied domains. The results show that the new version of TOrPEDO is significantly more efficient than the previous one and can compute topological proofs for models with less than 40 states within two hours. The topological proofs and counterexamples provided by TOrPEDO are useful to support the development of alternative design choices of (small) model instances in applied domains.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
AshburnerM, Ball CA, Blake JA, Botstein D, Butler H, Cherry JM, Davis AP, Dolinski K, Dwight SS, Eppig JT, et al (2000) Gene ontology: tool for the unification of biology. Nat Genet 25(1):25–29
Albarghouthi A, Gurfinkel A, Chechik M (2012) From under-approximations to over-approximations and back. In: International conference on tools and algorithms for the construction and analysis of systems, pp 157–172. Springer
Aluru S (2005) Handbook of computational molecular biology. Chapman & Hall/CRC
Alur R, Moarref S, Topcu U (2013) Counter-strategy guided refinement of GR(1) temporal logic specifications. In: Formal methods in computer-aided design, pp 26–33. IEEE
Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs. In: Design automation conference, pp 317–320. ACM
Brunet G, Chechik M, Easterbrook S, Nejati S, Niu N, SabetzadehM(2006) A manifesto for model merging. In: International workshop on Global integrated model management, pages 5–12. ACM
Bernasconi A, Canakoglu A, MasseroliM, Ceri S (2021) The road towards data integration in human genomics: players, steps and interactions. Brief Bioinform 22(1):30–44
Bruns G, Godefroid P (1999) Model checking partial state spaces with 3-valued temporal logics. In: International conference on computer aided verification, pp 274–287. Springer
Bruns G, Godefroid P (2000) Generalized model checking: reasoning about partial state spaces. In: International conference on concurrency theory, pp 168–182. Springer
Bruns G, Godefroid P (2004) Model checking with multi-valued logics. In: International colloquium on automata, languages and programming, pp 281–293. Springer
Beyer D, Henzinger TA, Jhala R, Majumdar R (2007) The software model checker Blast. Int J Softw Tools Technol Transf 9(5–6):505–525
Baier C, Katoen J-P (2008) Principles of model checking. The MIT Press
Baresi L, Kallehbasti MMP, Rossi M (2015) Efficient scalable verification of LTL specifications. In: International conference on software engineering, pp 711–721. IEEE
Bernasconi A, Menghi C, Spoletini P, Zuck LD, Ghezzi C (2017) From model checking to a temporal proof for partial models. In: International conference on software engineering and formal methods, pp 54–69. Springer
Camilli M, Bellettini C, Gargantini A, Scandurra P (2018) Online model-based testing under uncertainty. In: International symposium on software reliability engineering (ISSRE), pp 36–46. IEEE
Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an opensource tool for symbolic model checking. In: International conference on computer aided verification, pp 359–364. Springer
Chechik M, Devereux B, Easterbrook S, Gurfinkel A (2004) Multi-valued symbolic model-checking. Trans Softw Eng Methodol 12(4):1–38
Camilli M, Gargantini A, Scandurra P (2020) Model-based hypothesis testing of uncertain software systems. Softw Test Verif Reliab 30(2):e1730
Clarke E, Kroening D, Ouaknine J, Strichman O (2004) Completeness and complexity of bounded model checking. In: International conference on verification, model checking, and abstract interpretation, pp 85–96. Springer
Clarke E, Kroening D, Ouaknine J, Strichman O (2005) Computational challenges in bounded model checking. Int J Softw Tools Technol Transf 7(2):174–183
Chechik M, Salay R, Viger T, Kokaly S, Rahimi M (2019) Software assurance in an uncertain world. In: Fundamental approaches to software engineering, pp 3–21
Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: International conference on software engineering, pp 411–420. ACM
Daca P,Henzinger TA, KrennW,NickovicD(2014) Compositional specifications for ioco testing. In: International conference on software testing, verification and validation, pp 373–382. IEEE
De Moura L, Bjørner N (2008) Z3: an efficient smt solver. In: International conference on tools and algorithms for the construction and analysis of systems, pp 337–340. Springer
Deng C, Namjoshi KS (2017) Witnessing network transformations. In: International conference on runtime verification, pp 155–171. Springer
Easterbrook S, Chechik M (2001) A framework for multi-valued reasoning over inconsistent viewpoints. In: International conference on software engineering, pp 411–420. IEEE
Easterbrook SM, Chechik M, Devereux B, Gurfinkel A, Lai Albert YC, Petrovykh V, Tafliovich A, Thompson-Walsh CD (2003) χChek: a model checker for multi-valued reasoning. In: International conference on software engineering, pp 804–805. IEEE
Een N, Mishchenko A, Amla N (2010) A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. In: Conference on formal methods in computer-aided design, pp 181–188. IEEE
Emmert-StreibF,DehmerM, Haibe-KainsB(2014) Gene regulatory networks and their applications: understanding biological and medical problems in terms of networks. Front Cell Dev Biol, 2
ETAPS 2018 Test of time award. https://etaps.org/about/test-of-time-award/test-of-time-award-2018, 07 2020
Fisman D, Kupferman O, Sheinvald-Faragy S, Vardi MY (2008) A framework for inherent vacuity. In: International Haifa verification conference, pp 7–22. Springer
Famelis M, Salay R, Chechik M (2012) Partial models: Towards modeling and reasoning with uncertainty. In: International conference on software engineering, pp 7–22. IEEE
Foster H, Uchitel S, Magee J, Kramer J (2006) LTSA-WS: a tool for model-based verification of web service compositions and choreography. In: International conference on Software engineering, pp 771–774. ACM
Gurfinkel A, Chechik M (2003) Multi-valued model checking via classical model checking. In: International conference on concurrency theory, pp 263–277. Springer
Gurfinkel A, Chechik M (2003) Proof-like counter-examples. In: International conference on tools and algorithms for the construction and analysis of systems, pp 160–175. Springer
Godefroid P, HuthM(2005) Model checking vs. generalized model checking: semantic minimizations for temporal logics. In: Logic in computer science, pp 158–167. IEEE
Godefroid P, HuthM, JagadeesanR(2001) Abstraction-based model checking using modal transition systems. In: International conference on concurrency theory, pp 426–440. Springer
Godefroid P, JagadeesanR(2003) On the expressiveness of 3-valued models. In: International conference on verification, model checking, and abstract interpretation, pp 206–222. Springer
Gong H, Klinger J, Damazyn K, Li X, Huang S (2015) A novel procedure for statistical inference and verification of gene regulatory subnetwork. BMC Bioinform, 16(7):1–10
Godefroid P, Piterman N (2009) LTL generalized model checking revisited. In: Verification, model checking, and abstract interpretation, pp 89–104. Springer
Godefroid P, Piterman N (2011) LTL generalized model checking revisited. Int J Softw Tools Technol Transf 13(6):571–584
Griggio A, Roveri M, Tonetta S (2018) Certifying proofs for LTL model checking. In: Formal methods in computer aided design, pp 1–9. IEEE
Henzinger TA, Jhala R, Majumdar R, Sanvido MAA (2003) Extreme model checking. In: Verification: theory and practice, pp 332–358. Springer
Hong HS, Lee I, Sokolsky O, Ural H (2002) A temporal logic based theory of test coverage and generation. In: International conference on tools and algorithms for the construction and analysis of systems, pp 327–341. Springer
Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P (2009) A bayesian approach to model checking biological systems. In: Computational methods in systems biology, pp 218–234. Springer
Jiang J-M, Hong Z, Chen Y (2019) Modeling and analyzing incremental natures of developing software. Trans Manag Inf Syst 10(2)
Kupferman O, Grumberg O (1996) Branching-time temporal logic and tree automata. Inf Comput 125(1):62–69
Kanehisa M, Goto S (2000) KEGG: kyoto encyclopedia of genes and genomes. Nucleic Acids Res 28(1):27–30
Kroening D, Ouaknine J, Strichman O,Wahl T,Worrell J (2011) Linear completeness thresholds for bounded model checking. In: Computer aided verification, pp 557–572. Springer
Kripke SA (1963) Semantical considerations on modal logic. Acta Philos Fennica 16(1963):83–94
Letier E, Kramer J,Magee J, Uchitel S (2008) Deriving event-based transition systems fromgoal-oriented requirements models. Autom Softw Eng, pp 175–206
Larsen KG, Thomsen B (1988) A modal process logic. In: Logic in computer science, pp 203–210. IEEE
Liang X-J, Xia Z, Zhang L-W, Wu F-X (2012) Inference of gene regulatory subnetworks from time course gene expression data. In: BMC bioinformatics, volume 13, page S3. Springer
MaY,DamazynK, Klinger J,GongH(2015) Inference and verification of probabilistic graphical models fromhigh-dimensional data. In: International conference on data integration in the life sciences, pp 223–239. Springer
Menghi C, Garcia S, Pelliccione P, Tumova J (2018) Multi-robot LTL planning under uncertainty. In: Formal methods, pp 399–417. Springer
Menghi C, Rizzi AM, Bernasconi A (2020) Integrating topological proofs with model checking to instrument iterative design. In: Fundamental approaches to software engineering, pp 53–74. Springer
Maoz S, Shalom R (2020) Inherent vacuity for GR(1) specifications. In: European software engineering conference and symposium on the foundations of software engineering, pp 99–110. ACM
Menghi C, Spoletini P, Chechik M, Ghezzi C (2018) Supporting verification-driven incremental distributed design of components. In: Fundamental approaches to software engineering, pp 169–188. Springer
Menghi C, Spoletini P, Chechik M, Ghezzi C (2019) A verification-driven framework for iterative design of controllers. Formal Aspects Comput 31(5):459–502
Menghi C, Spoletini P, Ghezzi C (2016) Dealing with incompleteness in automata-based model checking. In: Formal Methods, pp 531–550. Springer
Menghi C, Spoletini P, Ghezzi C (2017) Integrating goal model analysis with iterative design. In: International working conference on requirements engineering: foundation for software quality, pp 112–128. Springer
Namjoshi KS (2001) Certifying model checkers. In: Computer aided verification, pp 2–13. Springer
Pourhashem KMM, RossiMG, Baresi L (2020) On how bit-vector logic can help verify LTL-based specifications. IEEE Trans Softw Eng, pp 1–1
Pnueli A (1977) The temporal logic of programs. In: Annual symposium on foundations of computer science, pp 46–57. IEEE
Peled D, Pnueli A, Zuck L (2001) From falsification to verification. In: Foundations of software technology and theoretical computer science, pp 292–304
Pill I, Quaritsch T (2013) Behavioral diagnosis of LTL specifications at operator level. In: International joint conference on artificial intelligence, pp 1053–1059. IJCAI/AAAI
Pencolé Y, Steinbauer G, Mühlbacher C, Travé-Massuyès L (2017) Diagnosing discrete event systems using nominal models only. In: International workshop on principles of diagnosis, pp 169–183. EasyChair
Peled D, Zuck L (2001) From model checking to a temporal proof. In: International SPIN workshop on model checking of software, pp 1–14. Springer
Raman V, Lignos C, Finucane C, Lee KCT, Marcus MP, Kress-Gazit H (2013) Sorry Dave, I’m Afraid I Can’t Do That: explaining unachievable robot tasks using natural language. In: Robotics: science and systems, vol 2, pp 2–1. Citeseer
Simmonds J, Davies J, Gurfinkel A, Chechik M (2010) Exploiting resolution proofs to speed up LTL vacuity detection for BMC. Int J Softw Tools Technol Transf 12(5):319–335
Shoham S, Grumberg O (2003) A game-based framework for ctl counterexamples and 3-valued abstraction-refinement. In: International conference on computer aided verification, pp 275–287. Springer
Sergeant T, Goré SR, Thomson J (2013) Finding minimal unsatisfiable subsets in linear temporal logic using BDDs, https://cs.anu.edu.au/courses/csprojects/13S1/Reports/Timothy_Sergeant_Report.pdf.
Saïs L, Hacid M-S, Hantry F (2012) On the complexity of computing minimal unsatisfiable LTL formulas. Electronic Colloquium on Computational Complexity (ECCC), 19:69, Hasso Plattner Institute
SIGPLAN ACM - Programming Languages Software Award. http://www.sigplan.org/Awards/Software/, 07 2020
Schuppan V, Latvala T, Junttila T, Heljanko K, Biere A (2006) Linear encodings of bounded LTL model checking. Log Methods Comput Sci, 2, Episciences.org
Stamoulakatou E, Piccardi C, Masseroli M (2019) Analysis of gene regulatory networks inferred from chip-seq data. In: International work-conference on bioinformatics and biomedical engineering, pp 319–331. Springer
Tan L, Cleaveland R (2002) Evidence-based model checking. In: International conference on computer aided verification, pp 455–470. Springer
Timm N, Gruner S (2019) Abstraction refinement with path constraints for 3-valued bounded model checking. In: Formal techniques for safety-critical systems, pp 139–157. Springer
Timm N, Gruner S, Nxumalo M, Botha J (2020) Model checking safety and liveness via k-induction and witness refinement with constraint generation. Science of Computer Programming, 200:102532, Elsevier
Tao X, Li G (2017) The complexity of linear-time temporal logic model repair. In: International workshop on structured object-oriented formal language and method, pp 69–87. Springer
Torpedo. http://github.com/alessandrorizzi/torpedo, 2020
Tretmans J (1999) Testing concurrent systems: a formal approach. In: International conference on concurrency theory, pp 46–65. Springer
Uchitel S, AlrajehD, Ben-David S, BrabermanV, Chechik M, De CasoG, D’IppolitoN, FischbeinD, GarbervetskyD,Kramer J et al (2013). Supporting incremental behaviour model elaboration. Comput Sci-Res Dev 28(4):279–293
Uchitel S, Brunet G, ChechikM(2009) Synthesis of partial behavior models from properties and scenarios. IEEE Trans Softw Eng, 35(3):384–406
Uchitel S (2009) Partial behaviour modelling: foundations for incremental and iterative model-based software engineering. In: Formal methods: foundations and applications. Springer
van der Bijl M, Rensink A, Tretmans J (2004) Compositional testing with ioco. In: Formal approaches to software testing, pp 86–100. Springer
Yu J, Smith VA, Wang PP, Hartemink AJ, Jarvis ED (2004) Advances to bayesian network inference for generating causal networks from observational biological data. Bioinformatics, oxford university press, 20(18):3594–3603
Acknowledgements
This work has received funding from the European Research Council under the European Union's Horizon 2020 research and innovation programme (grant No 694277). We thank the anonymous reviewers for the useful comments.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Jordi Cabot, Heike Wehrheim and Eerke Boiten
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Menghi, C., Rizzi, A.M., Bernasconi, A. et al. TOrPEDO: witnessing model correctness with topological proofs. Form Asp Comp 33, 1039–1066 (2021). https://doi.org/10.1007/s00165-021-00564-1
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-021-00564-1