Description

Domain-specific language for light control queries

TNO-ESI/Philips Lighting are interested in modelling complex systems of lighting. They have modelled systems using a Domain Specific Language. This language can transpile to formal models which can be model checked like any other formal modal.

During the analysis of these model light designers want to check certain properties. An example by TNO-ESI/Philips Lighting of such a property is “when there is no presence detected for 15 minutes, the light in that room is off”.

During my research, I will look into these properties in three pillars. Firstly, a so called Domain Specific Language (DSL) will be created for these queries. This DSL has to be capable of hiding complex formal logic from the light designers and be expressive enough to cover any possible query the light designer wants to test.

Secondly, a Model to Model (M2M) transformation needs to be created to translate these queries to the formal world.

Finally, the queries have to be evaluated in the context of the complete system. Here, the different DSL that TNO-ESI/Philips Lighting plus my DSL come together and have to be verified. TNO-ESI/Philips Lighting is not only interested in whether a query holds, but if it doesn’t hold how long it will take for the system to recover from this violation.

Additional Resources

1. The paper