Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

11-2017

Abstract

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.

Keywords

Automata theory, Formal methods, Software engineering, Time sharing systems

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Formal methods and software engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17: Proceedings

Volume

10610

First Page

243

Last Page

261

ISBN

9783319686899

Identifier

10.1007/978-3-319-68690-5_15

Publisher

Springer

City or Country

Cham

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1007/978-3-319-68690-5_15

Download

Share

COinS