ProjectsI am involved in the following projects:
- Centre for Tactile Internet with Human-in-the-loop (CeTI) - Cluster of Excellence in the German Excellence Initiative
- Center for Perspicuous Computing (CPEC) - Collaborative Research Center 248 Foundations of Perspicuous Software Systems
- Journals: LMCS, SCP, FMSD, EMSE, JLAMP, FoMaC, ...
- Conferences: LICS, CONCUR, ICALP, STACS, CSL, FoSSaCS, FSEN, LATA, TACAS, CSR, FASE, VSTTE, FSTTCS, ...
ToolsProFeat is developed at TU Dresden and is both, a language and a tool. It can be used to describe and analyze (probabilistic) feature-oriented systems such as (probabilistic) software product lines. But it is also useful for non-featured family-based analysis and as an extension of the input language of the probabilistic model checker Prism by supporting arrays and simple for-loops. It fully covers the modeling framework for feature-oriented systems presented in the Modularity'14 paper and can generate family-ready Prism models (at least for the parallel feature composition according to the SEFM'19 publication). ProFeat is mainly developed by Philipp Chrszon.
You can find more information about the tool and download options here.
aMeSGee is a tool written in Java I developed for the FORMATS'15 publication about quantitative message sequence graphs (qMSGs). It enables model checking CSL properties even for compositional qMSGs. Please contact me if you are interested in the program. As the underlying semantics also provides a transition-system semantics, this implementation can also be useful for (bounded, non-probabilistic) model checking of MSGs. See also this publication about delayed-choice semantics of MSGs.