Annual Landin Semantics Seminar
Date: Dec 07, 2015 12:00 pm – Dec 07, 2015 3:00 pm
Location: London
Annual Landin Semantics Seminar: Semantic Families for Cyber-Physical Systems
By Prof. Jan Peleska | jointly organized by FME Europe and BCS-FACS Specialist Group
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
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
Submitted by Amy Karns
on
Annual Landin Semantics Seminar: Semantic Families for Cyber-Physical Systems
By Prof. Jan Peleska | jointly organized by FME Europe and BCS-FACS Specialist Group
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
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