Formal methods for practical reverse engineering and software verification

Software development processes are committed at producing high quality software system. Traditionally, this goal is reached through systematic testing. This thesis project analyzes the possibility of applying mathematical logic and so-called formal methods into the software development process. In fact software testing has two major limitations with respect to verification by means of software testing: every test can show correctness for one possible behavior, while formal methods verification shows that correctness, if proved, holds for all the executions of the system. Furthermore, testing can be used to stress the system implementation, while formal verification can be done also during earlier stages of software development, when abstract models of the system are first sketched. In this work we present an integrated working environment that aims at guiding the software engineer along some of the most relevant moments of a software system lifetime: its development, its verification, its maintenance up to a complete re-structuring. The core of the proposed environment is the language XAL , a parametric extension of the theory of networks of timed automata. After defining its syntax and semantics, we show a novel cutoff theorem for it, proving that systems that are both parametric and timed can be model checked. We then describe two methodologies: the former helps in restructuring existing applications using XAL , extracting parameterized finite-state models from legacy code. The latter is about conducting a formal verification using XAL and its cutoff theorem, if needed. A few case-studies are described that uses the proposed language and methodologies. These case-studies are real-world software systems analyzed in a joint effort with Computer VAR ITT and BINT, two Italian ITC companies.