Verificarea şi specificarea formală a produselor software. Posibilităţi de implementare şi dificultăţi

Abstract

Formal specification is concerned with producing an unambiguous set of product specifications so that customer requirements, as well as environmental constraints and design intentions, are correctly reflected, thus reducing the chances of accidental fault injections. The purpose of this article is to describe the formal analyses and verifications based on formal models of program and their expected behavior, as an alternative way for software quality assurance.