Exploring Architectural Model Checking with Declarative Specifications

In this work we explore the FVS language in the context of architectural behavior model checking. FVS holds desirable characteristics for this particular domain. Its flexible notation enables the possibility of performing behavioral exploration when denoting the properties to be satisfied. In additi...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Asteasuain, Fernando, Tarulla, Francisco
Formato: Objeto de conferencia
Lenguaje:Inglés
Publicado: 2017
Materias:
Ciencias Informáticas
Software Architectures
Model checking
Requirements/Specifications
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/63796
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-63796
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Software Architectures
Model checking
Requirements/Specifications
spellingShingle Ciencias Informáticas
Software Architectures
Model checking
Requirements/Specifications
Asteasuain, Fernando
Tarulla, Francisco
Exploring Architectural Model Checking with Declarative Specifications
topic_facet Ciencias Informáticas
Software Architectures
Model checking
Requirements/Specifications
description In this work we explore the FVS language in the context of architectural behavior model checking. FVS holds desirable characteristics for this particular domain. Its flexible notation enables the possibility of performing behavioral exploration when denoting the properties to be satisfied. In addition, FVS expressive power capable of denoting ω-regular properties is useful to denote behavior in a higher level of abstraction. These are two key activities when specifying and validating a system architecture. Given that FVS specifications can be translated into B¨uchi automata they can be used as input in a validation tool like model checkers. In this sense, we conducted industrial relevant case studies to apply our approach in concrete examples.
format Objeto de conferencia
Objeto de conferencia
author Asteasuain, Fernando
Tarulla, Francisco
author_facet Asteasuain, Fernando
Tarulla, Francisco
author_sort Asteasuain, Fernando
title Exploring Architectural Model Checking with Declarative Specifications
title_short Exploring Architectural Model Checking with Declarative Specifications
title_full Exploring Architectural Model Checking with Declarative Specifications
title_fullStr Exploring Architectural Model Checking with Declarative Specifications
title_full_unstemmed Exploring Architectural Model Checking with Declarative Specifications
title_sort exploring architectural model checking with declarative specifications
publishDate 2017
url http://sedici.unlp.edu.ar/handle/10915/63796
work_keys_str_mv AT asteasuainfernando exploringarchitecturalmodelcheckingwithdeclarativespecifications
AT tarullafrancisco exploringarchitecturalmodelcheckingwithdeclarativespecifications
bdutipo_str Repositorios
_version_ 1764820479297716225

Ejemplares similares