Parametric Systems: Verification and Synthesis

Issue title: Special Issue on The Working Formal Methods Symposium (FROM 2018)

Guest editors: Jetty Kleijn, Laurenţiu Leuştean and Dorel Lucanu

Article type: Research Article

Authors: Sofronie-Stokkermans, Viorica

Affiliations: University Koblenz-Landau, Universitätsstr. 1, D-56070 Koblenz, Germany. sofronie@uni-koblenz.de

Correspondence: [] Address for correspondence: University Koblenz-Landau, Universitätsstr. 1, D-56070 Koblenz, Germany

Abstract: In this paper we study possibilities of using hierarchical reasoning, symbol elimination and model generation for the verification of parametric systems, where the parameters can be constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We analyze the possibility of automatically generating such guarantees in the form of constraints on parameters. We illustrate our methods on several examples.

DOI: 10.3233/FI-2020-1918

Journal: Fundamenta Informaticae, vol. 173, no. 2-3, pp. 91-138, 2020