Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic
This research project concerns the theoretical foundations and practical utility of the growing number of languages for specifying reactive systems software that enrich state machine notations with logic connectives. Examples are the Interface Theories of de Alfaro/Henzinger and Caillaud et al., which consider logic conjunction, and the Contractual State Machines of Paige et al., which incorporate temporal logic. While these heterogeneous languages promise more concise specifications and are accompanied by modern refinement-based approaches to software design, they lack mathematically robust semantics that respect the concurrency inherent in reactive systems.
Our research applies the setting of Logic Labelled Transition Systems (Logic LTS), which was co-developed by us, to fix this shortcoming. This will pave the way for advanced tool support, including the development of automated refinement checkers for Interface Theories and Contractual State Machines. Future work will also extend Logic LTS so as to capture complex safety, liveness and fairness properties, thereby allowing us to develop richer Interface Theories. It is anticipated that this will permit more concise descriptions of reactive systems software, thereby aiding programmers in software specification and design.
This website reports on the SWT team's current research into interface theories and behavioural types. Based on our previous work on Logic Labelled Transition Systems, Modal Interface Automata and the following DFG project (case for support), we have been pursing multiple lines of research in this topic.
We envisage our Interface Theories to be of use across a number of domains, including the following:
- Heterogenous specification, where operational and declarative formalisms may be combined for specifying concurrent reactive systems in an incremental approach to design.
- Software Product Lines, underspecification may be used to express product variability and one wishes to find compatible subfamilies of given product lines.
- Communication error analysis, the design of complex concurrent systems are prone to subtle communication bugs. A detailed communication error analysis may detect such errors and propose alternative solutions early in the design phase.
- Behavioural types, permitting the transition from design to programming where behavioural types inferred from program code may be verified against interface specifications.
- G. Lüttgen and W. Vogler. Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic. Deutsche Forschungsgemeinschaft (DFG, LU 1748/3-1 and VO 615/12-1), 2013. (Case for Support)
- S. Fendrich and G. Lüttgen. A Generalised Theory of Interface Automata, Component Compatibility and Error. Integrated Formal Methods (iFM 2016), LNCS, 2016. [to appear]
- F. Bujtor, S. Fendrich, G. Lüttgen and W. Vogler. Nondeterministic Modal Interfaces. Theory and Practice of Computer Science (SOFSEM 2015), LNCS 8939, pp. 152-163, 2015. (DOI: 10.1007/978-3-662-46078-8_13)
- G. Lüttgen, W. Vogler, S. Fendrich. Richer Interface Automata with Optimistic and Pessimistic Compatibility. Acta Informatica, 52(4-5), pp. 305-336, 2015 (DOI: 10.1007/s00236-014-0211-0)
- S. Fendrich and G. Lüttgen. A Generalised Theory of Interface Automata, Component Compatibility and Error. Technical report, Bamberger Beiträge zur Wirtschaftsinformatik und Angewandten Informatik No. 98, Univ. Bamberg, 2016.
- F. Bujtor, S. Fendrich, G. Lüttgen and W. Vogler. Nondeterministic Modal Interfaces. Technical report, Reports / Technische Berichte der Fakultät für Angewandte Informatik Nr. 2014-06, Univ. Augsburg, 2014.
- S. Fendrich. What is in an Error? A Generalised Theory of Interface Automata, Component Compatibility and Error. D-CON 2016, Saarbrücken, DE, 2016.
- S. Fendrich. Nondeterministic Modal Interfaces, D-CON 2015, Kerkrade, NL, 2015.
- S. Fendrich. Nondeterministic Modal Interfaces. SOFSEM 2015, Pec pod Sněžkou, CZ, 2015.
- S. Fendrich. Richer Interface Automata with Optimistic and Pessimistic Compatibility. Mini-Workshop on Interface Theories Augsburg, DE, 2014.
In February 2014 we held a small international workshop in Augsburg, Germany to discuss the current state of the art of interface theories.