eLite

Intelligent environments, such as smart homes or domotic systems, allow complex control strategies to manage the various capabilities (lighs, doors, temperature, power, music, ...) of a house or a building. Too much automation and too much software can be dangerous, since it may generate (due to software bugs or design defects) unwanted behaviors (locked-in persons, free access to burglars, incontrollable environment, ...).

In previous research, we already developed a semantic model (DogOnt) for describing intelligent domotic environments, and we are able to translate that model into UML Statecharts (described in SCXML) and to simulate the system (using the Commons simulator). Simulation is very useful for validation, but will never give you the certainty of the correctness of the design.

For having exact results about the correct behavior of a complex system, we may rely on model checking, where the system is checked to verify if a given formula about the possible evolutions of the system, expressed in a temporal logic, is true. Such formulae may express properties such as the absence of deadlocks, the reachability of given state configurations, etc.

The thesis aims at using the UMC model checker developed by the CNR in Pisa to prove temporal properties of intelligent domotic environments.

The thesis will consist of a theoretical part, where the semantic matching between the SCXML descriptions and the UMC interpretation is cheched, and a practical part, where suitable translators and automation tools will be developed to enable quick and automated verification of temporal properties.

The system will be validated by designing, and verifying, a set of meaningful properties over a significantly large domotic model.