Bounded Model Checking de programas imperativos

Abstract

A detecção de erros em sistemas computacionais, em particular em sistemas críticos, é uma tarefa fundamental para garantir o correcto funcionamento dos sistemas e, por este motivo, a verificação formal é um elemento primordial no desenvolvimento de sistemas computacionais. Muitas das técnicas de verificação formal de sistemas computacionais são baseadas em Model Checking (MC). O MC é uma técnica de verificação automática que assenta na modelação de sistemas através de máquinas de estados finitas e na especificação das propriedades pretendidas para os sistemas através de fórmulas lógicas (tipicamente em alguma lógica temporal). O Bounded Model Checking (BMC) é uma técnica de MC que restringe a exploração do espaço de estados até um determinado comprimento (bound) dos traços de execução, como forma de evitar o problema da explosão de estados do MC tradicional. Por isso, as propriedades garantidas por este método aplicam-se apenas à execução até um certo bound. Nesta tese focamos no Bounded Model Checking aplicado a software (BMCsw), no contexto de linguagens imperativas, cujas ideias essenciais passam por usar asserts ao longo dos programas, como forma de declarar propriedades que devem ser satisfeitas por qualquer execução desses programas, e por expandir ciclos, escrevendo-os a custa de construções if then else. O BMCsw pode ser visto como uma sequência de transformações ao nível do programa e por uma transformação final que produz uma fórmula lógica, cuja validade garante a correcção do programa. Especificamente, nesta tese de mestrado estudamos a validade do método BMC no contexto de programas While com asserts. Por um lado, estabelecemos uma semântica operacional para uma linguagem While com asserts, que designamos por Whileassert, onde o estado de erro desempenha um papel fundamental. Por outro lado, estudamos propriedades desta linguagem e, com base nestas propriedades, provamos a validade (correcção e completude) da transformação final envolvida no método BMCsw. O BMC apresenta problemas de escalabilidade que são amenizados pelo actual poder de decisão dos Satisfiability problem (SAT) solvers. Durante esta tese foi desenvolvida uma ferramenta de software que implementa o método BMC para a linguagem minimalista Whileassert. Dado um programa Whileassert, esta ferramenta produz uma fórmula lógica, codificando as propriedades do programa, cuja validade garante a correcção do programa. A validade da fórmula é então avaliada com recurso ao SAT solver Z3.

Error detection in computer systems, particularly in critical systems, is a key task to ensure the correct functioning of systems and, therefore, formal verification is a key element in the development of computer systems. Many of the techniques of formal verification of computer systems are based on Model Checking (MC). MC is an automatic verification technique which is based on using finite state machines to model systems, and on the specification of the desired properties for the systems by logical formulas (typically in some temporal logic). Bounded Model Checking (BMC) is a technique of MC that restricts the exploration of the state space up to a certain execution trace length (bound), in order to avoid the problem of state explosion in traditional MC. Therefore, the properties guaranteed by this method apply only to a certain bound enforcement. In this thesis we focus on Bounded Model Checking applied to software (BMCsw), in the context of imperative languages, whose key ideas are to use assertions throughout programs as a way to declare properties that must be satisfied by any execution of these programs, and to expand cycles, rewriting them in terms of the construct if then else. The BMCsw can be seen as a sequence of transformations at the level of the program and a final transformation which produces a logical formula whose validity ensures the correctness of the program. Specifically, in this master thesis we study the validity of the method BMC in the context of While programs with asserts. On the one hand, we establish an operational semantics for a While language with assertions, which we call Whileassert, where the error state plays a key role. On the other hand, we study properties of this language and, based on these properties, we prove the validity (correctness and completeness) involved in the final transformation of the BMCsw method. BMC presents scalability issues that are mitigated by the decision-making power of the current Satis ability problem (SAT) solvers. During this thesis we have developed a software tool that implements the BMC method for the minimal language Whileassert. Given a program Whileassert, this tool produces a logical formula, encoding properties of the program, whose validity ensures the correctness of the program. The validity of the formula is then evaluated using the Z3 SAT solver .