1.1.1. Test generation methods and tools

In the focus of the study are techniques to improve the efficiency of testing embedded systems and system components. In the case of black box testing we assume that the system under test (SUT) communicates with its environment via asynchronous message passing. The benefit of the approach relies on automatic generation and excecution of tests using standard TTCN-3 language from SUT specifications given in state and class diagram form.

 1.1.2. Code generation methods and tools

Theoretical part of this subproject is related to the analysis and development of property preserving model transformations. In practice we study the applicability of transformation definition languages and related tools, for example MTL, ModTransf, ATL, QVT, and KM3 to transform platform independent models to platform specific models, and further on, to executable C# or Java code.

1.1.3. Synthesis of provably correct digital controllers

Well-hidden design faults and unreproducable timing errors can expose in embedded systems when unforeseen or exceptional situations emerge. The goal of the research is to develop methods and algorithms for synthesis of provably correct controller programs. Within the context of timing constraints the correctness is stated in terms of bounded liveness and safety properties. The result of synthesis is a model of controller that is implementable and deployable on relevant hardware architectures using techniques developed under activity line 1.1.2.