| KEYWORD |
Model checking of properties of domotic environments
keywords AMBIENT INTELLIGENCE, FORMAL MODELS, MODEL CHECKING
Reference persons FULVIO CORNO
Research Groups E-LEARNING, E-INTELLIGENCE, E-INTERACTION GROUP - E-LITE
Thesis type RESEARCH
Description Use model checking technologies for proving temporal properties over intelligent domotic environments
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.
Required skills Good programming skills, Logic Formalisms
Deadline 10/11/2012
PROPONI LA TUA CANDIDATURA