En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir árboles binarios en Isabelle/HOL y cómo demostrar sus propiedades.
La correspondiente teoría Isabelle/HOL se muestra a continuación
Read More “RA2013: Razonamiento sobre árboles binarios con Isabelle/HOL”
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha comentado las soluciones de la 5ª relación de ejercicios cuyo objetivo es automáticamente con Isabelle/HOL propiedades de programas de cuantificadores sobre listas.
Los ejercicios y sus soluciones se muestran a continuación
Read More “RA2013: Ejercicios de cuantificadores sobre listas con Isabelle/HOL”
En la primera parte de la clase de hoy del curso Lógica Informática se estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra G que no tenga cuantificadores, que esté en forma normal conjuntiva y que sea equisatisfacible con F (es decir, que G es satisfacible precisamente si lo es F). Con dicho procedimiento se calcula la forma normal de Skolem. A partir de las formas se Skolem se obtienen las formas clausales.
En la segunda parte se ha presentado la resolución en la lógica de primer orden como ampliación del presentado en el tema 5 para la lógica proposicional.
Las principales diferencias se encuentran en la unificación, separación de variables y factorización.
Como tarea pendientes se propone la resolución de los ejercicios de los temas 10 y 12 del libro de ejercicios.
Las transparencias de la primera parte son las del tema 10
Read More “LI2013 Resolución en lógica de primer orden”
En la tesis doctoral Mechanical verification of parameterized real-time systems se presenta un marco para la verificación formal en Isabelle/HOL sistemas en tiempo real parametrizados.
Su autor es Thomas Göthel (de la Universidad Técnica de Berlín).
Su resumen es
Real-time systems often have to be able to cope with an unbounded number of components. For example, a real-time operating system scheduler manages arbitrarily many threads or a bus system copes with arbitrarily many connected devices. Such systems can be characterized as parameterized systems. The number of (homogeneous) components is the parameter of these systems. This makes their formal verification hard because standard verification techniques for finite system models (for example model checking) can be employed directly only for instances of the system. There exist several approaches for the (automatic) verification of special sub-classes of (mostly untimed) parameterized systems. However, approaches or tools that enable the comprehensive and mechanical verification of parameterized real-time systems with complex system topologies are still missing.
In this thesis, we overcome this problem by providing a framework for the mechanical, comprehensive, and semi-automatic verification of parameterized real-time systems. At its core we employ the process calculus Timed CSP, which is well-suited to describe the functional behavior as well as the non-functional timing behavior of systems. Our main contribution is threefold: First, we have developed a formalization of the operational semantics of Timed CSP together with notions of bisimulation equivalences in the Isabelle/HOL theorem prover. Second, in order to specify (timing) properties of systems, we provide a (mechanized) timed extension of Hennessy-Milner logic. Together with our formalization of Timed CSP and corresponding bisimulations, this enables the comprehensive and mechanical verification of possibly infinite (parameterized) real-time systems in a modular fashion. In particular, by providing both bisimulation and property based verification, we allow the developer to divide the verification problem into subproblems, which eases verification significantly. At the same time, the theorem prover ensures that no corner cases can be overlooked and all proofs are guaranteed to be correct. Finally, we support the development process of such systems with the integration of automatic verification tools. To this end, we have enriched our framework with transformation engines with which (finite) Timed CSP specifications can be transformed to a discrete dialect of CSP and to UPPAAL timed automata. By this, the FDR2 refinement checker and the UPPAAL tool suite can be used to explore and verify finite instances automatically. Thus, possible design flaws can be detected and corrected early in the development cycle and prior to the relatively time-consuming task of interactive theorem proving.
We show the applicability of our framework using the case study of a parameterized real-time operating system scheduler. Thereby, we demonstrate the benefits of the proposed mapping of Timed CSP to automatically analyzable languages. Furthermore, we show the effectiveness of our theorem proving approach for the comprehensive verification of parameterized real-time systems.
The motivation for our work comes from the observation that, due to their increasing complexity, embedded systems are often built atop trusted cores such as bus systems and real-time operating systems. Their correct functioning thus heavily depends on the correctness of the underlying cores. In the area of safety-critical embedded real-time systems, simulation and testing are not sufficient because they cannot ensure the absence of critical errors. Formal verification tackles this problem. To be of practical relevance, however, formal verification techniques should be mechanized and automatized as far as possible. The mechanization comes with the additional benefit of precluding verification faults as they can occur in hand-written proofs. Our case study forms an important core part of many safety-critical systems. In summary, we show how such cores can be mechanically verified and how their development can be supported with the help of automatic verification tools.
Se ha publicado un artículo de razonamiento formalizado en Coq sobre coindución titulado Moessner’s theorem: an exercise in coinductive reasoning in Coq.
Sus autores son
Su resumen es
Moessner’s Theorem describes a construction of the sequence of powers (1ⁿ, 2ⁿ, 3ⁿ,…), by repeatedly dropping and summing elements from the sequence of positive natural numbers. The theorem was presented by Moessner in 1951 without a proof and later proved and generalized in several directions. More recently, a coinductive proof of the original theorem was given by Niqui and Rutten. We present a formalization of their proof in the Coq proof assistant. This formalization serves as a non-trivial illustration of the use of coinduction in Coq. In the process of formalizing the original proof we discovered that Long and Salié’s generalization of Moessner’s Theorem could also be proved using (almost) the same bisimulation.
El trabajo se presentó en el seminario del COIN (Coalgebra in the Netherlands) . Las transparencias de la presentación se encuentran aquí.
El código de las correspondientes teorías en Coq se encuentra aquí.