Artículo

Frias, M.F.; Lopez Pombo, C.G.; Moscato, M.M. "Alloy Analyzer+PVS in the analysis and verification of Alloy specifications" (2007) 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2007). 4424 LNCS:587-601
La versión final de este artículo es de uso interno. El editor solo permite incluir en el repositorio el artículo en su versión post-print. Por favor, si usted la posee enviela a
Consulte la política de Acceso Abierto del editor

Abstract:

This article contains two main contributions. On the theoretical side, it presents a novel complete proof calculus for Alloy. On the applied side we present Dynamite, a tool that combines the semiautomatic theorem prover PVS with the Alloy Analyzer. Dynamite allows one to prove an Alloy assertion from an Alloy specification using PVS, while using the Alloy Analyzer for the automated analysis of hypotheses introduced during the proof process. As a means to assess the usability of the tool, we present a complex case-study based on Zave's Alloy model of addressing for interoperating networks. © Springer-Verlag Berlin Heidelberg 2007.

Registro:

Documento: Artículo
Título:Alloy Analyzer+PVS in the analysis and verification of Alloy specifications
Autor:Frias, M.F.; Lopez Pombo, C.G.; Moscato, M.M.
Ciudad:Braga
Filiación:Department of Computer Science, FCEyN, Universidad de Buenos Aires, Argentina
Palabras clave:Alloy Analyzer; Automated analysis; Interoperating networks; Semiautomatic theorem; Alloy analyzers; Analysis and verifications; Automated analysis; Proof calculus; Theorem provers; Alloys; Computer aided software engineering; Interoperability; Specifications; Verification; Calculations; Complex networks; Software prototyping; Specifications
Año:2007
Volumen:4424 LNCS
Página de inicio:587
Página de fin:601
Handle:http://hdl.handle.net/20.500.12110/paper_03029743_v4424LNCS_n_p587_Frias
Título revista:13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2007)
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4424LNCS_n_p587_Frias

Referencias:

  • Arkoudas, K., Type-ω DPLs (2001) MIT AI Memo, 2001 -27
  • Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M., Integrating Model Checking and Theorem Proving for Relational Reasoning (2003) LNCS, , Proceedings of RelMiCS'03 Relational Methods in Computer Science, Springer
  • Frias, M., Fork Algebras in Algebra, Logic and Computer Science (2002) Series Advances on Logic, , World Scientific Publishing Co
  • Frias, M.F., Haeberer, A.M., Veloso, P.A.S., A Finite Axiomatization for Fork Algebras (1997) Logic Journal of the IGPL, 5 (3), pp. 311-319
  • Frias, M.F., López Pombo, C.G., Aguirre, N., A Complete Equational Calculus for Alloy (2004) Lecture Notes in Computer Science, 3308, pp. 162-175. , Proceedings of Internacional Conference on Formal Engineering Methods ICFEM'04, Seattle, USA, November, Springer-Verlag
  • Frias M.F., López Pombo C.G. and Moscato M.M., Dynamite: Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications, in Proceedings of the First Alloy Workshop (Daniel Jackson and Pamela Zave Eds.), colocated with 14th ACM Symposium on Foundations of Software Engineering, 2006, to appear; Jackson, D., Shlyakhter, I., Sridharan, M., A Micromodularity Mechanism (2001) Proc. ACM SIGSOFT Conf. Foundations of Software Engineering/European Software Engineering Conference (FSE/ESEC '01), , Vienna, September
  • Kong, W., Ogata, K., Seino, T., Futatsugi, K., A Lightweight Integration of Theorem Proving and Model Checking for System Verification Proc. of APSEC'05, , IEEE
  • Maddux, R.D., Pair-Dense Relation Algebras (1991) Transactions of the AMS, 328 (1)
  • Shankar, N., Owre, S., Rushby, J.M., Stringer-Calvert, D.W.J., (1999) PVS Prover Guide, , Computer Science Laboratory, SRI International, Menlo Park, CA, September
  • Shankar, N., Combining Theorem Proving and Model Checking through Symbolic Analysis (2000) LNCS, , Proc. of CONCUR, Springer
  • Zave, P., A Formal Model of Addressing for Interoperating Networks (2005) LNCS, 3582, pp. 318-333. , Proceedings of the Thirteenth International Symposium of Formal Methods Europe, SpringerVerlag

Citas:

---------- APA ----------
Frias, M.F., Lopez Pombo, C.G. & Moscato, M.M. (2007) . Alloy Analyzer+PVS in the analysis and verification of Alloy specifications. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2007), 4424 LNCS, 587-601.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4424LNCS_n_p587_Frias [ ]
---------- CHICAGO ----------
Frias, M.F., Lopez Pombo, C.G., Moscato, M.M. "Alloy Analyzer+PVS in the analysis and verification of Alloy specifications" . 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2007) 4424 LNCS (2007) : 587-601.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4424LNCS_n_p587_Frias [ ]
---------- MLA ----------
Frias, M.F., Lopez Pombo, C.G., Moscato, M.M. "Alloy Analyzer+PVS in the analysis and verification of Alloy specifications" . 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2007), vol. 4424 LNCS, 2007, pp. 587-601.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4424LNCS_n_p587_Frias [ ]
---------- VANCOUVER ----------
Frias, M.F., Lopez Pombo, C.G., Moscato, M.M. Alloy Analyzer+PVS in the analysis and verification of Alloy specifications. Lect. Notes Comput. Sci. 2007;4424 LNCS:587-601.
Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v4424LNCS_n_p587_Frias [ ]