Title: Why Formal Modeling Language Semantics Matters

Speaker: Jose Meseguer

        (University of Illinois at Urbana-Champaign, USA)

        formal.cs.uiuc.edu/meseguer

Time: 22nd April 2015, 10:00

Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, CAS

Abstract:

The point of modeling languages is not just modeling, but modeling as a powerful means of making software development much more reliable, reusable, automated, and cost effective. For all these purposes, model transformations, as a disciplined technique to systematically relate models within a modeling language and across languages, play a crucial role. In particular, automatic code generation from models is one of its great advantages.

As in the case of programming languages and compilers for such languages which can be seen as a specific, special case of modeling languages and model transformations| there are two ways of going about all this: (i) the usual, engineering way of building and using practical tools, like parsers, compilers, and debuggers and, likewise, modeling tools and model transformations, where the semantics is implicit in the tools themselves and informal; and (ii) a formal semantics based approach, where the different languages involved are given a formal semantics and correctness issues, such as the correctness of programs and models, and of compilers and model transformers, can be addressed head-on with powerful methods.

It seems fair to say that, both for programming and for modeling languages, the usual engineering approach is at present the prevailing one. But this should not blind us to the existence of intrinsically superior technological possibilities for the future. Furthermore, the reasons for taking formal semantics seriously are even more compelling for modeling languages than for programming languages. Specifically, the following crucial advantages can be gained:

1. Formal Analysis of Model-Based Designs, to uncover costly design errors much earlier in the development cycle.

2. Correct-by-Construction Model Transformations based on formal patterns, that can be amortized across many instances.

3. Modeling-Language-Generic formal analysis tools that are semantics-based and can likewise be amortized across many languages.

4. Correct-by-Construction Code Generators, a burning issue for cyber-physical systems, and a must for high-quality, highly reliable implementations.

Although the full potential for enjoying all these advantages has yet to be exploited and much work remains ahead, none of this is some pie-in-the-sky day dreaming. There is already a substantial body of research, tools, and case studies demonstrating that a formal semantics based approach to modeling languages is a real possibility. For example, formal approaches to modeling language semantics based on: (i) type theory, (ii) graph transformations, and (iii) rewriting logic, all converge in giving strong evidence about the many practical advantages that can be gained. Besides discussing in more detail the issues involved, the talk will give a report from the trenches based on my own personal involvement in advancing semantics-based approached to modeling and programming languages. In particular, I will discuss relevant advances within the rewriting logic semantics project, which explicitly aims at basing both programming and modeling languages on a formal executable semantics; and at developing language-generic, semantics-based formal analysis tool and methods.

Biography:

Jose Meseguer received his Ph.D. in Mathematics from the University of Zaragoza, Spain. He is Professor of Computer Science at the University of Illinois at Urbana-Champaign (UIUC). Prior to moving to UIUC he was a Principal Scientist at SRI International, where he worked from 1980 to 2001 after having held postdoctoral positions at the University of California at Berkeley and IBM Research. He was also an Initiator Member of Stanford University's Center for the Study of Language and Information (CSLI).

Meseguer has made fundamental contributions in the frontier between mathematical logic, executable formal specification and verification, declarative programming languages, programming methodology, programming language semantics, concurrency, and security. His work in all these areas, comprising over 350 publications, is very highly cited. His contributions to security include fundamental concepts such as nointerference, browser security verification, new algorithms and verification techniques to defend systems against Denial of Service (DoS) attacks, and new symbolic techniques to analyze cryptographic protocols modulo complex algebraic properties that have been embodied in the Maude-NPA Protocol Analyzer. He is the creator of rewriting logic, a very flexible computational logic to specify concurrent systems. The 2012 rewriting logic bibliography has about 1,000 publications. The Maude rewriting logic language is one of the most advanced and efficient executable formal specification languages worldwide. It supports a wide range of formal analyses, including symbolic simulation, search, model checking, and theorem proving. It is also an advanced declarative concurrent language with sophisticated object-oriented features and powerful module composition and reflective meta-programming capabilities. He, his collaborators, and other researchers have used Maude and its tool environment to build sophisticated systems and tools, and to specify and analyze many systems, including cryptographic protocols, network protocols, web browsers, cyber-physical systems, models of cell biology, executable formal semantics of programming and software modeling languages, formal analyzers for conventional code, theorem provers, and tools for interoperating different formal systems. Meseguer has given numerous invited lectures at international scientific meetings and has taught advanced courses on his research at leading American, British, German, Spanish, Italian, and Japanese universities and research centers. He has also served in numerous program committees of international scientific conferences and as editor of various scientific journals.