Software Engineering with the B Method

David DéharbeAnamaria Martins Moreira

By Integrating specification, verification, refinement and synthesis in a single formalism, the B Method provides an effective process for code generation based on the best practices of formal methods in software engineering. An interesting characteristic of B is that it has been devised to attend the needs of its final users and its supporting tools have been developed with the help of industrial groups. Its perfecting and availability have been recently the target of academic research. The tutorial will approach the mathematical foundations of the B method (set theory, first order logic and calculus of generalized substitutions). After that the main steps of the method will be presented: from specification to code generation. Examples will be used to illustrate the main syntactical constructs of B notation. The production and the verification of proof obligations, that establish the correctness of artifacts will be detailed. Tool support for final users will also be discussed.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: