Functional and nonfunctional design verification for embedded software systems

In model-based design verification, software models are checked against functional and nonfunctional requirements. Many of the mathematically well-founded theories developed for functional verification suffer from limitations (poor integration with industrial modeling tools and inability to scale to larger, more complicated systems) that restrict their practical adoption. Nonfunctional verification approaches, because of their inherent subjectivity ("what does it mean for a system to be modifiable?"), remain largely ad hoc and manual. There is also another overarching problem in that functional and nonfunctional verification take place on widely different representations of the system making it difficult to ensure that these representations are consistent with each other. This chapter highlights the latest research done into (1) a practical, formal, coverage-based functional verification approach called instrumentation-based verification, (2) quality attribute reasoning , a semiautomated, nonfunctional verification theory, and (3) an integrated functional and nonfunctional verification approach for model-based development.