D 2012

Reliability analysis in component-based development via probabilistic model checking

BENEŠ, Nikola, Barbora BÜHNOVÁ, Ivana ČERNÁ a Radek OŠLEJŠEK

Základní údaje

Originální název

Reliability analysis in component-based development via probabilistic model checking

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Barbora BÜHNOVÁ (203 Česká republika, garant, domácí), Ivana ČERNÁ (203 Česká republika, domácí) a Radek OŠLEJŠEK (203 Česká republika, domácí)

Vydání

New York, NY, USA, Proceedings of the 15th ACM SIGSOFT symposium on Component Based Software Engineering (CBSE '12), od s. 83-92, 10 s. 2012

Nakladatel

ACM

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Itálie

Utajení

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

Forma vydání

tištěná verze "print"

Kód RIV

RIV/00216224:14330/12:00057593

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4503-1345-2

Klíčová slova anglicky

Reliability; component-based systems; probabilistic model checking; Markov decision processes (MDP)

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 5. 3. 2021 08:34, doc. RNDr. Radek Ošlejšek, Ph.D.

Anotace

V originále

Engineering of highly reliable systems requires support of sophisticated design methods allowing software architects to competently decide between various design alternatives already early in the development process. Architecture-based reliability prediction provides such capability. The formalisms and analytical methods employed by existing approaches are however often limited to a single reliability measure (the probability of failure on demand) and consideration of behavioural uncertainty (focusing on the uncertainty in model parameters, not the behaviour itself). This paper presents a formal reliability assessment approach for component-based systems based on the probabilistic model checking of various reliability-related properties specified in probabilistic linear temporal logic (PLTL). The systems are formalized as Markov decision processes (MDP), which allows software architects to encode behavioural uncertainties into the models in terms of nondeterministic (scheduler-decided) choices in the MDP.

Návaznosti

GAP202/11/0312, projekt VaV
Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)
Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
GD102/09/H042, projekt VaV
Název: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
LA09016, projekt VaV
Název: Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM) (Akronym: ERCIM)
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Účast ČR v European Research Consortium for Informatics and Mathematics
MUNI/A/0914/2009, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Přiložené soubory