Advertisement

Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals

  • Massimo Narizzano
  • Luca Pulina
  • Armando Tacchella
  • Simone Vuotto
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10811)

Abstract

Property Specification Patterns (PSPs) have been proposed to solve recurring specification needs, to ease the formalization of requirements, and enable automated verification thereof. In this paper, we extend PSPs by considering Boolean as well as atomic numerical assertions. This extension enables us to reason about functional requirements which would not be captured by basic PSPs. We contribute an encoding from constrained PSPs to LTL formulae, and we show experimental results demonstrating that our approach scales on requirements of realistic size generated using a probabilistic model. Finally, we show that our extension enables us to prove (in)consistency of requirements about an embedded controller for a robotic manipulator.

Notes

Acknowledgments

The research of Luca Pulina and Simone Vuotto has been funded by the EU Commissions H2020 Programme under grant agreement N.732105 (CERBERO project).

References

  1. 1.
    Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45657-0_29 CrossRefGoogle Scholar
  2. 2.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244–263 (1986)CrossRefzbMATHGoogle Scholar
  3. 3.
    Comon, H., Cortier, V.: Flatness is not a weakness. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 262–276. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-44622-2_17 CrossRefGoogle Scholar
  4. 4.
    Demri, S., DSouza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380–415 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Dillon, L.K., Kutty, G., Moser, L.E., Melliar-Smith, P.M., Ramakrishna, Y.S.: A graphical interval logic for specifying concurrent systems. ACM Trans. Softw. Eng. Methodol. (TOSEM) 3(2), 131–165 (1994)CrossRefzbMATHGoogle Scholar
  6. 6.
    Dokhanchi, A., Hoxha, B., Fainekos, G.: Metric interval temporal logic specification elicitation and debugging. In: 13th ACM-IEEE International Conference on Formal Methods and Models for Codesign, pp. 21–23 (2015)Google Scholar
  7. 7.
    Dokhanchi, A., Hoxha, B., Fainekos, G.: Formal requirement debugging for testing and verification of cyber-physical systems. arXiv preprint arXiv:1607.02549 (2016)
  8. 8.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, pp. 411–420 (1999)Google Scholar
  9. 9.
    Hustadt, U., Konev, B.: TRP++ 2.0: a temporal resolution prover. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 274–278. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-45085-6_21 CrossRefGoogle Scholar
  10. 10.
    Konrad, S., Cheng, B.H.: Real-time specification patterns. In: Proceedings of the 27th International Conference on Software Engineering, pp. 372–381 (2005)Google Scholar
  11. 11.
    Li, J., Pu, G., Zhang, L., Yao, Y., Vardi, M.Y., et al.: Polsat: a portfolio LTL satisfiability solver. arXiv preprint arXiv:1311.1602 (2013)
  12. 12.
    Li, J., Yao, Y., Pu, G., Zhang, L., He, J.: 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 (2014)Google Scholar
  13. 13.
    Li, J., Zhang, L., Pu, G., Vardi, M.Y., He, J.: LTL satisfiability checking revisited. In: 20th International Symposium on Temporal Representation and Reasoning, pp. 91–98 (2013)Google Scholar
  14. 14.
    Li, J., Zhu, S., Pu, G., Vardi, M.Y.: SAT-based explicit LTL reasoning. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 209–224. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-26287-1_13 CrossRefGoogle Scholar
  15. 15.
    Lumpe, M., Meedeniya, I., Grunske, L.: 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 (2011)Google Scholar
  16. 16.
    Masin, M., Palumbo, F., Myrhaug, H., de Oliveira Filho, J., Pastena, M., Pelcat, M., Raffo, L., Regazzoni, F., Sanchez, A., Toffetti, A., et al.: Cross-layer design of reconfigurable cyber-physical systems. In: 2017 Design, Automation and Test in Europe Conference and Exhibition (DATE), pp. 740–745. IEEE (2017)Google Scholar
  17. 17.
    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE (1977)Google Scholar
  18. 18.
    Pnueli, A., Manna, Z.: The temporal logic of reactive and concurrent systems. Springer 16, 12 (1992)zbMATHGoogle Scholar
  19. 19.
    Post, A., Hoenicke, J.: Formalization and analysis of real-time requirements: a feasibility study at BOSCH. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 225–240. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-27705-4_18 CrossRefGoogle Scholar
  20. 20.
    Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149–167. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73370-6_11 CrossRefGoogle Scholar
  21. 21.
    Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. Int. J. Softw. Tools Technol. Transf. (STTT) 12(2), 123–137 (2010)CrossRefGoogle Scholar
  22. 22.
    Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417–431. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-21437-0_31 CrossRefGoogle Scholar
  23. 23.
    Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 277–291. Springer, Heidelberg (1998).  https://doi.org/10.1007/3-540-69778-0_28 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.DIBRISUniversity of GenoaGenoaItaly
  2. 2.Chemistry and Pharmacy DepartmentUniversity of SassariSassariItaly

Personalised recommendations