VERIS VERification of Interacting Systems
The VERIS-project aims at developing new techniques to increase the quality of embedded systems. The techniques will allow exhaustive checking of all states of the embedded system. Recent results have made this feasible for systems of moderate size. The project will try to push the limit on the size of systems that can be handled to include industrial-sized applications.
The verification group behind the project has already had some initial success in this direction. A new data structure called Boolean Expression Diagrams has improved upon the verification of combinational circuits, and a structural technique has been used in verifying large systems of concurrently executing state machines.
The focus of the VERIS-project is on automatic techniques. It will try to achieve the goals by a combination of compact representations of large state-sets and compositional techniques. The quality of the new techniques will be measured on international benchmarks and examples obtained from our industrial contacts.
The embedded systems can be purely hardware, software, or a mixture of both. Examples of what is considered to be embedded systems are: airbag controllers, portable phones, railway interlocking systems, and digital instruments.
Current members of the project are:
The project has close relationships to other staff members of the Computer Systems Section (see the Formal Verification page) and the project VVS under the Danish Center for Information Technology with participants from Aalborg University and the Danish company Visualstate (now part of IAR Systems). The company was formerly named Baan Visualstate and before that Beologic A/S.
The VERIS-project is directed by Associate Professor Henrik Reif Andersen (hra@itu.dk) and supported by a grant from the Danish Technical Research Council (STVF "Talentprojekt") for initially 3 years starting fall 1997. The project is hosted by the Computer Systems Section within the Department of Information Technology at the Technical University of Denmark. In Danish VERIS is constructed from: "VERifikation af Indlejrede Systemer."