Abstract:
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.
Registro:
Documento: |
Conferencia
|
Título: | Modal logic as a design notation |
Autor: | Areces, C.; Felder, M.; Hirsch, D.; Yankelevich, D.; ACM Special Interest Group on Software Engineering (SIGSOFT) |
Filiación: | Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina
|
Palabras clave: | 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ño: | 1998
|
Página de inicio: | 150
|
Página de fin: | 152
|
Título revista: | 9th International Workshop on Software Specification and Design, IWSSD 1998
|
Título revista abreviado: | Proc. Int. Workshop Softw. Specification and Design, IWSSD
|
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08186843_v_n_p150_Areces |
Referencias:
- Agustí, J., Robertson, D., Puigsegur, J., Grasp: A graphical specification language for the preliminary specification of logic programs (1995) Technical Report, , Institut d'Investigació en Intelligència Artificial (CSIC)
- Allen, R., Garlan, D., Formalizing architectural connection (1994) International Conference on Software Engineering, , May
- Areces, C., Hirsch, D., (1996) Modal Logic As A Software Engineering Tool TR 96-0004, , http://www.dc.uba.ar, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales. Dep. de Computación
- Bernhard, S., Tiziana, M., Automatic synthesis of design plans in metaframe (1996) Technical Report MIP- 9610, , Universität Passau. Fakultät für Mathematik und Informatik
- Clarke, E., Emerson, E., Sistla, A., Automatic verification of finite-state concurrent systems using temporal logic specifications (1986) ACM Transactions on Programming Languages and Systems, 8, p. 2
- Cosens, M., Mendelzon, A., Ryman, A., Visualizing and quering software structures (1992) ICSE'92 Proceedings of the 14th International Conference on Software Engineering
- Garlan, D., Shaw, M., An introduction to software architecture (1993) Advances in Software Engineering and Knowledge Engineering, 1
- Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S., Symbolic model checking for real-time systems (1994) Information and Computation, 111 (2), pp. 193-244. , June
- Maibaum, T., Sadler, M., Veloso, P., Logical speci fication and implementation (1984) Lecture Notes in Computer Science, 18
- Paul, S., Prakash, A., A query algebra for program databases (1995) IEEE Transactions on Software Engineering, 22, p. 3. , March
- Perry, D., Software interconnection models (1987) Proceedings of the 9th International Conference on Software Engineering, pp. 61-69. , Monterey, California, March
- Pnueli, A., The temporal logic of programs (1977) Proceedings of the 18th. Annual Symposium on the Foundations of Computer Science, , New York, IEEEA4 - ACM Special Interest Group on Software Engineering (SIGSOFT)
Citas:
---------- APA ----------
Areces, C., Felder, M., Hirsch, D., Yankelevich, D. & ACM Special Interest Group on Software Engineering (SIGSOFT)
(1998)
. Modal logic as a design notation. 9th International Workshop on Software Specification and Design, IWSSD 1998, 150-152.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08186843_v_n_p150_Areces [ ]
---------- CHICAGO ----------
Areces, C., Felder, M., Hirsch, D., Yankelevich, D., ACM Special Interest Group on Software Engineering (SIGSOFT)
"Modal logic as a design notation"
. 9th International Workshop on Software Specification and Design, IWSSD 1998
(1998) : 150-152.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08186843_v_n_p150_Areces [ ]
---------- MLA ----------
Areces, C., Felder, M., Hirsch, D., Yankelevich, D., ACM Special Interest Group on Software Engineering (SIGSOFT)
"Modal logic as a design notation"
. 9th International Workshop on Software Specification and Design, IWSSD 1998, 1998, pp. 150-152.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08186843_v_n_p150_Areces [ ]
---------- VANCOUVER ----------
Areces, C., Felder, M., Hirsch, D., Yankelevich, D., ACM Special Interest Group on Software Engineering (SIGSOFT) Modal logic as a design notation. Proc. Int. Workshop Softw. Specification and Design, IWSSD. 1998:150-152.
Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08186843_v_n_p150_Areces [ ]