Boosting the Reuse of Formal Specifications

Advances in theorem proving have enabled the emergence of a variety of formal developments that, over the years, have resulted in large corpuses of formalizations. For example, the NASA PVS Library is a collection of 55 formal developments written in the Prototype Verification System (PVS) over a pe...

Descripción completa

Guardado en:

Detalles Bibliográficos
Publicado:	2018
Materias:	Algebra Computer circuits Formal specification NASA Reusability Specification languages Algebraic specifications Formal definition Formal Description Formal development Formal systems Prototype verification systems Universal algebra Theorem proving
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v10895LNCS_n_p477_Moscato http://hdl.handle.net/20.500.12110/paper_03029743_v10895LNCS_n_p477_Moscato
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_03029743_v10895LNCS_n_p477_Moscato
record_format	dspace
spelling	paper:paper_03029743_v10895LNCS_n_p477_Moscato2023-06-08T15:28:16Z Boosting the Reuse of Formal Specifications Algebra Computer circuits Formal specification NASA Reusability Specification languages Algebraic specifications Formal definition Formal Description Formal development Formal systems Prototype verification systems Universal algebra Theorem proving Advances in theorem proving have enabled the emergence of a variety of formal developments that, over the years, have resulted in large corpuses of formalizations. For example, the NASA PVS Library is a collection of 55 formal developments written in the Prototype Verification System (PVS) over a period of almost 30 years and containing more than 28000 proofs. Unfortunately, the simple accumulation of formal developments does not guarantee their reusability. In fact, in formal systems with very expressive specification languages, it is often the case that a particular conceptual object is defined in different ways. This paper presents a technique to establish sound connections between formal definitions. Such connections support the possibility of (partial) borrowing of proved results from one formal description into another, improving the reusability of formal developments. The technique is described using concepts from the field of universal algebra and algebraic specification. The technique is illustrated with concrete examples taken from formalizations available in the NASA PVS Library. © 2018, Springer International Publishing AG, part of Springer Nature. 2018 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v10895LNCS_n_p477_Moscato http://hdl.handle.net/20.500.12110/paper_03029743_v10895LNCS_n_p477_Moscato
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Algebra Computer circuits Formal specification NASA Reusability Specification languages Algebraic specifications Formal definition Formal Description Formal development Formal systems Prototype verification systems Universal algebra Theorem proving
spellingShingle	Algebra Computer circuits Formal specification NASA Reusability Specification languages Algebraic specifications Formal definition Formal Description Formal development Formal systems Prototype verification systems Universal algebra Theorem proving Boosting the Reuse of Formal Specifications
topic_facet	Algebra Computer circuits Formal specification NASA Reusability Specification languages Algebraic specifications Formal definition Formal Description Formal development Formal systems Prototype verification systems Universal algebra Theorem proving
description	Advances in theorem proving have enabled the emergence of a variety of formal developments that, over the years, have resulted in large corpuses of formalizations. For example, the NASA PVS Library is a collection of 55 formal developments written in the Prototype Verification System (PVS) over a period of almost 30 years and containing more than 28000 proofs. Unfortunately, the simple accumulation of formal developments does not guarantee their reusability. In fact, in formal systems with very expressive specification languages, it is often the case that a particular conceptual object is defined in different ways. This paper presents a technique to establish sound connections between formal definitions. Such connections support the possibility of (partial) borrowing of proved results from one formal description into another, improving the reusability of formal developments. The technique is described using concepts from the field of universal algebra and algebraic specification. The technique is illustrated with concrete examples taken from formalizations available in the NASA PVS Library. © 2018, Springer International Publishing AG, part of Springer Nature.
title	Boosting the Reuse of Formal Specifications
title_short	Boosting the Reuse of Formal Specifications
title_full	Boosting the Reuse of Formal Specifications
title_fullStr	Boosting the Reuse of Formal Specifications
title_full_unstemmed	Boosting the Reuse of Formal Specifications
title_sort	boosting the reuse of formal specifications
publishDate	2018
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v10895LNCS_n_p477_Moscato http://hdl.handle.net/20.500.12110/paper_03029743_v10895LNCS_n_p477_Moscato
_version_	1768544365259522048

Boosting the Reuse of Formal Specifications

Ejemplares similares