Reseña: Software component design with the B method: a formalization in Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Software component design with the B method: a formalization in Isabelle/HOL.

Sus autores son

  • David Déharbe (del grupo ForAll (Formal Methods and Languages Laboratory) en la UFRN (Universidade Federal do Rio Grande do Norte), Brasil) y
  • Stephan Merz (del grupo VeriDis (Verification of Distributed Systems) en el INRIA Nancy & LORIA, Francia).

Su resumen es

This paper presents a formal development of an Isabelle/HOL theory for the behavioral aspects of artifacts produced in the design of software components with the B method. We first provide a formalization of semantic objects such as labelled transition systems and notions of behavior and simulation. We define an interpretation of the B method using such concepts. We also address the issue of component composition in the B method.

El trabajo se ha presentado en FACS 2015 (12th Intl. Conf. Formal Aspects of Component Software).

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.