On the use of assertions for embedded-software dynamic verification