Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic

Johannes Gareis & Gerald Lüttgen

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 paves the way for advanced tool support, including the development of automated refinement checkers for Interface Theories and Contractual State Machines.

As its main contribution so far, the project has introduced the novel Modal Interface Automata (MIA) theory, which stands apart from related work in that it fully supports compositional, nondeterministic specifications and feature temporal-logic operators for specifying safety properties. Now, the MIA-theory shall be extended in two ways. First, MIAs heterogeneity shall be expanded by adding further logic operators and refining MIA’s semantics, so that also liveness and fairness properties can be expressed. It is anticipated that this will permit more concise descriptions of reactive systems software, thereby aiding programmers in software specification and design. Secondly, MIA’s application scope shall be widened significantly from solely being a refinement theory for compositional specification and design, to also lending itself as a behavioural type theory. This will allow for advanced typing support for parallel programming, which will ultimately lead to more reliable concurrent software.

Applications

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.
  • Communication error analysis, as the design of complex concurrent systems is 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, that help translating from design to programming, where behavioural types inferred from program code may be verified against interface specifications.
  • Software Product Lines, where underspecification may be used to express product variability and one wishes to find compatible subfamilies of given product lines.

Grants

  • 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)
  • G. Lüttgen and W. Vogler. Foundations of Heterogeneous Specifications Using State Machines and Temporal Logic. - Follow up. Deutsche Forschungsgemeinschaft (DFG, LU 1748/3-2), 2016. (Case for Support)

Publications (Peer-reviewed)

  • Lüttgen, G. A Note on Refinement in Hierarchical Transition Systems. In 23rd Intl. Conf. on Formal Methods for Industrial Critical Systems (FMICS 2018) , LNCS, 2018 (DOI: 10.1007/978-3-030-00244-2/_14)
  • Fendrich, S. and Lüttgen, G. A Generalised Theory of Interface Automata, Component Compatibility and Error. Acta Informatica, 2018. (DOI: 10.1007/s00236-018-0319-8)
  • Automata, Component Compatibility and Error. S. Fendrich and G. Lüttgen. A Generalised Theory of Interface Integrated Formal Methods (iFM 2016), LNCS, 2016. (DOI: 10.1007/978-3-319-33693-0_11)
  • 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)

Other Publications

  • 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, D, 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, D, 2014.

Further Talks

  • J. Gareis. Interface Automata for Shared Memory. D-CON 2018, Darmstadt, D, 2018.
  • S. Fendrich. and J. Gareis. From Interface Theories towards Behavioural Types for Go. D-CON 2017, Paderborn, D, 2017.
  • S. Fendrich. What is in an Error? A Generalised Theory of Interface Automata, Component Compatibility and Error. D-CON 2016, Saarbrücken, D, 2016.
  • S. Fendrich. Nondeterministic Modal Interfaces, D-CON 2015, Kerkrade, NL, 2015.
  • S. Fendrich. Richer Interface Automata with Optimistic and Pessimistic Compatibility. Mini-Workshop on Interface Theories, Augsburg, DE, 2014.