BENDÍK, Jaroslav, Nikola BENEŠ, Jiří BARNAT a Ivana ČERNÁ. Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis. In Rocco De Nicola, Eva K{\"{u}}hn. Software Engineering and Formal Methods - 14th International Conference, SEFM 2016. Berlin: Lecture Notes in Computer Sciences in Computer Science, 9763, 2016, s. 121-136. ISBN 978-3-319-41590-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-41591-8_9.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis
Autoři BENDÍK, Jaroslav (203 Česká republika, garant, domácí), Nikola BENEŠ (203 Česká republika, domácí), Jiří BARNAT (203 Česká republika, domácí) a Ivana ČERNÁ (203 Česká republika, domácí).
Vydání Berlin, Software Engineering and Formal Methods - 14th International Conference, SEFM 2016, od s. 121-136, 16 s. 2016.
Nakladatel Lecture Notes in Computer Sciences in Computer Science, 9763
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
WWW URL
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/16:00090470
Organizační jednotka Fakulta informatiky
ISBN 978-3-319-41590-1
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-41591-8_9
UT WoS 000386263500009
Klíčová slova anglicky Requirements analysis Formal verification Safety analysis
Štítky firank_B
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 13. 5. 2020 19:19.
Anotace
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.
Návaznosti
MUNI/A/0945/2015, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
7H13001, projekt VaVNázev: Critical System Engineering Acceleration (Akronym: CRYSTAL (MSMT))
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Critical System Engineering Acceleration
VytisknoutZobrazeno: 9. 6. 2024 07:26