Jobs & Karriere

Software development starts from preliminary requirements, going through requirement analysis phase, architecture design phase, code implementation phase, and test phase. In traditional software engineering, automatic validation & verification can only be performed after code is implemented. We are working on a new methodology for software engineering in which requirement analysis and architecture design can be described with Java code. Such a methodology makes it possible to conduct automatic validation & verification based on the code generated in the requirement analysis phase and architecture design phase. In order to extract verification models from current code of requirement analysis and architecture design, we need a model extractor which can perform such a task automatically.

Your tasks:

• You will look into current verification models, e.g. the SPIN model. And you will write a report about the characteristics and application domains of these different verification models.
• You will develop the extraction process from Java code to a verification model.
• You will develop a model extractor which can automatically generate verification models from Java code.
• You have to demonstrate the feasibility of your extraction process and the model extractor.