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...
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | CONF |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_08186843_v_n_p150_Areces |
| Aporte de: |
| id |
todo:paper_08186843_v_n_p150_Areces |
|---|---|
| record_format |
dspace |
| spelling |
todo:paper_08186843_v_n_p150_Areces2023-10-03T15:39:58Z Modal logic as a design notation Areces, C. Felder, M. Hirsch, D. Yankelevich, D. ACM Special Interest Group on Software Engineering (SIGSOFT) 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. CONF info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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 Areces, C. Felder, M. Hirsch, D. Yankelevich, D. ACM Special Interest Group on Software Engineering (SIGSOFT) 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. |
| format |
CONF |
| author |
Areces, C. Felder, M. Hirsch, D. Yankelevich, D. ACM Special Interest Group on Software Engineering (SIGSOFT) |
| author_facet |
Areces, C. Felder, M. Hirsch, D. Yankelevich, D. ACM Special Interest Group on Software Engineering (SIGSOFT) |
| author_sort |
Areces, C. |
| 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 |
| url |
http://hdl.handle.net/20.500.12110/paper_08186843_v_n_p150_Areces |
| work_keys_str_mv |
AT arecesc modallogicasadesignnotation AT felderm modallogicasadesignnotation AT hirschd modallogicasadesignnotation AT yankelevichd modallogicasadesignnotation AT acmspecialinterestgrouponsoftwareengineeringsigsoft modallogicasadesignnotation |
| _version_ |
1807324599758618624 |