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...

Full description

Saved in:
Bibliographic Details
Main Authors: LI, Jiaying, SUN, Jun, GAO, Bo, ANDRE, Étienne
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