Formalization of Invariant Patterns for the Invariant Refinement Method

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F15%3A10320424" target="_blank" >RIV/00216208:11320/15:10320424 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-15545-6_34" target="_blank" >http://dx.doi.org/10.1007/978-3-319-15545-6_34</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-15545-6_34" target="_blank" >10.1007/978-3-319-15545-6_34</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Formalization of Invariant Patterns for the Invariant Refinement Method

Popis výsledku v původním jazyce

Refining high-level system invariants into lower-level software obligations has been successfully employed in the design of ensemble-based systems. In order to obtain guarantees of design correctness, it is necessary to formalize the invariants in a form amenable to mathematical analysis. This paper provides such a formalization and demonstrates it in the context of the Invariant Refinement Method. The formalization is used to formally define invariant patterns at different levels of abstraction and with respect to different (soft) real-time constraints, and to provide proofs of theorems related to refinement among these patterns.

Název v anglickém jazyce

Formalization of Invariant Patterns for the Invariant Refinement Method

Popis výsledku anglicky

Refining high-level system invariants into lower-level software obligations has been successfully employed in the design of ensemble-based systems. In order to obtain guarantees of design correctness, it is necessary to formalize the invariants in a form amenable to mathematical analysis. This paper provides such a formalization and demonstrates it in the context of the Invariant Refinement Method. The formalization is used to formally define invariant patterns at different levels of abstraction and with respect to different (soft) real-time constraints, and to provide proofs of theorems related to refinement among these patterns.

Druh

C - Kapitola v odborné knize

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/7E12045" target="_blank" >7E12045: Autonomic Service-Component Ensembles</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název knihy nebo sborníku

Software, Services, and Systems

ISBN

978-3-319-15544-9

Počet stran výsledku

17

Strana od-do

602-618

Počet stran knihy

692

Název nakladatele

Springer International Publishing

Místo vydání

Cham

Kód UT WoS kapitoly

—