Property-based support for verification and validation - EV2

• Applicant: Professor Dr.-Ing. Ulrich Heinkel
• Subject Area: Electronic Semiconductors, Components and Circuits, Integrated Systems, Sensor Technology, Theoretical Electrical Engineering
• Term: from 2019 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 423801535

Aim of this project is to extend the use of formal methods, which are used in IC design, towards IC verification.In the context of verification, the term "formal methods" describes the process of proving or falsifying desired or undesired IC properties using mathematical methods. Formal verification algorithms are state of the art and can be considered mature.For synthesis of integrated circuits, formal methods are available as well. A suitable formalism for such properties are operation properties which can be used to represent temporal correlations and sequences in multiple granularities. Synthesis of operation properties, i.e. using a property set for automatic generation of a concrete implementation, is well-explored for hardware. One subgoal of this project is to use a complete and consistent set of operation properties for verification. The property set shall be used for automated generation of test cases for the entire functionality as well as corner cases of the specification, enabling the verification of existing, manual implementations of a system under test, with the aid of a formal system specification.Furthermore, an intermediate language shall be developed to enable hardware abstraction and cross-platform application of the proposed methodology. To show the generality of the approach, another target platform is considered (in addition to integrated circuits): Programmable Logic Controllers (PLCs). This platform was chosen, because verification of PLCs doesn’t play a role in practice – even for safety-critical applications like nuclear power control systems. Since PLCs can only cover a part of all possible operation properties, platform-dependent limitations shall be formalized.Furthermore, it is planned that test results should be fed back to the original specification. This is possible for those properties which are suitable for automated test case generation. This enables the creation of a "closed loop" in the waterfall model. At our professorship, the specification tool "SpecScribe" was developed, which implements a workflow for requirements management, backed by formal specification of components and interfaces to formal tools. SpecScribe shall be enhanced in such a way that the "Closed Loop" of specification and verification can be fully represented, which leads to a complete implementation of the waterfall model. This will allow for early visibility of verification results on specification level and it will simplify error tracking from source all the way up to the specification.

• DFG Programme: Research Grants