Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic

• Applicant: Professor Dr. Gerald Lüttgen, since 5/2020
• Subject Area: Theoretical Computer Science
• Term: from 2013 to 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 233929853

This project shall significantly enhance the foundations and practical utility of concurrency-theoretic specification formalisms, and in particular interface theories, that enrich state machine notations with logic connectives, thus promising more concise specifications. Prior work in this project has seen the development of the MIA (Modal Interface Automata) interface theory that combines de Alfaro and Henzinger´s Interface Automata with Larsen et al.´s Modal Transition Systems. In contrast to related work, MIA is nondeterministic, properly handles conjunction and internal behaviour, and allows for fully compositional interface refinement, all while preserving an optimistic view of component compatibility. The project so far has also added temporal-logic operators for expressing safety properties within interfaces, thereby yielding a truly heterogeneous specification theory.The follow-up project proposed here shall further enrich MIA´s heterogeneity and practicality along three dimensions. Firstly, the MIA framework shall be elaborated so as to be able to reason also about liveness and fairness properties, and equipped with an according and more sophisticated notion of interface refinement. Secondly, MIA´s communication mechanism shall be extended to handle value-passing and complemented by a mechanism for shared-variable communication; both are necessary to adequately capture features of modern parallel programming languages. Thirdly, MIA shall be cast into a behavioural type theory, thereby making it not only useful for the model-based design but also for the programming of complex concurrent systems. The outcome of this project shall be novel and expressive interface and behavioural type theories as well as accompanying prototypic tools centered around Google´s parallel programming language Go, together with demonstrators and evaluations on the basis of case studies.

• DFG Programme: Research Grants
• International Connection: Finland, USA
• Cooperation Partners: Professor Rance Cleaveland, Ph.D.; Professor Dr.-Ing. Uwe Nestmann; Professor Antti Valmari
• Ehemaliger Antragsteller: Professor Dr. Walter Vogler, until 5/2020