文摘
This contribution advocates the use of formal methods to verify and certifiably control the behaviour of computational devices interacting over a shared infrastructure. Formal techniques can provide compelling solutions not only when safety-critical goals are the target, but also to tackle verification and synthesis problems on populations of such devices: we argue that alternative solutions based on classical analytical techniques or on approximate computations are prone to errors with global repercussions, and instead propose an approach based on formal abstractions, error-based refinements, and the use of interface functions for the synthesis of abstract controllers and their concrete implementation. Two applicative areas are elucidated, dealing respectively with thermal loads and electricity-generating devices interacting over a smart energy network or over a local power grid. We discuss the aggregation of large populations of thermostatically-controlled loads and of photovoltaic panels, and the corresponding problems of energy management in smart buildings, of demand-response on smart grids, and respectively of frequency stabilisation and grid robustness.
