Doctoral thesis committee for Biljana Bajić’s thesis entitled ’Animation-Based Service Specification, Verification and Validation’, supervised by Prof. Alain Wegmann, EPFL.
“Service specifications are used to represent the service systems on different levels of abstraction: from business down to IT. High-level service specifications are mostly used for the communication among different participants, to catalyze the discussions between them, but only service specifications modeling IT systems have enough details to be simulated and executed. As a consequence, it becomes difficult to create precise specifications on high-level of abstraction, potentially leading to severe project problems. This can be compensated with use of formal methods and code generation techniques to get abstract, yet precise specifications, whose services can be simulated and prototyped. By capturing design decisions, the high-level service specifications can be refined into more detailed ones with possibility to validate the specification at any level of abstraction.