Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři

BENDÍK Jaroslav BENEŠ Nikola BARNAT Jiří ČERNÁ Ivana

Rok publikování 2016
Druh Článek ve sborníku
Konference Software Engineering and Formal Methods - 14th International Conference, SEFM 2016
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://dx.doi.org/10.1007/978-3-319-41591-8_9p://dx.doi.org/10.1007/978-3-319-41591-8_9
Doi http://dx.doi.org/10.1007/978-3-319-41591-8_9
Obor Informatika
Klíčová slova Requirements analysis Formal verification Safety analysis
Popis The motivation for this study comes from various sources such as parametric formal verification, requirements engineering, and safety analysis. In these areas, there are often situations in which we are given a set of configurations and a property of interest with the goal of computing all the configurations for which the property is valid. Checking the validity of each single configuration may be a costly process. We are thus interested in reducing the number of such validity queries. In this work, we assume that the configuration space is equipped with a partial ordering that is preserved by the property to be checked. In such a case, the set of all valid configurations can be effectively represented by the set of all maximum valid (or minimum invalid) configurations w.r.t. the ordering. We show an algorithm to compute such boundary elements. We explain how this general setting applies to consistency and redundancy checking of requirements and to finding minimum cut-sets for safety analysis. We further discuss various heuristics and evaluate their efficiency, measured primarily by the number of validity queries, on a preliminary set of experiments.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.