Timed Model-Checking for Time-Triggered System Designs

• Applicant: Dr. Bernd Westphal
• Subject Area: Software Engineering and Programming Languages
• Term: from 2017 to 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 385729514

The goal of the proposed project is to advance the state of the art in model-checking for timed systems. Timed systems can be modelled and verified using networks of timed automata (Alur & Dill, 1994). Model-checking models of timed systems is currently gaining momentum in the high-tech industry even for small or medium sized enterprises. Although tools like Uppaal have been improved over time, the well-known state explosion problem is still a major obstacle for a wide application of this technology.The project will build upon a body of active research, including our own. In preliminary work, we have introduced the notion of quasi-equal clocks. Quasi-equal clocks in particular occur in concurrent system designs which use time triggered architectures, for example, in the form of the well-known time division multiple access (TDMA) principle for time multiplexing. We have developed a tool called saset, which implements a source-to-source transformation on networks of timed automata (called QE-transformation). Given an original network with quasi-equal clocks, the tool yields a transformed network where all clocks of an equivalence class wrt. quasi-equality are replaced by a single representative clock. In many industrial case-studies from the literature and our own projects, the application of the QE-transformation yields a significant reduction of the number of clocks in the model and of the computational effort for model-checking.The proposed project addresses three subtopics:(1) investigation of complexity aspects and, based on the results, further improvements of the QE-transformation,(2) automatic and efficient inference of certain clock resetting edges for which the QE-transformation is most effective, and(3) development of a new model-checking procedure where inference of quasi-equality and the QE-transformation are tightly integrated.The overall contribution of the project will be theoretical and practical. We will have a deeper understanding of the possibilities and the limitations of the QE-transformation. We will have a tool as an extension of saset with an improved QE-transformation and integrated modules for inferring independent edges, and an implementation of the new model-checking procedure. The tool will be made available to the academic research community.

• DFG Programme: Research Grants