Formal Modelling of App-Ensembles

Abstract

This chapter shows how flexible systems of user interfaces with an underlying formal model can be created by learning from the success story of apps on mobile devices and leveraging the concept of business process modelling. It is shown how these multi-app user interfaces are modelled and how they can be transformed into Petri nets in order to apply existing formal analysis methods. The created user interfaces are called App-Ensembles and resemble interactive systems comprised of self-contained apps that are connected in a purposeful manner via navigation links and data channels. A formal language for modelling these App-Ensembles is introduced (AOF-L). The graphical modelling elements are taken exclusively from BPMN 2.0 (Business Process Model and Notation). The underlying notation is formalized using an OWL 2 ontology. It is shown how App-Ensembles can be easily integrated into existing classical business process models. Two use cases illustrate the utility of App-Ensembles and the practicality of the modelling approach. This chapter demonstrates that it is useful to combine a semi-formal graphical notation with a strictly formal mathematical model. Strengths of the approach include the ability to run reasoning algorithms on the model, to query the model using languages such as SPARQL, and to perform a formal verification regarding contradictions and BPMN compliance.