Modal logic as a design notation

A notation to describe software system designs is given together with the means to verify properties over them. Designs are considered as models of a modal logic. The procedure to derive the modal model associated to a design, the algorithm to check properties over a model, the method to define new...

Descripción completa

Guardado en:
Detalles Bibliográficos
Publicado: 1998
Materias:
Formal logic
Inverse problems
Model checking
Specification languages
Specifications
Design notations
Inverse operators
Method of modeling
Modal models
Model checking algorithm
Property specification language
Prototype tools
Software system designs
Computer circuits
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08186843_v_n_p150_Areces
http://hdl.handle.net/20.500.12110/paper_08186843_v_n_p150_Areces
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_08186843_v_n_p150_Areces
record_format dspace
spelling paper:paper_08186843_v_n_p150_Areces2025-07-30T18:22:27Z Modal logic as a design notation Formal logic Inverse problems Model checking Specification languages Specifications Design notations Inverse operators Method of modeling Modal models Model checking algorithm Property specification language Prototype tools Software system designs Computer circuits A notation to describe software system designs is given together with the means to verify properties over them. Designs are considered as models of a modal logic. The procedure to derive the modal model associated to a design, the algorithm to check properties over a model, the method to define new relations and the method of model filtration are presented. The proposed logic (KPI a poly-modal logic with inverse operators) is used as a property specification language verified through a model checking algorithm. The methods provided proved to be effective and simple to implement. A prototype tool has been developed in SML-NJ covering all functionalities described. 1998 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08186843_v_n_p150_Areces http://hdl.handle.net/20.500.12110/paper_08186843_v_n_p150_Areces
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Formal logic
Inverse problems
Model checking
Specification languages
Specifications
Design notations
Inverse operators
Method of modeling
Modal models
Model checking algorithm
Property specification language
Prototype tools
Software system designs
Computer circuits
spellingShingle Formal logic
Inverse problems
Model checking
Specification languages
Specifications
Design notations
Inverse operators
Method of modeling
Modal models
Model checking algorithm
Property specification language
Prototype tools
Software system designs
Computer circuits
Modal logic as a design notation
topic_facet Formal logic
Inverse problems
Model checking
Specification languages
Specifications
Design notations
Inverse operators
Method of modeling
Modal models
Model checking algorithm
Property specification language
Prototype tools
Software system designs
Computer circuits
description A notation to describe software system designs is given together with the means to verify properties over them. Designs are considered as models of a modal logic. The procedure to derive the modal model associated to a design, the algorithm to check properties over a model, the method to define new relations and the method of model filtration are presented. The proposed logic (KPI a poly-modal logic with inverse operators) is used as a property specification language verified through a model checking algorithm. The methods provided proved to be effective and simple to implement. A prototype tool has been developed in SML-NJ covering all functionalities described.
title Modal logic as a design notation
title_short Modal logic as a design notation
title_full Modal logic as a design notation
title_fullStr Modal logic as a design notation
title_full_unstemmed Modal logic as a design notation
title_sort modal logic as a design notation
publishDate 1998
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08186843_v_n_p150_Areces
http://hdl.handle.net/20.500.12110/paper_08186843_v_n_p150_Areces
_version_ 1840321568271499264

Ejemplares similares