Enhancing active model learning with equivalence checking using simulation relations

Springer Science and Business Media LLC - 2022
Yogananda Jeppu1, Tom Melham1, Daniel Kroening2
1University Of Oxford, Oxford, UK
2Amazon, Inc., Seattle, USA

Tóm tắt

AbstractWe present a new active model-learning approach to generating abstractions of a system from its execution traces. Given a system and a set of observables to collect execution traces, the abstraction produced by the algorithm is guaranteed to admit all system traces over the set of observables. To achieve this, the approach uses a pluggable model-learning component that can generate a model from a given set of traces. Conditions that encode a certain completeness hypothesis, formulated based on simulation relations, are then extracted from the abstraction under construction and used to evaluate its degree of completeness. The extracted conditions are sufficient to prove model completeness but not necessary. If all conditions are true, the algorithm terminates, returning a system overapproximation. A condition falsification may not necessarily correspond to missing system behaviour in the abstraction. This is resolved by applying model checking to determine whether it corresponds to any concrete system trace. If so, the new concrete trace is used to iteratively learn new abstractions, until all extracted completeness conditions are true. To evaluate the approach, we reverse-engineer a set of publicly available Simulink Stateflow models from their C implementations. Our algorithm generates an equivalent model for 98% of the Stateflow models.

Từ khóa


Tài liệu tham khảo

Aarts F, Jonsson B, Uijen J (2010) Generating models of infinite-state communication protocols using regular inference with abstraction. In: Petrenko A, Simão A, Maldonado JC (eds) Testing software and systems. Springer, pp 188–204. https://doi.org/10.1007/978-3-642-16573-3_14

Aarts F, Heidarian F, Kuppens H, et al (2012) Automata learning through counterexample guided abstraction refinement. In: Giannakopoulou D, Méry D (eds) Formal methods. Springer, pp 10–27. https://doi.org/10.1007/978-3-642-32759-9_4

Alur R, Benedikt M, Etessami K, et al (2005) Analysis of recursive state machines. In: ACM Trans. Program. Lang. Syst., vol 27. Association for Computing Machinery, pp 786-818. https://doi.org/10.1145/1075382.1075387

Angluin D (1987) Learning regular sets from queries and counterexamples. In: Inf. Comput., vol 75. Academic Press, Inc., pp 87–106. https://doi.org/10.1016/0890-5401(87)90052-6

Argyros G, D’Antoni L (2018) The learnability of symbolic automata. In: Chockler H, Weissenbacher G (eds) Computer aided verification. Springer, pp 427–445. https://doi.org/10.1007/978-3-319-96145-3_23

Ashar P, Ghosh A, Devadas S (1992) Boolean satisfiability and equivalence checking using general binary decision diagrams. In: Integration, pp 1–16. https://doi.org/10.1016/0167-9260(92)90015-Q

Berg T, Jonsson B, Raffelt H (2008) Regular inference for state machines using domains with equality tests. In: Fiadeiro JL, Inverardi P (eds) Fundamental approaches to software engineering. Springer, pp 317–331.https://doi.org/10.1007/978-3-540-78743-3_24

Biermann AW, Feldman JA (1972) On the synthesis of finite-state machines from samples of their behavior. In: IEEE Trans. Comput., vol 21. IEEE Computer Society, pp 592–597. https://doi.org/10.1109/TC.1972.5009015

Botinčan M, Babić D (2013) Sigma*: Symbolic learning of input-output specifications. In: Principles of programming languages. ACM, POPL ’13, pp 443–456. https://doi.org/10.1145/2429069.2429123

Cassel S, Howar F, Jonsson B (2015) RALib: a LearnLib extension for inferring EFSMs. In: DIFTS

Cassel S, Howar F, Jonsson B, et al (2016) Active learning for extended finite state machines. In: Formal aspects of computing, pp 233–263. https://doi.org/10.1007/s00165-016-0355-5

Chockler H, Kesseli P, Kroening D, et al (2020) Learning the language of software errors. In: Journal artificial intelligence research, vol 67. Morgan Kaufmann Publishers, Inc., pp 881–903. https://doi.org/10.1613/jair.1.11798

Clarke E, Grumberg O, Jha S, et al (2000) Counterexample-guided abstraction refinement. In: Emerson EA, Sistla AP (eds) Computer aided verification. Springer, pp 154–169. https://doi.org/10.1007/10722167_15

Clarke E, Kroening D, Yorav K (2003) Behavioral consistency of C and Verilog programs using bounded model checking. In: Design automation conference. Association for Computing Machinery, DAC ’03, pp 368–371.https://doi.org/10.1145/775832.775928

Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Tools and algorithms for the construction and analysis of systems. Springer, pp 168–176. https://doi.org/10.1007/978-3-540-24730-2_15

Clarke EM, Grumberg O, Kroening D et al (2018) Model checking, 2nd edn. MIT Press

Cobleigh JM, Giannakopoulou D, Păsăreanu CS (2003) Learning assumptions for compositional verification. In: Garavel H, Hatcliff J (eds) Tools and algorithms for the construction and analysis of systems. Springer, pp 331–346. https://doi.org/10.1007/3-540-36577-X_24

Dorofeeva R, El-Fakih K, Maag S, et al (2010) FSM-based conformance testing methods: a survey annotated with experimental evaluation. In: Information and software technology, pp 1286–1297. https://doi.org/10.1016/j.infsof.2010.07.001

Dupont P, Lambeau B, Damas C, et al (2008) The QSM algorithm and its application to software behavior model induction. In: Applied artificial intelligence, vol 22. Taylor & Francis, pp 77–115. https://doi.org/10.1080/08839510701853200

Feng L, Kwiatkowska M, Parker D (2011) Automated learning of probabilistic assumptions for compositional reasoning. In: Giannakopoulou D, Orejas F (eds) Fundamental approaches to software engineering. Springer, pp 2–17. https://doi.org/10.1007/978-3-642-19811-3_2

Fiterău-Broştean P, Howar F (2017) Learning-based testing the sliding window behavior of TCP implementations. In: Petrucci L, Seceleanu C, Cavalcanti A (eds) Critical systems: formal methods and automated verification. Springer, pp 185–200. https://doi.org/10.1007/978-3-319-67113-0_12

Gallier J, La Torre S, Mukhopadhyay S (2003) Deterministic finite automata with recursive calls and DPDAs. In: Inf. Process. Lett., pp 187–193. https://doi.org/10.1016/S0020-0190(03)00281-3

Garhewal B, Vaandrager F, Howar F, et al (2020) Grey-box learning of register automata. In: Integrated formal methods. Springer, pp 22–40. https://doi.org/10.1007/978-3-030-63461-2_2

Giannakopoulou D, Rakamarić Z, Raman V (2012) Symbolic learning of component interfaces. In: Miné A, Schmidt D (eds) Static analysis. Springer, pp 248–264. https://doi.org/10.1007/978-3-642-33125-1_18

Goldberg E, Prasad M, Brayton R (2001) Using SAT for combinational equivalence checking. In: Design, automation and test in Europe, pp 114–121. https://doi.org/10.1109/DATE.2001.915010

Groce A, Peled D, Yannakakis M (2002) Adaptive model checking. In: Katoen JP, Stevens P (eds) Tools and algorithms for the construction and analysis of systems. Springer, pp 357–370. https://doi.org/10.1007/3-540-46002-0_25

Heule MJH, Verwer S (2010) Exact DFA identification using SAT solvers. In: Sempere JM, García P (eds) Grammatical inference: theoretical results and applications. Springer, pp 66–79. https://doi.org/10.1007/978-3-642-15488-1_7

Howar F, Steffen B (2018) Active automata learning in practice: an annotated bibliography of the years 2011 to 2016. In: Bennaceur A, Hähnle R, Meinke K (eds) Machine learning for dynamic software analysis, lecture notes in computer science, vol 11026. Springer, pp 123–148. https://doi.org/10.1007/978-3-319-96562-8_5

Howar F, Steffen B, Merten M (2011) Automata learning with automated alphabet abstraction refinement. In: Jhala R, Schmidt D (eds) Verification, model checking, and abstract interpretation. Springer, pp 263–277.https://doi.org/10.1007/978-3-642-18275-4_19

Howar F, Giannakopoulou D, Rakamarić Z (2013) Hybrid learning: Interface generation through static, dynamic, and symbolic analysis. In: Symposium on software testing and analysis. Association for Computing Machinery, ISSTA, pp 268–279. https://doi.org/10.1145/2483760.2483783

Howar F, Jonsson B, Vaandrager F (2019) Combining black-box and white-box techniques for learning register automata. In: Steffen B, Woeginger G (eds) Computing and software science: state of the art and perspectives. Springer, pp 563–588. https://doi.org/10.1007/978-3-319-91908-9_26

Isberner M, Howar F, Steffen B (2014) The TTT algorithm: A redundancy-free approach to active automata learning. In: Bonakdarpour B, Smolka SA (eds) Runtime verification. Springer, pp 307–322. https://doi.org/10.1007/978-3-319-11164-3_26

Jeppu NY (2020) Trace2Model Github repository. https://github.com/natasha-jeppu/Trace2Model

Jeppu NY (2021) ActiveLearning. https://github.com/natasha-jeppu/ActiveLearning

Jeppu NY (2023). Active learning implementation. https://doi.org/10.5287/ora-aownkwvym

Jeppu NY, Melham T, Kroening D, et al (2020) Learning concise models from long execution traces. In: 57th ACM/IEEE design automation conference (DAC), pp 1–6. https://doi.org/10.1109/DAC18072.2020.9218613

Kearns MJ, Vazirani UV (1994) An introduction to computational learning theory. MIT Press

King JC (1976) Symbolic execution and program testing. In: Commun. ACM, vol 19. Association for Computing Machinery, pp 385–394. https://doi.org/10.1145/360248.360252

Kroening D, Clarke E (2004) Checking consistency of C and Verilog using predicate abstraction and induction. pp 66–72. https://doi.org/10.1109/ICCAD.2004.1382544

Lang KJ, Pearlmutter BA, Price RA (1998) Results of the Abbadingo One DFA learning competition and a new evidence-driven state merging algorithm. In: Honavar V, Slutzki G (eds) Grammatical inference. Springer, pp 1–12. https://doi.org/10.1007/BFb0054059

Lorenzoli D, Mariani L, Pezzè M (2008) Automatic generation of software behavioral models. In: ACM/IEEE 30th international conference on software engineering, pp 501–510. https://doi.org/10.1145/1368088.1368157

Maler O, Mens I (2014a) Learning regular languages over large ordered alphabets. In: Logical methods in computer science. https://doi.org/10.2168/LMCS-11(3:13)2015

Maler O, Mens IE (2014b) Learning regular languages over large alphabets. In: Ábrahám E, Havelund K (eds) Tools and algorithms for the construction and analysis of systems. Springer, pp 485–499. https://doi.org/10.1007/978-3-642-54862-8_41

Marques-Silva J, Glass T (1999) Combinational equivalence checking using satisfiability and recursive learning. In: Design, automation and test in Europe, pp 145–149. https://doi.org/10.1109/DATE.1999.761110

Marquez CIC, Strum M, Chau WJ (2013) Formal equivalence checking between high-level and RTL hardware designs. In: Latin American test workshop (LATW), pp 1–6. https://doi.org/10.1109/LATW.2013.6562666

Mukherjee R, Kroening D, Melham T, et al (2015) Equivalence checking using trace partitioning. In: VLSI, pp 13–18. https://doi.org/10.1109/ISVLSI.2015.110

Park DMR (1981) Concurrency and automata on infinite sequences. In: Theoretical computer science, lecture notes in computer science, vol 104. Springer, pp 167–183. https://doi.org/10.1007/BFb0017309

Peled D, Vardi M, Yannakakis M (2002) Black box checking. In: Journal of automata, languages and combinatorics, pp 225–246. https://doi.org/10.1007/978-0-387-35578-8_13

Rivest RL, Schapire RE (1989) Inference of finite automata using homing sequences. In: Theory of computing. Association for Computing Machinery, STOC ’89, pp 411–420. https://doi.org/10.1145/73007.73047

Ruf J, Hoffmann D, Kropf T, et al (2001) Simulation-guided property checking based on multi-valued AR-automata. In: Design, automation and test in Europe. IEEE, pp 742–748. https://doi.org/10.1109/DATE.2001.915111

Shahbaz M, Groz R (2009) Inferring Mealy machines. In: Cavalcanti A, Dams DR (eds) Formal methods. Springer, pp 207–222. https://doi.org/10.1007/978-3-642-05089-3_14

Sheeran M, Singh S, Stålmarck G (2000) Checking safety properties using induction and a SAT-solver. In: Hunt WA, Johnson SD (eds) Formal methods in computer-aided design. Springer, pp 127–144. https://doi.org/10.1007/3-540-40922-X_8

Simulink (2021) Embedded Coder. https://uk.mathworks.com/products/embedded-coder.html

Simulink (2021a) Simulation and Model-Based Design. https://www.mathworks.com/products/simulink.html

Simulink (2021b) Stateflow Examples. https://uk.mathworks.com/help/stateflow/examples.html?s_tid=CRUX_topnav

Smetsers R, Moerman J, Janssen M, et al (2016) Complementing model learning with mutation-based fuzzing. arXiv:1611.02429

Steffen B, Hungar H (2003) Behavior-based model construction. In: Zuck LD, Attie PC, Cortesi A, et al (eds) Verification, model checking, and abstract interpretation. Springer, pp 5–19. https://doi.org/10.1007/s10009-004-0139-8

Ulyantsev V, Tsarev F (2011) Extended finite-state machine induction using SAT-solver. In: International conference on machine learning and applications and workshops, pp 346–349. https://doi.org/10.1109/ICMLA.2011.166

Ulyantsev V, Buzhinsky I, Shalyto A (2018) Exact finite-state machine identification from scenarios and temporal properties. In: International journal on software tools for technology transfer. https://doi.org/10.1007/s10009-016-0442-1

Vaandrager F, Bloem R, Ebrahimi M (2021) Learning Mealy machines with one timer. In: Leporati A, Martín-Vide C, Shapira D, et al (eds) Language and automata theory and applications. Springer, pp 157–170. https://doi.org/10.1007/978-3-030-68195-1_13

van Eijk CAJ (2000) Sequential equivalence checking based on structural similarities. In: IEEE Transactions on computer-aided design of integrated circuits and systems, pp 814–819. https://doi.org/10.1109/43.851997

Walkinshaw N, Bogdanov K (2008) Inferring finite-state models with temporal constraints. In: Automated software engineering, pp 248–257. https://doi.org/10.1109/ASE.2008.35

Walkinshaw N, Hall M (2016) Inferring computational state machine models from program executions. In: International conference on software maintenance and evolution (ICSME). IEEE, pp 122–132. https://doi.org/10.1109/ICSME.2016.74

Walkinshaw N, Derrick J, Guo Q (2009) Iterative refinement of reverse-engineered models by model-based testing. In: Cavalcanti A, Dams DR (eds) Formal methods. Springer, pp 305–320. https://doi.org/10.1007/978-3-642-05089-3_20

Walkinshaw N, Taylor R, Derrick J (2016) Inferring extended finite state machine models from software executions. In: Empirical software engineering, pp 811–853. https://doi.org/10.1007/s10664-015-9367-7

Zalewski M (2013) American Fuzzy Lop (AFL) fuzzer. https://lcamtuf.coredump.cx/afl/

Thông tin
Thông tin xuất bản

Springer Science and Business Media LLC

Thông tin tác giả