[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Property specification patterns at work: verification and inconsistency explanation

  • S.I. : NFM2018
  • Published:
Innovations in Systems and Software Engineering Aims and scope Submit manuscript

Abstract

Property specification patterns (PSPs) have been proposed to ease the formalization of requirements, yet enable automated verification thereof. In particular, the internal consistency of specifications written with PSPs can be checked automatically with the use of, for example, linear temporal logic (LTL) satisfiability solvers. However, for most practical applications, the expressiveness of PSPs is too restricted to enable writing useful requirement specifications, and proving that a set of requirements is inconsistent can be worthless unless a minimal set of conflicting requirements is extracted to help designers to correct a wrong specification. In this paper, we extend PSPs by considering Boolean as well as atomic numerical assertions, we contribute an encoding from extended PSPs to LTL formulas, and we present an algorithm computing inconsistency explanations, i.e., irreducible inconsistent subsets of the original set of requirements. Our extension enables us to reason about the internal consistency of functional requirements which would not be captured by basic PSPs. Experimental results demonstrate that our approach can check and explain (in)consistencies in specifications with nearly two thousand requirements generated using a probabilistic model, and that it enables effective handling of real-world case studies.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. Cross-layer modEl-based fRamework for multi-oBjective dEsign of Reconfigurable systems in unceRtain hybRid envirOnments—http://www.cerbero-h2020.eu/.

  2. https://gitlab.sagelab.it/sage/SpecPro.

  3. https://ti.arc.nasa.gov/m/profile/kyrozier/PANDA/PANDA.html.

  4. We omitted aspects which are not relevant for our work, e.g., translations to other logics like CTL [18]. The full list of PSPs considered in this paper and their mapping to LTL and other logics is available at http://patterns.projects.cis.ksu.edu/.

  5. Strictly speaking, the syntax used is not that of \({\mathcal {D}}_C\), but a statement like \(v \le 5.0\) can be thought as syntactic sugar for the expression \((v < 5.0) \vee (v = 5.0)\).

  6. http://www.trossenrobotics.com/widowxrobotarm.

  7. http://www.coppeliarobotics.com/.

  8. The full list of requirements and the fault injection examples are available at https://github.com/SAGE-Lab/robot-arm-usecase.

  9. Experiments herein presented ran on a PC equipped with a CPU Intel Core i7-2760QM @ 2.40 GHz (8 cores) and 8 GB of RAM, running Ubuntu 14.04 LTS.

References

  1. Awad A, Goré R, Thomson J, Weidlich M (2011) An iterative approach for business process template synthesis from compliance rules. In: International conference on advanced information systems engineering, Springer, pp 406–421

  2. Bakker RR, Dikker F, Tempelman F, Wognum PM (1993) Diagnosing and solving over-determined constraint satisfaction problems. IJCAI 93:276–281

    Google Scholar 

  3. Barnat J, Bauch P, Beneš N, Brim L, Beran J, Kratochvíla T (2016) Analysing sanity of requirements for avionics systems. Form Asp Comput 28(1):45–63

    Article  MathSciNet  MATH  Google Scholar 

  4. Belov A, Marques-Silva J (2011) Accelerating MUS extraction with recursive model rotation. In: Formal methods in computer-aided design (FMCAD), 2011. pp 37–40. IEEE

  5. Belov A, Marques-Silva J (2012) Muser2: an efficient mus extractor. J Satisf Boolean Model Comput 8:123–128

    MATH  Google Scholar 

  6. Bendík J (2017) Consistency checking in requirements analysis. In: Proceedings of the 26th ACM SIGSOFT international symposium on software testing and analysis, pp 408–411. ACM

  7. Bertello M, Gigante N, Montanari A (2016) Reynolds M Leviathan: A new ltl satisfiability checking tool based on a one-pass tree-shaped tableau. In: Proceedings of the twenty-fifth international joint conference on artificial intelligence, AAAI Press, pp 950–956. IJCAI’16, http://dl.acm.org/citation.cfm?id=3060621.3060753

  8. Chinneck JW, Dravnieks EW (1991) Locating minimal infeasible constraint sets in linear programs. ORSA J Comput 3(2):157–168

    Article  MATH  Google Scholar 

  9. 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: 14th international conference on computer aided verification (CAV 2002), pp 359–364

  10. Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Progr Lang Syst (TOPLAS) 8(2):244–263

    Article  MATH  Google Scholar 

  11. Comon H, Cortier V (2000) Flatness is not a weakness. In: International workshop on computer science logic, pp 262–276

  12. Demri S, DSouza D (2007) An automata-theoretic approach to constraint LTL. Inf Comput 205(3):380–415

    Article  MathSciNet  MATH  Google Scholar 

  13. Desrosiers C, Galinier P, Hertz A, Paroz S (2009) Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems. J Comb Optim 18(2):124–150

    Article  MathSciNet  MATH  Google Scholar 

  14. Dillon LK, Kutty G, Moser LE, Melliar-Smith PM, Ramakrishna YS (1994) A graphical interval logic for specifying concurrent systems. ACM Trans Softw Eng Methodol (TOSEM) 3(2):131–165

    Article  MATH  Google Scholar 

  15. Dokhanchi A, Hoxha B, Fainekos G (2015) Metric interval temporal logic specification elicitation and debugging. In: 13th ACM-IEEE international conference on formal methods and models for codesign, pp 21–23

  16. Dokhanchi A, Hoxha B, Fainekos G (2016) Formal requirement debugging for testing and verification of cyber-physical systems. arXiv preprint arXiv:1607.02549

  17. Dravnieks EW (1989) Identifying minimal sets of inconsistent constraints in linear programs: deletion, squeeze and sensitivity filtering. Carleton University

  18. Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: Proceedings of the 21st international conference on software engineering, pp 411–420

  19. Fisman D, Kupferman O, Sheinvald-Faragy S, Vardi MY (2008) A framework for inherent vacuity. In: Haifa verification conference, Springer, pp 7–22

  20. Goré R, Huang J, Sergeant T, Thomson J (2013) Finding minimal unsatisfiable subsets in linear temporal logic using BDDS. https://www.timsergeant.com/files/pltlmup/gore_huang_sergeant_thomson_mus_pltl.pdf

  21. Hustadt U, Konev B (2003) TRP++ 2.0: A temporal resolution prover. In: 19th international conference on automated deduction, pp 274–278

  22. Junker U (2001) Quickxplain: Conflict detection for arbitrary constraint propagation algorithms. In: IJCAI01 workshop on modelling and solving problems with constraints

  23. Kesten Y, Manna Z, McGuire H, Pnueli A (1993) A decision algorithm for full propositional temporal logic. In: International conference on computer aided verification, Springer, pp 97–109

  24. Konrad S, Cheng BH (2005) Real-time specification patterns. In: Proceedings of the 27th international conference on software engineering, pp 372–381

  25. Li J, Pu G, Zhang L, Yao Y, Vardi M Y et al. (2013) Polsat: A portfolio LTL satisfiability solver. arXiv preprint arXiv:1311.1602

  26. Li J, Yao Y, Pu G, Zhang L, He J (2014) Aalta: an LTL satisfiability checker over infinite/finite traces. In: Proceedings of the 22nd ACM SIGSOFT international symposium on foundations of software engineering, pp 731–734

  27. Li J, Zhang L, Pu G, Vardi MY, He J (2013) LTL satisfiability checking revisited. In: 20th international symposium on temporal representation and reasoning, pp 91–98

  28. Li J, Zhu S, Pu G, Vardi MY (2015) Sat-based explicit LTL reasoning. In: 11th Haifa verification conference, pp 209–224

  29. Liffiton MH, Malik A (2013) Enumerating infeasibility: finding multiple muses quickly. In: International conference on AI and OR techniques in constraint programming for combinatorial optimization problems, Springer, pp 160–175

  30. Liffiton MH, Sakallah KA (2008) Algorithms for computing minimal unsatisfiable subsets of constraints. J Autom Reason 40(1):1–33

    Article  MathSciNet  MATH  Google Scholar 

  31. Lumpe M, Meedeniya I, Grunske L (2011) PSPWizard: machine-assisted definition of temporal logical properties with specification patterns. In: Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on foundations of software engineering, pp 468–471

  32. Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signals. In: Formal techniques, modelling and analysis of timed and fault-tolerant systems, Springer, pp 152–166

  33. Manna Z, Pnueli A (2012) Temporal verification of reactive systems: safety. Springer, Berlin

    MATH  Google Scholar 

  34. Marques-Silva J, Lynce I (2011) On improving MUS extraction algorithms. In: International conference on theory and applications of satisfiability testing. Springer, pp 159–173

  35. Masin M, Palumbo F, Myrhaug H, de Oliveira Filho J, Pastena M, Pelcat M, Raffo L, Regazzoni F, Sanchez A, Toffetti A, et al. (2017) Cross-layer design of reconfigurable cyber-physical systems. In: 2017 design, automation & test in Europe conference & exhibition (DATE), pp 740–745. IEEE

  36. Nadel A (2010) Boosting minimal unsatisfiable core extraction. In: Proceedings of the 2010 conference on formal methods in computer-aided design, pp 221–229. FMCAD Inc

  37. Narizzano M, Pulina L, Tacchella A, Vuotto S (2018) Consistency of property specification patterns with boolean and constrained numerical signals. In: NASA formal methods: 10th international symposium, NFM 2018, Newport News, VA, USA, April 17–19, 2018, Proceedings, vol 10811. Springer, pp 383–398

  38. Pnueli A (1977) The temporal logic of programs. In: 18th annual symposium on foundations of computer science, 1977, pp 46–57. IEEE

  39. Pnueli A, Manna Z (1992) The temporal logic of reactive and concurrent systems. Springer, Berlin 16:12

  40. Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 179–190. ACM

  41. Post A, Hoenicke J (2012) Formalization and analysis of real-time requirements: a feasibility study at BOSCH. Verified software: theories, tools, experiments, pp 225–240

  42. Rozier KY, Vardi MY (2007) LTL satisfiability checking. In: Spin. vol. 4595, pp 149–167. Springer

  43. Rozier KY, Vardi MY (2010) LTL satisfiability checking. Int J Softw Tools Technol Transf (STTT) 12(2):123–137

    Article  Google Scholar 

  44. Rozier KY, Vardi MY (2011) A multi-encoding approach for LTL symbolic satisfiability checking. In: International symposium on formal methods, Springer, pp 417–431

  45. Schuppan V (2016) Extracting unsatisfiable cores for lTl via temporal resolution. Acta Inform 53(3):247–299

    Article  MathSciNet  MATH  Google Scholar 

  46. Schwendimann S (1998) A new one-pass tableau calculus for PLTL. In: International conference on automated reasoning with analytic tableaux and related methods, Springer, pp 277–291

  47. Wolper P (1985) The tableau method for temporal logic: an overview. Logique et Analyse 28(110/111):119–136

    MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

The research of Luca Pulina and Simone Vuotto has been funded by the EU Commissions H2020 Programme under grant agreement No. 732105 (CERBERO project). The research of Luca Pulina has been also partially funded by the Sardinian Regional Project PROSSIMO (POR FESR 2014/20-ASSE I).

Author information

Authors and Affiliations

  1. DIBRIS, University of Genoa, Viale Causa 13, 16145, Genoa, Italy

    Massimo Narizzano, Armando Tacchella & Simone Vuotto

  2. Chemistry and Pharmacy Department, University of Sassari, Via Vienna 2, Sassari, Italy

    Luca Pulina & Simone Vuotto

Authors
  1. Massimo Narizzano
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luca Pulina
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Armando Tacchella
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Simone Vuotto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Simone Vuotto.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Narizzano, M., Pulina, L., Tacchella, A. et al. Property specification patterns at work: verification and inconsistency explanation. Innovations Syst Softw Eng 15, 307–323 (2019). https://doi.org/10.1007/s11334-019-00339-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11334-019-00339-1

Keywords

Search

Navigation