Enhancing active model learning with equivalence checking using simulation relations
We 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 ac...
| Κύριοι συγγραφείς: | , , |
|---|---|
| Μορφή: | Journal article |
| Γλώσσα: | English |
| Έκδοση: |
Springer
2023
|
| _version_ | 1826311131723988992 |
|---|---|
| author | Yogananda Jeppu, N Melham, T Kroening, D |
| author_facet | Yogananda Jeppu, N Melham, T Kroening, D |
| author_sort | Yogananda Jeppu, N |
| collection | OXFORD |
| description | We 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. |
| first_indexed | 2024-03-07T08:03:51Z |
| format | Journal article |
| id | oxford-uuid:963755fc-639c-4e9a-8157-59593fdf1a5c |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T08:03:51Z |
| publishDate | 2023 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:963755fc-639c-4e9a-8157-59593fdf1a5c2023-10-12T14:41:08ZEnhancing active model learning with equivalence checking using simulation relationsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:963755fc-639c-4e9a-8157-59593fdf1a5cEnglishSymplectic ElementsSpringer2023Yogananda Jeppu, NMelham, TKroening, DWe 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. |
| spellingShingle | Yogananda Jeppu, N Melham, T Kroening, D Enhancing active model learning with equivalence checking using simulation relations |
| title | Enhancing active model learning with equivalence checking using simulation relations |
| title_full | Enhancing active model learning with equivalence checking using simulation relations |
| title_fullStr | Enhancing active model learning with equivalence checking using simulation relations |
| title_full_unstemmed | Enhancing active model learning with equivalence checking using simulation relations |
| title_short | Enhancing active model learning with equivalence checking using simulation relations |
| title_sort | enhancing active model learning with equivalence checking using simulation relations |
| work_keys_str_mv | AT yoganandajeppun enhancingactivemodellearningwithequivalencecheckingusingsimulationrelations AT melhamt enhancingactivemodellearningwithequivalencecheckingusingsimulationrelations AT kroeningd enhancingactivemodellearningwithequivalencecheckingusingsimulationrelations |