Classification-based parameter synthesis for parametric timed automata
Parametric timed automata are designed to model timed systems with unknown parameters, often representing design uncertainties of external environments. In order to design a robust system, it is crucial to synthesize constraints on the parameters, which guarantee the system behaves according to cert...
Saved in:
Main Authors: | , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2017
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4707 https://ink.library.smu.edu.sg/context/sis_research/article/5710/viewcontent/Classification_based_parameter_icfem17_av.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-5710 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-57102020-03-26T07:54:31Z Classification-based parameter synthesis for parametric timed automata LI, Jiaying SUN, Jun GAO, Bo ANDRE, Étienne Parametric timed automata are designed to model timed systems with unknown parameters, often representing design uncertainties of external environments. In order to design a robust system, it is crucial to synthesize constraints on the parameters, which guarantee the system behaves according to certain properties. Existing approaches suffer from scalability issues. In this work, we propose to enhance existing approaches through classification-based learning. We sample multiple concrete values for parameters and model check the corresponding non-parametric models. Based on the checking results, we form conjectures on the constraint through classification techniques, which can be subsequently confirmed by existing model checkers for parametric timed automata. In order to limit the number of model checker invocations, we actively identify informative parameter values so as to help the classification converge quickly. We have implemented a prototype and evaluated our idea on 24 benchmark systems. The result shows our approach can synthesize parameter constraints effectively and thus improve parametric verification. 2017-11-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4707 info:doi/10.1007/978-3-319-68690-5_15 https://ink.library.smu.edu.sg/context/sis_research/article/5710/viewcontent/Classification_based_parameter_icfem17_av.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Automata theory Formal methods Software engineering Time sharing systems Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Automata theory Formal methods Software engineering Time sharing systems Software Engineering |
spellingShingle |
Automata theory Formal methods Software engineering Time sharing systems Software Engineering LI, Jiaying SUN, Jun GAO, Bo ANDRE, Étienne Classification-based parameter synthesis for parametric timed automata |
description |
Parametric timed automata are designed to model timed systems with unknown parameters, often representing design uncertainties of external environments. In order to design a robust system, it is crucial to synthesize constraints on the parameters, which guarantee the system behaves according to certain properties. Existing approaches suffer from scalability issues. In this work, we propose to enhance existing approaches through classification-based learning. We sample multiple concrete values for parameters and model check the corresponding non-parametric models. Based on the checking results, we form conjectures on the constraint through classification techniques, which can be subsequently confirmed by existing model checkers for parametric timed automata. In order to limit the number of model checker invocations, we actively identify informative parameter values so as to help the classification converge quickly. We have implemented a prototype and evaluated our idea on 24 benchmark systems. The result shows our approach can synthesize parameter constraints effectively and thus improve parametric verification. |
format |
text |
author |
LI, Jiaying SUN, Jun GAO, Bo ANDRE, Étienne |
author_facet |
LI, Jiaying SUN, Jun GAO, Bo ANDRE, Étienne |
author_sort |
LI, Jiaying |
title |
Classification-based parameter synthesis for parametric timed automata |
title_short |
Classification-based parameter synthesis for parametric timed automata |
title_full |
Classification-based parameter synthesis for parametric timed automata |
title_fullStr |
Classification-based parameter synthesis for parametric timed automata |
title_full_unstemmed |
Classification-based parameter synthesis for parametric timed automata |
title_sort |
classification-based parameter synthesis for parametric timed automata |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2017 |
url |
https://ink.library.smu.edu.sg/sis_research/4707 https://ink.library.smu.edu.sg/context/sis_research/article/5710/viewcontent/Classification_based_parameter_icfem17_av.pdf |
_version_ |
1770574985255976960 |