Formalization of Invariant Patterns for the Invariant Refinement Method

Result code in 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>
Result on the web
<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>

Result language
angličtina
Original language name
Formalization of Invariant Patterns for the Invariant Refinement Method
Original language description
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.
Czech name
—
Czech description
—

Project
<a href="/en/project/7E12045" target="_blank" >7E12045: Autonomic Service-Component Ensembles</a><br>
Continuities
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

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

Similar results(10)