Modern embedded systems have more and more constraints on ressources, while their the complexity of their functionality keeps increesing. Not only the functionality should be correct, but other, non-functional aspects have critical importance.
We are particularly interested in the following properties:
This talks starts with a brief panorama of the existing methods for the study of non-functional properties, with a short comparison of computational methods, model-checking, and analytic methods.
We then present the works already carried out in Verimag, in particular in the area of sensor networks (with the simulator Glonemo) and Systems-on-a-Chip (work done in partnership with Docea-Power on early estimation of power-consumption taking temperature into account).
We conclude the first part of the talk with a list of requirements for studying non-functional properties in embedded systems. Mainly: State-based behavior, Solution to the state-explosion problem, and compositionality.
The talks ends with a presentation of work in progress, with mostly two questions: Can Real-time calculus model energy in state-based systems? and How can probabilistic model-checkers scale-up in the verification of a system with quality of service?