The project is intended to study and design theoretical models for the verification of embedded systems, in particular hybrid and real-time software systems, by combining abstract interpretation and model checking techniques.
The project aims both at specifying novel automatic tools based on model checking and abstract interpretation, and defining a taxonomy of modal specification logics and system models based onthe precision and computational complexity of verification procedures.
The activities of the research unit in Verona are scheduled as follows:
- Task 1: Completeness of abstract models
In this task we are mainly interested in the systematic design of temporal logic which are complete for a given, possibly abstract, system and in the application of complete model checking in the automatic certification of secure information flows in software for embedded systems, e.g. Java byte-code program. The first issue is an essential step in order to specify the properties of the approximate system that can be checked by complete model checking. This is fundamental in order to provide a taxonomy of temporal logic with respect to the structure of abstract systems and completeness. The second instead, is particularly relevant in order to automatically verify secure information flows in Java byte-code.
- Task 2: Abstract interpretation and model checking of real-time and hybrid systems
In this field we are interested in extending the theory of complete abstract interpretation to the abstract model checking of systems with continuous information (either real-time or hybrid and probabilistic). This can be achieved by first generalizing the theory of abstract domain refinement to the refinement of abstractions of hybrid systems, and then to study the problems of completeness in these systems. The major challenge in this field is given by the structure of hybrid systems, involving continuous information (e.g. differential equations). In this direction we plan to consider as background the recent studies in the field of domain-theory for probabilistic and real-time systems, and the works on abstract interpretation of probabilistic programming.