ASM-based formal design of an adaptivity component for a Cloud system

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F16%3A10331996" target="_blank" >RIV/00216208:11320/16:10331996 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/s00165-016-0371-5" target="_blank" >http://dx.doi.org/10.1007/s00165-016-0371-5</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/s00165-016-0371-5" target="_blank" >10.1007/s00165-016-0371-5</a>

Jazyk výsledku

angličtina

Název v původním jazyce

ASM-based formal design of an adaptivity component for a Cloud system

Popis výsledku v původním jazyce

The request of formal methods for the specification and analysis of distributed systems is nowadays increasing, especially when considering the development of Cloud systems and Web applications. This is due to the fact that modeling languages currently used in these areas have informal definitions and ambiguous semantics, and therefore their use may be unreliable. Thanks to their mathematical foundation, formal methods can guarantee rigorous system design, leading to precise models where requirements can be validated and properties can be assured, already at the early stages of the system development. In this paper, we present a rigorous engineering process for distributed systems, based on the Abstract State Machines (ASM) formal method. We rely on the foundational notions of ASM ground model and model refinement to obtain a precise model for a client-server application for Cloud systems. This application has been proposed to tackle the problem of making Cloud services usable to different end-devices by adapting on-the-fly the content coming from the Cloud to the different devices contexts. The ASM-based modeling process is supported by a number of validation and verification activities that have been exploited on the component under development to guarantee consistency, correctness, and reliability properties.

Název v anglickém jazyce

ASM-based formal design of an adaptivity component for a Cloud system

Popis výsledku anglicky

The request of formal methods for the specification and analysis of distributed systems is nowadays increasing, especially when considering the development of Cloud systems and Web applications. This is due to the fact that modeling languages currently used in these areas have informal definitions and ambiguous semantics, and therefore their use may be unreliable. Thanks to their mathematical foundation, formal methods can guarantee rigorous system design, leading to precise models where requirements can be validated and properties can be assured, already at the early stages of the system development. In this paper, we present a rigorous engineering process for distributed systems, based on the Abstract State Machines (ASM) formal method. We rely on the foundational notions of ASM ground model and model refinement to obtain a precise model for a client-server application for Cloud systems. This application has been proposed to tackle the problem of making Cloud services usable to different end-devices by adapting on-the-fly the content coming from the Cloud to the different devices contexts. The ASM-based modeling process is supported by a number of validation and verification activities that have been exploited on the component under development to guarantee consistency, correctness, and reliability properties.

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2016

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 periodika

Formal Aspects of Computing

ISSN

0934-5043

e-ISSN

—

Svazek periodika

28

Číslo periodika v rámci svazku

4

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

29

Strana od-do

567-595

Kód UT WoS článku

000380112600003

EID výsledku v databázi Scopus

2-s2.0-84963682810