From boxes to worlds

In this paper we show an innovative way to represent graphic designs 01 systems and to verify design properties. The graphic designs are thought as models of an extended modal logic; and the methods used to verify properties are developed from techniques typical of classic modal logic, extended to c...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Hirsch, Dan Francisco, Areces, Carlos Eduardo
Formato: Objeto de conferencia
Lenguaje:Inglés
Publicado: 1995
Materias:
Ciencias Informáticas
Software Design
Graphic Languages
Modal Logics
Formal Verification
Languages
Software
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/24296
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-24296
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 Design
Graphic Languages
Modal Logics
Formal Verification
Languages
Software
spellingShingle Ciencias Informáticas
Software Design
Graphic Languages
Modal Logics
Formal Verification
Languages
Software
Hirsch, Dan Francisco
Areces, Carlos Eduardo
From boxes to worlds
topic_facet Ciencias Informáticas
Software Design
Graphic Languages
Modal Logics
Formal Verification
Languages
Software
description In this paper we show an innovative way to represent graphic designs 01 systems and to verify design properties. The graphic designs are thought as models of an extended modal logic; and the methods used to verify properties are developed from techniques typical of classic modal logic, extended to cover the differences in the underlying formalism. We present the procedures orlogical tools to derive the modal model associated to a given design, the filtration of models and the construction 01 modal descriptions. A higher level of abstraction is obtained in this way, and it lets us reason over designs in a strictly formal manner. The power of formal provability is also achieved. We use a working example to show how our tools help to veri1y properties 01 design like the detection of cycles (self loops).
format Objeto de conferencia
Objeto de conferencia
author Hirsch, Dan Francisco
Areces, Carlos Eduardo
author_facet Hirsch, Dan Francisco
Areces, Carlos Eduardo
author_sort Hirsch, Dan Francisco
title From boxes to worlds
title_short From boxes to worlds
title_full From boxes to worlds
title_fullStr From boxes to worlds
title_full_unstemmed From boxes to worlds
title_sort from boxes to worlds
publishDate 1995
url http://sedici.unlp.edu.ar/handle/10915/24296
work_keys_str_mv AT hirschdanfrancisco fromboxestoworlds
AT arecescarloseduardo fromboxestoworlds
bdutipo_str Repositorios
_version_ 1764820466916130816

Ejemplares similares