We mourn for our friend and colleague Daniel Wonisch.

 † 21.2.2012

Research Group Specification and Modelling of Software Systems

Welcome to the web-pages of the research group "Specification and Modelling of Software Systems"! The scope of the group is model-based software development with formal methods. Formal methods are languages for describing software and hardware, which are equipped with a formal mathematical semantics.The generel objective of such a design technique is the development of high quality software. 

Our research can broadly be structured into three areas: the development of semantics for specification formalisms, the design of verification techniques for proving correctness and the definition of refinement concepts for model transformations. On the application side we apply our methods in the area of service-oriented architectures, mechatronic systems (in particular for reconfiguration) and lock-free algorithms.

Currently we work on the following topics:

• Languages and semantics: 
  • refactoring languages and correctness of refactorings
  
  
• Verification:
  • Compositional verification and decomposition of models
  • Abstraction techniques for parallel systems (DFG project ViPar)
  • Shape analysis for graph transformation systems (SFB 614, subproject B1)
  • Compositional analysis in partially known contexts (SFB 901, subproject B3)
  • Proof-Carrying Code (SFB 901, subproject B4)
  • In addition, we have a cooperation with the subproject R1 of the SFB/TR 14 AVACS in the area of verification methods. 

• Refinement:
  • Correctness of model transformations (cooperation with U. Twente and U. Duisburg-Essen)
  • Linearizability of lock-free algorithms (ccoperation with U. Augsburg and U. Sheffield)