Verification at the Formal Specification Level / Dipl.-Math. Dipl.-Inf. Nils Przigoda
Sprache des Titels:
Englisch
Original Kurzfassung:
The complexity of modern embedded or pure hardware systems makes it inevitable to consider higher levels of abstraction in order to overcome problems in an acceptable time or with an acceptable effort. In this regard, the so-called Formal Specification Level (FSL) has been proposed in the last years. Here, modeling languages such as UML or SysML are used for describing systems at a very abstract level. Due to their formal nature, they already allow for the conduction of first verification tasks. In the talk, general verification tasks will be introduced and it will be explained how they can be solved using satisfiability solvers (SMT solvers with QF_BV). Besides that, some ideas for debugging inconsistent models will be explained in detail. Other applications for detecting invariant independence, concurrency analysis, frame condition consideration, etc. will shortly be sketched.
Forschungs-