×

Temporal logic specification mining of programs. (English) Zbl 1477.68168

Summary: This paper proposes a dynamic approach of specification mining for Propositional Projection Temporal Logic (PPTL). To this end, a pattern library is built to collect some common temporal relation among events. Further, several algorithms of specification mining for PPTL are designed. With our approach, PPTL specifications are mined from a trace set of a target program by using patterns in the library. In addition, a specification mining tool PPTLMiner supporting this approach is developed. In practice, given a trace set and user selected patterns, PPTLMiner can capture PPTL specifications of target programs.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] The Daikon Invariant Detector
[2] Autili, M.; Grunske, L.; Lumpe, M.; Pelliccione, P.; Tang, A., Aligning qualitative, real-time, and probabilistic property specification patterns using a structured English grammar, IEEE Trans. Softw. Eng., 41, 7, 620-638 (2015)
[3] Diekert, V.; Rozenberg, G., The Book of Traces (1995), World Scientific
[4] Duan, Z., Temporal Logic and Temporal Logic Programming (2005), Science Press: Science Press Beijing
[5] Duan, Z.; Tian, C.; Zhang, L., A decision procedure for propositional projection temporal logic with infinite models, Acta Inform., 45, 1, 43-78 (2008) · Zbl 1141.68039
[6] Duan, Z.; Tian, C.; Zhang, N., A canonical form based decision procedure and model checking approach for propositional projection temporal logic, Theor. Comput. Sci., 609, 544-560 (2016) · Zbl 1370.68200
[7] Dupont, P.; Lambeau, B.; Damas, C.; Lamsweerde, A., The QSM algorithm and its application to software behavior model induction, Appl. Artif. Intell., 22, 1&2, 77-115 (2008)
[8] Dwyer, M. B.; Avrunin, G. S.; Corbett, J. C., Patterns in property specifications for finite-state verification, (Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No. 99CB37002) (1999)), 411-420
[9] Iegorov, O.; Fischmeister, S., Mining task precedence graphs from real-time embedded system traces, (Proceedings of the 2018 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS) (2018)), 251-260
[10] Konrad, S.; Cheng, B. H.C., Facilitating the construction of specification pattern-based properties, (Proceedings of the 2005 IEEE International Conference on Requirements Engineering (RE’05) (2005)), 329-338
[11] Le, T. B.; Lo, D., Deep specification mining, (Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis (2018)), 106-117
[12] Lemieux, C.; Park, D.; Beschastnikh, I., General LTL specification mining (t), (Proceedings of the 2015 IEEE/ACM International Conference on Automated Software Engineering (ASE) (2015)), 81-92
[13] Li, H.; Shen, L. M.; Ma, C.; Liu, M. Y., Role behavior detection method of privilege escalation attacks for Android applications, Int. J. Perform. Eng., 15, 6, 1631-1641 (2019)
[14] Lo, D.; Khoo, S. C., Mining patterns and rules for software specification discovery, (Proceedings of the VLDB Endowment, Vol. 1 (2008)), 1609-1616
[15] Narayan, A.; Cutulenco, G.; Joshi, Y.; Fischmeister, S., Mining timed regular specifications from system traces, ACM Trans. Embed. Comput. Syst., 17, 2, 1-21 (2018)
[16] Pradel, M.; Gross, T. R., Automatic generation of object usage specifications from large method traces, (Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering (2009)), 371-382
[17] Ratcliff, S.; White, D.; Clark, J., Searching for invariants using genetic programming and mutation testing, (Proceedings of the 2011 Annual Genetic and Evolutionary Computation Conference (2011)), 1907-1914
[18] Reger, G.; Havelund, K., What is a trace? A runtime verification perspective, (Proceedings of the 2016 International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - ISoLA 2016 (2016)), 339-355
[19] Schmidt, L.; Narayan, A.; Fischmeister, S., TREM: a tool for mining timed regular specifications from system traces, (Proceedings of the 2017 IEEE/ACM International Conference on Automated Software Engineering (2017)), 901-906
[20] Tian, C.; Duan, Z., Expressiveness of propositional projection temporal logic with star, Theor. Comput. Sci., 412, 18, 1729-1744 (2011) · Zbl 1221.03018
[21] Walkinshaw, N.; Bogdanov, K., Inferring finite-state models with temporal constraints, (Proceedings of the 2008 IEEE/ACM International Conference on Automated Software Engineering (2008)), 248-257
[22] Walkinshaw, N.; Bogdanov, K.; Holcombe, M.; Salahuddin, S., Reverse engineering state machines by interactive grammar inference, (Proceedings of the 2007 Working Conference on Reverse Engineering (2007)), 209-218
[23] Wasylkowski, A.; Zeller, A., Mining temporal specifications from object usage, (Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering (2009)), 295-306
[24] Weimer, W.; Necula, G. C., Mining temporal specifications for error detection, (Proceedings of the 2005 Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2005)), 461-476 · Zbl 1087.68600
[25] Yang, J.; Evans, D.; Bhardwaj, D.; Bhat, T.; Das. Perracotta, M., Mining temporal API rules from imperfect traces, (Proceedings of the 2006 International Conference on Software Engineering (2006)), 282-291
[26] Zhang, N.; Duan, Z. H.; Tian, C., A complete axiom system for propositional projection temporal logic with cylinder computation model, Theor. Comput. Sci., 609, 639-657 (2016) · Zbl 1332.68145
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.