PVS

Se ha publicado un artículo de razonamiento formalizado en PVS sobre concurrencia titulado Mutual exclusion by four shared bits with not more than quadratic complexity.

Su autor es Wim H. Hesselink (de la Universidad de Groninga, Países Bajos).

Su resumen es

For years, the mutual exclusion algorithm of Lycklama and Hadzilacos (1991) was the optimal mutual exclusion algorithm with the first-come-first-served property, with a minimal number of (non-atomic) communication variables (5 bits per thread). Recently, Aravind published an improvement of it, which uses 4 bits per threads and has simplified waiting conditions. This algorithm is extended here with fault tolerance, and it is verified by assertional methods, using the proof assistant PVS. Progress is proved by means of UNITY logic. The paper proposes a new measure of concurrent time complexity, and proves that the concurrent complexity for throughput of the present algorithm is not more than quadratic in the number of threads.

El código de las correspondientes teorías en PVS se encuentra aquí.

Se ha publicado un artículo de razonamiento formalizado en PVS titulado Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems

Sus autores son Anthony Narkawicz, César Muñoz y Aaron M. Dutle (del Formal Methods group en el NASA Langley Research Center).

Su resumen es

Sturm’s theorem is a well-known result in real algebraic geometry that provides a function that computes the number of roots of a univariate polynomial in a semi-open interval, not counting multiplicity. A generalization of Sturm’s theorem is known as Tarski’s theorem, which provides a linear relationship between functions known as Tarski queries and cardinalities of certain sets. The linear system that results from this relationship is in fact invertible and can be used to explicitly count the number of roots of a univariate polynomial on a set defined by a system of polynomial relations. This paper presents a formalization of these results in the PVS theorem prover, including formal proofs of Sturm’s and Tarski’s theorems. These theorems are at the basis of two decision procedures, which are implemented as computable functions in PVS. The first, based on Sturm’s theorem, determines satisfiability of a single polynomial relation over an interval. The second, based on Tarski’s theorem, determines the satisfiability of a system of polynomial relations over the real line. The soundness and completeness properties of these decision procedures are formally verified in PVS. The procedures and their correctness properties enable the implementation of PVS strategies for automatically proving existential and universal statements on polynomial systems. Since the decision procedures are formally verified in PVS, the soundness of the strategies depends solely on the internal logic of PVS rather than on an external oracle.

El trabajo se publicará en el Journal of Automated Reasoning.

El código de las correspondientes teorías en PVS del teorema de Sturm se encuentra aquí y el del teorema de Tarski aquí.

Se ha publicado un artículo de verificación formal en PVS sobre multi agentes titulado Formal modeling and verification of multi-agent system architecture.

Sus autores son

• Ling Yuan (de la Huazhong University of Science and Technology, Wuhan, China) y
• Ping Fan (de la Hubei University of Science and Technology, Hubei, China).

Su resumen es

In a multi-agent system, the multiple distributed intelligent agents interact with each other to solve problems. To guide the development of multi-agent system, the multi-agent system architecture would provide a framework. The specific multi- agent system can be customized from the multi-agent system architecture, which does not need to rewrite the construction. In order to satisfy the failure recovery property of multi-agent system, we propose dependable multi-agent system architecture with fault tolerant mechanisms. The PVS formal language is used to build a system architecture, which can provide common patterns and idioms to the system developers. In order to satisfy the reliability requirements, the powerful PVS theorem prover can be used to analyze the high reliability property of the proposed architecture.

El trabajo se ha presentado en la 2013 AASRI Conference on Parallel and Distributed Computing and Systems.

Se ha publicado un artículo de verificación formal con PVS titulado Applications of real number theorem proving in PVS.

Sus autores son

• Hanne Gottliebsen (Queen Mary University of London),
• Ruth Hardy (University of St Andrews),
• Olga Lightfoot (Queen Mary University of London) y
• Ursula Martin (Queen Mary University of London).

Su resumen es

Real number theorem proving has many uses, particularly for verification of safety critical systems and systems for which design errors may be costly. We discuss a chain of developments building on real number theorem proving in PVS. This leads from the verification of aspects of an air traffic control system, through work on the integration of computer algebra and automated theorem proving to a new tool, NRV, first presented here that builds on the capabilities of Maple and PVS to provide a verified and automatic analysis of Nichols plots. This automates a standard technique used by control engineers and greatly improves assurance compared with the traditional method of visual inspection of the Nichols plots.