Formal Analysis & Verification of Timed Programs

In recent years, we are witnessing a continuous increase in distributed applications. With the rising of cloud-computing, developers need to consider a new spectrum of problems and domains. A particular domain of such problems is the time domain. For instance, developers use time to implement time frames when external events are expected to occur, to set execution timeouts, or to schedule events that occur periodically. Developers mainly use testing to attest the quality of the programs. However, due to the nature of time, it is hard to provide tests that exhaustively stress the program to detect time-related errors. Another technique to build confidence in the correctness of the program is by using formal methods. Formal methods provide a mathematical methodology to specify, develop, and verify software systems, but they have their limitations. They are usually complex, require a mathematical background, and involve the human. The latter is becoming a huge drawback for the application of formal methods. Traditional and contemporary methods in software evolution and maintenance are moving toward automated pipelines. These pipelines try to automate software development activities starting from building and testing to deploying the system to the customers. This way, developers can focus only on writing code. The emerging practice is to use a Continuous Integration pipeline, where software is compiled, tested, and build automatically. Approaches that involve the human do not fit into this methodology. Furthermore, existing research that tries to close this gap and provide more formal approaches to build confidence in the quality of programs does not consider time as first class citizen domain. They only retain time as a sequence of events that can happen during the execution of a program in a tree-like structure. This thesis presents a set of approaches to automatically improve, discover, and repair errors in implementing time properties of software systems. First, we present a time semantics that enables the reasoning on the influence over the time domain of each statement of a program. Then, we use the time semantics to develop multiple approaches that aid developers to automatically identify flaws in their software systems. First, we propose an approach that automatically extracts timed automata, a formal model that describes the time behavior of programs. The extracted timed automata are amenable to the verification of time properties and they can be used as documentation of the implemented time behavior of the software system. Second, we use the time semantics to encode a program into a set of Satisfiability Modulo Theories problems. If a problem cannot be solved, our approach identifies an execution path in the program that triggers an undesirable time behavior. Then, we refine the time semantics providing a Time Type System that automatically infers time types for integer variables. This additional information is used to automatically remove errors in the source code. Finally, we provide an approach to encode a monitor inside the executable of a program that protects its execution to enter in a wrong state. Furthermore, it is able to resume the expected execution behavior when an error is identified during the runtime. We have validated the applicability and effectiveness of our approaches with open source projects and mathematical proofs. We demonstrated that the extracted timed automata can be used to identify errors in the code as well as to certify that a patch removes such errors. Furthermore, developers indicated the usefulness of our approaches to detect time related errors in the source code. They confirmed the existence of our reported errors that were automatically discovered with our approach. Moreover, the patches generated by our automatic repair approach have been accepted by three different open source projects, removing 24 errors in total. Finally, our approach to protect the runtime of a program showed that it is able to automatically resume a correct execution behavior for 84\% of the identified errors, while introducing a median runtime overhead of 119ms.