research-article

Learning Temporal Specifications from Imperfect Traces Using Bayesian Inference

Authors:

Sebastian Steinhorst,

Stephan GünnemannAuthors Info & Claims

DAC '19: Proceedings of the 56th Annual Design Automation Conference 2019

Article No.: 96, Pages 1 - 6

https://doi.org/10.1145/3316781.3317847

Published: 02 June 2019 Publication History

Abstract

Verification is essential to prevent malfunctioning of software systems. Model checking allows to verify conformity with nominal behavior. As manual definition of specifications from such systems gets infeasible, automated techniques to mine specifications from data become increasingly important. Existing approaches produce specifications of limited lengths, do not segregate functions and do not easily allow to include expert input. We present BaySpec, a dynamic mining approach to extract temporal specifications from Bayesian models, which represent behavioral patterns. This allows to learn specifications of arbitrary length from imperfect traces. Within this framework we introduce a novel extraction algorithm that for the first time mines LTL specifications from such models.

References

[1]

R. Alur, P. Černy, P. Madhusudan, and W. Nam. 2005. Synthesis of interface specifications for Java classes. ACM SIGPLAN Notices 40, 1 (2005).

Digital Library

[2]

G. Ammons, R. Bodík, and J.R. Larus. 2002. Mining specifications. ACM Sigplan Notices 37, 1 (2002).

Digital Library

[3]

I. Beschastnikh, Y. Brun, S. Schneider, M. Sloan, and M.D. Ernst. 2011. Leveraging existing instrumentation to automatically infer invariant-constrained models. In Proc. of the ESEC/FSE '11.

Digital Library

[4]

M. Bonato, G. Di Guglielmo, M. Fujita, F. Fummi, and G. Pravadelli. 2012. Dynamic property mining for embedded software. In ACM Proc. of CODES+ISSS 2012.

Digital Library

[5]

G. Cutulenco, Y. Joshi, A. Narayan, and S. Fischmeister. 2016. Mining timed regular expressions from system traces. In Proc. of the ASE '16.

Digital Library

[6]

A. Danese, T. Ghasempouri, and G. Pravadelli. 2015. Automatic extraction of assertions from execution traces of behavioural models. In IEEE Proc. of DATE 2015.

Digital Library

[7]

D. Engler, D.Y. Chen, S. Hallem, A. Chou, and B. Chelf. 2001. Bugs as deviant behavior: A general approach to inferring errors in systems code. In ACM SIGOPS Operating Systems Review, Vol. 35.

Digital Library

[8]

D. Eppstein. 1998. Finding the k shortest paths. SIAM Journal on computing 28, 2 (1998).

[9]

M.D. Ernst, J. Cockrell, W.G. Griswold, and D. Notkin. 2001. Dynamically discovering likely program invariants to support program evolution. IEEE Trans. on Software Engineering 27, 2 (2001).

Digital Library

[10]

M. Gabel and Z. Su. 2008. Javert: fully automatic mining of general temporal properties from dynamic traces. In Proc. of SIGSOFT '08.

Digital Library

[11]

C. Lemieux, D. Park, and I. Beschastnikh. 2015. General LTL specification mining (t). In Proc. of ASE 2015.

[12]

V.I. Levenshtein. 1966. Binary codes capable of correcting deletions, insertions, and reversals. In Soviet physics doklady.

[13]

W. Li, A. Forin, and S.A. Seshia. 2010. Scalable specification mining for verification and diagnosis. In Proceedings of DAC 2010.

Digital Library

[14]

D. Lo and S.C. Khoo. 2006. SMArTIC: towards building an accurate, robust and scalable specification miner. In SIGSOFT '06.

Digital Library

[15]

D. Lo, S.C. Khoo, and C. Liu. 2008. Mining temporal rules for software maintenance. Journal of Software Maintenance and Evolution: Research and Practice 20, 4 (2008).

Digital Library

[16]

A. Mrowca, T. Pramsohler, S. Steinhorst, and U. Baumgarten. 2018. Automated interpretation and reduction of in-vehicle network traces at a large scale. In Proceedings of DAC 2018. IEEE.

Digital Library

[17]

M.K. Ramanathan, A. Grama, and S. Jagannathan. 2007. Static specification inference using predicate mining. In ACM SIGPLAN Notices, Vol. 42.

Digital Library

[18]

S. Shoham, E. Yahav, S.J. Fink, and M. Pistoia. 2008. Static specification mining using automata-based abstractions. IEEE Trans. on Software Engineering 34, 5 (2008).

Digital Library

[19]

S. Vasudevan, D. Sheridan, S. Patel, D. Tcheng, B. Tuohy, and D. Johnson. 2010. Goldmine: Automatic assertion generation using data mining and static analysis. In IEEE Proc. of DATE 2010.

Digital Library

[20]

A. Viterbi. 1967. Error bounds for convolutional codes and an asymptotically optimum decoding algorithm. IEEE Trans. on Information Theory 13, 2 (1967).

Digital Library

[21]

J. Yang, D. Evans, D. Bhardwaj, T. Bhat, and M. Das. 2006. Perracotta: mining temporal API rules from imperfect traces. In Proc. of ICSE 2006.

Digital Library

[22]

J.Y. Yen. 1971. Finding the k shortest loopless paths in a network. management Science 17, 11 (1971).

Cited By

Ahmed MNadimi BZheng H(2023)System-on-Chip Message Flow Mining with Masked-Language Models2023 IEEE 66th International Midwest Symposium on Circuits and Systems (MWSCAS)10.1109/MWSCAS57524.2023.10406038(496-500)Online publication date: 6-Aug-2023
https://doi.org/10.1109/MWSCAS57524.2023.10406038
Ielo ALaw MFionda VRicca FDe Giacomo GRusso A(2023)Towards ILP-Based $$\text {LTL}_\text {f}$$ Passive LearningInductive Logic Programming10.1007/978-3-031-49299-0_3(30-45)Online publication date: 22-Dec-2023
https://doi.org/10.1007/978-3-031-49299-0_3
Ahmed MZheng HMukherjee PKetkar MYang J(2022)Mining Patterns From Concurrent Execution TracesIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2021.310951341:8(2758-2762)Online publication date: Aug-2022
https://doi.org/10.1109/TCAD.2021.3109513
Show More Cited By

Recommendations

Automata-based Pattern Mining from Imperfect Traces

This paper considers automata-based pattern mining techniques for extracting specifications from runtime traces and suggests a novel extension that allows these techniques to work with so-called imperfect traces i.e. traces that do not exactly satisfy ...
Bayesian inference of temporal task specifications from demonstrations
NIPS'18: Proceedings of the 32nd International Conference on Neural Information Processing Systems

When observing task demonstrations, human apprentices are able to identify whether a given task is executed correctly long before they gain expertise in actually performing that task. Prior research into learning from demonstrations (LfD) has failed to ...
Extracting significant specifications from mining through mutation testing
ICFEM'11: Proceedings of the 13th international conference on Formal methods and software engineering

Specification mining techniques are used to automatically infer interaction specifications among objects in the format of call sequences, but many of these specifications can be meaningless or insignificant. As a consequence, when used in program ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '19: Proceedings of the 56th Annual Design Automation Conference 2019

June 2019

1378 pages

ISBN:9781450367257

DOI:10.1145/3316781

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CEDA

In-Cooperation

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 June 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

DAC '19

Sponsor:

SIGDA

DAC '19: The 56th Annual Design Automation Conference 2019

June 2 - 6, 2019

NV, Las Vegas, USA

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
208
Total Downloads

Downloads (Last 12 months)18
Downloads (Last 6 weeks)8

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ahmed MNadimi BZheng H(2023)System-on-Chip Message Flow Mining with Masked-Language Models2023 IEEE 66th International Midwest Symposium on Circuits and Systems (MWSCAS)10.1109/MWSCAS57524.2023.10406038(496-500)Online publication date: 6-Aug-2023
https://doi.org/10.1109/MWSCAS57524.2023.10406038
Ielo ALaw MFionda VRicca FDe Giacomo GRusso A(2023)Towards ILP-Based $$\text {LTL}_\text {f}$$ Passive LearningInductive Logic Programming10.1007/978-3-031-49299-0_3(30-45)Online publication date: 22-Dec-2023
https://doi.org/10.1007/978-3-031-49299-0_3
Ahmed MZheng HMukherjee PKetkar MYang J(2022)Mining Patterns From Concurrent Execution TracesIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2021.310951341:8(2758-2762)Online publication date: Aug-2022
https://doi.org/10.1109/TCAD.2021.3109513
Ahmed MZheng HMukherjee PKetkar MYang J(2021)A Comparative Study of Specification Mining Methods for SoC Communication Traces2021 IEEE Computer Society Annual Symposium on VLSI (ISVLSI)10.1109/ISVLSI51109.2021.00017(31-36)Online publication date: Jul-2021
https://doi.org/10.1109/ISVLSI51109.2021.00017
Ahmed MZheng HMukherjee PKetkar MYang J(2021)Mining Message Flows from System-on-Chip Execution Traces2021 22nd International Symposium on Quality Electronic Design (ISQED)10.1109/ISQED51717.2021.9424306(374-380)Online publication date: 7-Apr-2021
https://doi.org/10.1109/ISQED51717.2021.9424306
Zheng HAhmed MMukherjee PKetkar MYang J(2021)Model Synthesis for Communication Traces of System Designs2021 IEEE 39th International Conference on Computer Design (ICCD)10.1109/ICCD53106.2021.00082(492-499)Online publication date: Oct-2021
https://doi.org/10.1109/ICCD53106.2021.00082
Mrowca AGyrock FGünnemann S(2021)Temporal state change Bayesian networks for modeling of evolving multivariate state sequences: model, structure discovery and parameter estimationData Mining and Knowledge Discovery10.1007/s10618-021-00807-yOnline publication date: 1-Nov-2021
https://doi.org/10.1007/s10618-021-00807-y
Wang FCao ZTan LZong H(2020)Survey on learning-based formal methods: Taxonomy, Applications and Possible future directionsIEEE Access10.1109/ACCESS.2020.3000907(1-1)Online publication date: 2020
https://doi.org/10.1109/ACCESS.2020.3000907

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents