Regression testing of an evolving software system may involve significant challenges. While, there would be a requirement of maximising the probability of finding out if the latest changes to the system has broken some existing feature, it needs to be done as economically as possible. A particularly important class of software systems are API libraries. Such libraries would typically constitute a very important component of many software systems. High quality requirements make it imperative to continually optimise the internal implementation of such libraries without affecting the external interface. Therefore, it is preferred to guide the regression testing by some kind of formal specification of the library. The testing problem comprises of three parts: computation of test data, execution of test, and analysis of test results. Current research mostly focuses on the first part. The objective of test data computation is to maximise the probability of uncovering bugs, and to do it with as few test cases as possible. The problem of test data computation for regression testing is to select a subset of the original test suite running which would suffice to test for bugs probably inserted in the modifications done after the last round of testing. A variant of this problem is that of regression testing of API libraries. The regression testing of an API is usually done by making function calls in such a way that the sequence of function calls thus made suffices a test specification. The test specification in turn embodies some concept of completeness. In this thesis, we focus on the problem of test sequence computation for the regression testing of API libraries. At the heart of this method lies the creation of a state space model of the API library by reverse engineering it by executing the system, with guidance from an formal API specification. Once the state space graph is obtained, it is used to compute test sequences for satisfying some test specification. We analyse the theoretical complexity of the problem of test sequence computation and provide various heuristic algorithms for the same. State space explosion is a classical problem encountered whenever there is an attempt of creating a finite state model of a program. Our method also faces this limitation. We explore a simple and intuitive method of ameliorating this problem – by simply reducing the size of the state vector. We develop the theoretical insights into this method. Also, we present experimental results indicating the practical effectiveness of this method. Finally, we bring all this together into the design and implementation of a tool called Modest.

Model checking is a powerful technique for analyzing reach ability and temporal properties of finite state systems. Model-checking finite state systems has been well-studied and there are well known efficient algorithms for this problem. However these algorithms may not terminate when applied directly to in finite state systems. Counter systems are a class of in fininite state systems where the domain of counter values is possibly in finite. Many practical systems like cache coherence protocols, broadcast protocols etc, can naturally be modeled as counter systems. In this thesis we identify a class of counter systems, and propose a new technique to check whether a system from this class satires’ a given CTL formula. The key novelty of our approach is a way to use existing reach ability analysis techniques to answer both \until" and \global" properties; also our technique for \global" properties is different from previous techniques that work on other classes of counter systems, as well as other classes of in finite state systems. We also provide some results by applying our approach to several natural examples, which illustrates the scope of our approach.

Die Marktbedingungen in der Automobilindustrie sind durch kürzere Entwicklungszeiträume, eine zunehmende Anzahl an Komfortfunktionen und Fahrzeugderivaten sowie steigende Erwartungen an Qualität, Effizienz und Sicherheit geprägt. Die reale Erprobung ist ein kritischer Pfad im Entwicklungsprozess. Die vorliegende Arbeit beschreibt ein neues Prüfsystemkonzept für die Komponentenerprobung, welches diesen Anforderungen Rechnung trägt. Das Herzstück ist eine softwarebasierte Systemarchitektur zur Automatisierung von Prototypentests. Schwerpunkte sind die Flexibilität in der Praxisanwendung, die Ausweitung der Messdatenerfassung mit zweckmäßiger Verwaltung zur Bauteilüberwachung und Fehlerrekonstruktion sowie eine aufgabenorientierte Schnittstelle zur Integration von Robotern. Diese übernehmen die mechanische Betätigung von beweglichen Fahrzeugkomponenten. Anhand von zwei konkreten Beispielen, einem Prüfstand zur Absicherung von Fahrzeugtüren sowie einem Prüfstand für Steifigkeitsmessungen wird die Praxistauglichkeit nachgewiesen.