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
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 |
| 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 [ ]
