Peter Landin (1930 - 2009) was a pioneer whose ideas underpin modern computing. In the 1950s and 1960s, Landin showed that programs could be defined in terms of mathematical functions, translated into functional expressions in the lambda calculus, and
their meaning calculated with an abstract mathematical machine. Compiler writers and designers of modern-day programming languages alike owe much to Landin's pioneering work.

Each year, a leading figure in computer science will pay tribute to Landin's contribution to computing through a public seminar. This year's seminar is entitled "Semantic Families for Cyber Physical Systems" and will be given by Prof. Jan Peleska (
University of Bremen). The event will be chaired by Prof. John Fitzgerald (Newcastle University).

Programme

5.15pm - 6.00pm Tea/Coffee & Registration
6.00pm - Welcome & Introduction by Prof. John Fitzgerald, Newcastle University
6.05pm - Peter Landin Semantics Seminar - Semantic Families for Cyber Physical Systems - Prof. Jan Peleska (Bremen University)
7.20pm - 8.30pm - Drinks Reception

Seminar details

In this seminar talk we discuss a potential change of paradigm in the field of semantics, with focus on behavioural modelling formalisms applicable to cyber physical systems (CPS), systems of systems, or complex distributed reactive systems in general.
The ell-established semantic models for these application domains, such as Kripke structures, labelled transition systems, or finite state machines and their denotational or axiomatic counterparts, are reviewed in the light of today's practical
challenges.

To name just a few of them: how do these familiar approaches cope with large numbers of replicated components, the dynamicity of system configurations, evolution of contractual behaviour, and presentation of emergent properties? From the perspective of
today's distributed collaborative development and verification projects another challenge arises: how can artefacts (models, code, verification results) obtained "locally" in a semantic framework specialised for a system component be translated into
another framework used, for example, to model and verify emergent behaviour of the complete CPS?

The challenges and potential solutions are illustrated using examples from testing theories for and bounded model checking of CPS. It is shown how the objective to obtain bounded results (identification of finite test sequences, verification of behaviour
for a bounded number of transitions in the vicinity of a given state) facilitates the elaboration of solutions to the identified problems. Moreover, we advocate the identification of semantic families, each family well-optimised to model the behaviour of
a specific class of applications, and mechanisms to navigate between different families, while being able to translate theories and verification results between families.

It is pointed out that the means to set up such a collection of semantic families and navigation mechanisms have been established long ago and have matured to very powerful tools. To name two prominent examples, Goguen's and Burstall's theory of
institutions (the informal term "family" used above roughly corresponds to an institution), as well as the Unifying Theories of Programming are suitable vehicles for such an undertaking.

If you would like to attend, please book online at

https://events.bcs.org/book/1673/

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)