Analysis and Verification of Fault-tolerant Systems
From PUMA Graduiertenkolleg
Model-driven development accelerates the development process of complex systems. The complexity of the development process can be reduced by raising the level of abstraction. Unfortunately, existing code generators focus on functional aspects of the application. Non-functional aspects such as dependability, have to be implemented by the developer itself. Reasons are the absence of adequate models and the implementation's dependency on the used platform. Due to the vast heterogeneity of the used platforms, it is impossible to design a code generator that supports a priori all possible platforms. FTOS, a model-driven development tool for fault-tolerant systems, solves this problem by using a template based code generator. Templates are highly adaptable components that solve the generation of a specific aspect for a specific platform. New templates can be easily added.
In the context of this graduate school, formal verification should be integrated to FTOS to allow to verify the correctness of the generated systems. The verification process has to take into account potential hardware and software failures and has to prove the correct use and implementation of fault-tolerance mechansims.