Building Deductive Proofs of LTL Properties for Iteratively Refined Systems

Modern software development processes are evolving from sequential to increasingly agile and incremental paradigms. Verification, unavoidable step of a correct software production, cannot get left behind by this quickly changing practice. Advances in verification techniques have been considerable in the past years, and feasibility has been achieved on always greater systems. Nevertheless, we believe that verification and modern development processes are still not going at the same pace in terms of incrementality. Classical verification algorithms are applied when a complete specification of the model is available, and several development costs and efforts have been already spent. Today more than ever, the description of a system changes continuously during the phase of analysis, asking for periodical adjustments in its specifications. Various parts are often only sketched awaiting further enrichment, which is sometimes delegated to third parties. The classical scenario is, therefore, not applicable anymore: it becomes essential to come up with light iterative methods of verification that can be applied also to incomplete models at each stage of the design and development phases, contributing more incisively to developers choices. With particular focus on two main verification techniques, model checking and deductive verification, we study a way integrating them into this incremental context. The idea is to supply each step of the design phase with a way to prove behaviors of incomplete systems or only single components. Step-wise model checking can be augmented by a simple incremental deductive system generator that justifies why the system meets some requested temporal specification. This kind of infrastructure can bring a useful contribution in cases and refinements where safety, starvation or liveness are critical, and, in general, guide the choices of the developer that faces different designs. The main idea is to combine two approaches presented in literature: we would like to exploit a procedure of model checking that supports incompletely specified systems and we study a mechanism to build deductive proofs using information gathered during model checking. This thesis deals with the construction of these incremental deductive proofs of linear temporal logic properties in incomplete systems that are completed progressively when the system gets refined.