D 2016

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

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

Basic information

Original name

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

Authors

BENDÍK, Jaroslav (203 Czech Republic, guarantor, belonging to the institution), Nikola BENEŠ (203 Czech Republic, belonging to the institution), Jiří BARNAT (203 Czech Republic, belonging to the institution) and Ivana ČERNÁ (203 Czech Republic, belonging to the institution)

Edition

Berlin, Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, p. 121-136, 16 pp. 2016

Publisher

Lecture Notes in Computer Sciences in Computer Science, 9763

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

References:

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/16:00090470

Organization unit

Faculty of Informatics

ISBN

978-3-319-41590-1

ISSN

UT WoS

000386263500009

Keywords in English

Requirements analysis Formal verification Safety analysis

Tags

International impact, Reviewed
Změněno: 13/5/2020 19:19, RNDr. Pavel Šmerk, Ph.D.

Abstract

V originále

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.

Links

MUNI/A/0945/2015, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masaryk University, Category A
7H13001, research and development project
Name: Critical System Engineering Acceleration (Acronym: CRYSTAL (MSMT))
Investor: Ministry of Education, Youth and Sports of the CR