Alloy Analyzer+PVS in the analysis and verification of Alloy specifications

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 fr...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Frias, M.F., Lopez Pombo, C.G., Moscato, M.M.
Formato: SER
Materias:
Alloy Analyzer
Automated analysis
Interoperating networks
Semiautomatic theorem
Alloy analyzers
Analysis and verifications
Proof calculus
Theorem provers
Alloys
Computer aided software engineering
Interoperability
Specifications
Verification
Calculations
Complex networks
Software prototyping
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v4424LNCS_n_p587_Frias
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:paper_03029743_v4424LNCS_n_p587_Frias
record_format dspace
spelling todo:paper_03029743_v4424LNCS_n_p587_Frias2023-10-03T15:18:59Z Alloy Analyzer+PVS in the analysis and verification of Alloy specifications Frias, M.F. Lopez Pombo, C.G. Moscato, M.M. 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 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. Fil:Frias, M.F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Lopez Pombo, C.G. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. SER info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v4424LNCS_n_p587_Frias
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic 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
spellingShingle 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
Frias, M.F.
Lopez Pombo, C.G.
Moscato, M.M.
Alloy Analyzer+PVS in the analysis and verification of Alloy specifications
topic_facet 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
description 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.
format SER
author Frias, M.F.
Lopez Pombo, C.G.
Moscato, M.M.
author_facet Frias, M.F.
Lopez Pombo, C.G.
Moscato, M.M.
author_sort Frias, M.F.
title Alloy Analyzer+PVS in the analysis and verification of Alloy specifications
title_short Alloy Analyzer+PVS in the analysis and verification of Alloy specifications
title_full Alloy Analyzer+PVS in the analysis and verification of Alloy specifications
title_fullStr Alloy Analyzer+PVS in the analysis and verification of Alloy specifications
title_full_unstemmed Alloy Analyzer+PVS in the analysis and verification of Alloy specifications
title_sort alloy analyzer+pvs in the analysis and verification of alloy specifications
url http://hdl.handle.net/20.500.12110/paper_03029743_v4424LNCS_n_p587_Frias
work_keys_str_mv AT friasmf alloyanalyzerpvsintheanalysisandverificationofalloyspecifications
AT lopezpombocg alloyanalyzerpvsintheanalysisandverificationofalloyspecifications
AT moscatomm alloyanalyzerpvsintheanalysisandverificationofalloyspecifications
_version_ 1807315873277411328

Ejemplares similares