Case studies on automated verification with slope boundaries for block diagrams. (December 2018)

• Record Type: Journal Article
• Authors: Dernehl, Christian; Kühn, Jan; Kowalewski, Stefan
• Is Part Of: Computer languages, systems & structures. Volume 54(2018)
• Page Start: 528
• Page End: 543
• Publication Date: 2018-12
• Subjects: Verification -- Model based development -- Block diagrams -- Simulink; Programming languages (Electronic computers) -- Periodicals; Computer networks -- Periodicals; Computer architecture -- Periodicals; Computer systems -- Periodicals; Langage de programmation; Réseau d'ordinateurs; Architecture d'ordinateur; Périodique électronique (Descripteur de forme); Ressource Internet (Descripteur de forme); 005.13
• DOI: 10.1016/j.cl.2017.09.001
• Languages: English
• ISSNs: 1477-8424

Abstract

Highlights: Automated verification of block diagram models. Slope boundaries as new abstract domain. Integrated symbolic and interval verification. Block diagram case studies from research and industry. Abstract: Model-based development is increasingly used in embedded systems, which are often deployed in a safety-critical environment. Verification techniques, supporting the development process can not only increase safety, but also help to speed up the process. In many cases models are designed with block diagrams, assisting rapid prototyping. However, automated verification is, thereafter, often applied to the resulting code. Instead of focusing on code, we apply verification techniques to models consisting of block diagrams and MATLAB code. We propose to combine a value and slope range analysis, with symbolic methods. In this way, our concept can not only prove properties in models, but also check rate requirements automatically, which arise from physical constraints of the environment. We evaluate our work in case studies from ongoing research projects. These case studies cover the domains of clinical intensive care, autonomous drone control and driver assistance. All systems are also evaluated with a commercial verification tool, highlighting benefits of the tool and our implementation.