[ecoop-info] Annual Landin Semantics Seminar: Semantic Families for Cyber Physical Systems, By Prof. Jan Peleska, 7th December, London

[Announcements of FME events]

Please could you distribute details of the upcoming Landin seminar, jointly
organized by FME Europe and BCS-FACS
thank you.

Paul Boca
_____

                  Annual Peter Landin Semantics Seminar

Organized jointly with Formal Methods Europe (FME) and BCS-FACS Specialist
Group

                   Semantic Families for Cyber Physical Systems

                     By Prof Jan Peleska (University of Bremen)


                         Date/Time: 7th December 2015, 6pm



Venue: BCS, First Floor, The Davidson Building, 5 Southampton Street,
London, WC2E 7HA

Book online at: https://events.bcs.org/book/1673/


Peter Landin (1930 - 2009) was a pioneer whose ideas underpin modern
computing. In the 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               Tea/Coffee


6.00pm               Welcome & Introduction (Professor 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 well-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.

Sponsors: Formal Methods Europe (FME) and BCS-FACS
-------------- next part --------------
_______________________________________________
events mailing list
events at fmeurope.org
http://fmeurope.hosting.west.nl/mailman/listinfo/events