Formal Verification of A Domain Specific Language for Run-time Adaptation

Compared to general purpose programming languages, domain specific languages (DSLs) targeting adaptive embedded software development provide a very promising alternative for developing clean and error free run-time adaptations. However, the ability to use several rules in a single adaptation strategy, as allowed by some DSLs, may lead to conflicts and reachability issues, which can eventually lead to functional bugs. Traditionally, such conflict analysis is done using software testing or manual manipulation of automata based models of rules. However, both of these techniques are error-prone and thus can lead to unwanted situations. As an accurate alternative, we propose to use model checking for rule conflict and reachability analysis in DSL adaptation. In particular, this paper provides an approach to formally model DSL adaptation specifications, along with their rules, and identifies a set of generic temporal properties to check for reachability and other rule conflicts, using the finite and infinite state-space based model checking capabilities of nuXmv model checker. For illustration, formal analyses of an energy aware CPU scheduling algorithm, i.e, PAST, for adaptivity rules for a stereo navigation system and for a context aware application are presented.