Database of Research Tools Developed Using CADP

MOZART Tool for Designing and Deploying Advanced IoT Applications

Organisation: Nokia Bell Labs, Nozay (FRANCE)
CONVECS project-team, Inria Grenoble - Rhône-Alpes and LIG, Grenoble (FRANCE)

Functionality: Internet of Things

Tools used: Mozilla Web of Things
CADP (Construction and Analysis of Distributed Processes)

Period: 2019-2022

Description: The Internet of Things (IoT) originally refers to everything connected via the internet. It recently evolved to represent physical devices and software objects deployed on lightweight nodes that communicate with each other and results in new added-value applications built on top of those devices and objects. The growth of the connected device market and its central role in many application areas (healthcare, transportation, agriculture, manufacturing, smarthomes and cities, etc.) has turned IoT at the heart of the digital economy. The advent of IoT has introduced a number of challenges, such as security, privacy, platform heterogeneity, lack of universal standards, device autonomy, and application design.

This work proposes an approach to support end-users when designing IoT applications that are not simplistic, thus cannot be built by simple rules or existing recipes using popular tools like IFTTT. The approach includes a composition language, which allows one to write not only event-action rules, but also to compose these rules to impose an order of execution between two rules, a choice among several rules or a simultaneous execution of several rules. The writing of a composition expression is achieved using a user-friendly interface newly implemented, which does not require a high-level of domain expertise. Since building such advanced compositions can be error-prone (e.g., resulting into erroneous or deadlocking executions), the approach also provides analysis techniques for automatically detecting errors in the composition. Last but not least, the approach supports not only the design of the application, but also its deployment.

The whole approach was implemented using three different components gathered under the name MOZART (Mozilla and Advanced Rule Triggers). First, the Mozilla Web of Things (WoT) platform was extended by developing an interface to support advanced compositions. This interface also enables users to perform the subsequent steps, i.e., design, analysis, and deployment. Second, the analysis part is achieved by encoding the objects and composition expression into LNT and by invoking the verification tools available in the CADP toolbox. Third, application deployment is managed by an execution engine built on top of the Mozilla WebThings platform.

The R-MOZART extension brings support for reconfiguring IoT applications. Three notions of reconfiguration are proposed (seamless, conservative, and impactful) and implemented using the Maude rewriting framework. Quantitative properties related to probability and cost analysis are analyzed using CADP, and functional properties are verified using the Maude tool.

Conclusions: The MOZART tool was proposed for supporting end-users when designing new IoT applications using available objects and devices. The tool was evaluated by carrying out an extensive number of experiments involving the deployment of advanced compositions, which indicated that users can build verified home automation applications easily and in a reasonable amount of time (a few minutes).

Publications: [Krishna-LePallec-Martinez-et-al-20] Ajay Krishna, Michel Le Pallec, Alejandro Martinez, Radu Mateescu, and Gwen Salaün. "MOZART: Design and Deployment of Advanced IoT Applications". Companion Proceedings of the Web Conference WWW'2020 (Taipei, Taiwan), pp. 163-166, April 2020.
Available on-line at:
or from the CADP Web site in PDF or PostScript

[Salaun-21-b] Gwen Salaün. "Consistent Substitution of Object in Rule-based IoT Applications". Proc. of the IEEE 45th Annual Computers, Software, and Applications Conference (COMPSAC'2021), Madrid, Spain, July 12-16, 2021.
Available on-line at:
or from the CADP Web site in PDF or PostScript

[Krishna-LePallec-Mateescu-Salaun-22] Ajay Krishna, Michel Le Pallec, Radu Mateescu, and Gwen Salaün. "Design and Deployment of Expressive and Correct Web of Things Applications". ACM Transactions on Internet of Things 3(1):1-30, 2022.
Available on-line at:
or from the CADP Web site in PDF or PostScript

[Duran-Krishna-LePallec-et-al-22] Francisco Durán, Ajay Krishna, Michel Le Pallec, Radu Mateescu, and Gwen Salaün. "Models and Analysis for User-driven Reconfiguration of Rule-based IoT Applications". Internet of Things 19:100515, August 2022.
Available on-line at:
or from the CADP Web site in PDF or PostScript

Gwen Salaün
Inria Grenoble - Rhône-Alpes / CONVECS
655 Avenue de l'Europe
38330 Montbonnot Saint-Martin
Email: Gwen.Salaun at

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Fri Feb 23 09:45:26 2024.

Back to the CADP research tools page