Formal models are central to building confidence in complex software systems. Type systems, interface theories, formal semantics, and concurrent models of computation all augment classical software engineering techniques such as object-oriented design to catch errors and to make software more modular and composable. Every formal model lives within a modeling framework that gives semantics to the model, and many modeling frameworks have been developed that enable rigorous analysis and proof of properties. But every such modeling framework is an imperfect mirror of reality. A computer system operating in the physical world may or may not accurately reflect behaviors predicted by a model, and the model may not reflect behaviors that are critical to correct operation of the software. Software in a cyber-physical system, for example, has timing properties that are rarely represented in formal models. In this talk, I will examine the limitations in the use of models. I will show that two very different classes of models are used in practice, classes that I call “scientific models” and “engineering models.” These two classes have complementary properties, and many misuses of models stem from confusion about which class is being used.

Edward A. Lee is the Robert S. Pepper Distinguished Professor Emeritus in EECS at UC Berkeley. He is the author of several books and more than 300 papers and has delivered more than 170 keynote and other invited talks at venues worldwide. Lee’s research focuses on cyber-physical systems, which integrate physical dynamics with software and networks. His focus is on the use of deterministic models as a central part of the engineering toolkit for such systems. He is the director of iCyPhy, the Berkeley Industrial Cyber-Physical Systems Research Center, and the director of the Berkeley Ptolemy project. From 2005-2008, he served as chair of the EE Division and then chair of the EECS Department at UC Berkeley. He led the development of several influential open-source software packages, notably Ptolemy and its spinoffs. From 1979 to 1982 he was a member of technical staff at Bell Labs in Holmdel, New Jersey. He is a co-founder of BDTI, Inc. and has consulted for a number of other companies. He is a Fellow of the IEEE, was an NSF Presidential Young Investigator, won the 1997 Frederick Emmons Terman Award for Engineering Education, received the 2016 Outstanding Technical Achievement and Leadership Award from the IEEE Technical Committee on Real-Time Systems (TCRTS) and The Berkeley Citation in 2018.

————————————————————————————————————————————————————————————————————————————–

Many of the recent cryptocurrency bugs and exploits are due to flaws or weaknesses of the underlying blockchain programming languages or virtual machines. The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore. New blockchain languages or virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially significant value. Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines. We present recent academic and commercial results in developing blockchain languages and virtual machines that come directly equipped with formal analysis and verification tools. The main idea is to generate all these automatically, correct-by-construction from a formal specification. We demonstrate the feasibility of the proposed approach by applying it to two blockchains, Ethereum and Cardano.

Grigore Rosu is a professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL), and the founder and president of Runtime Verification, Inc (RV). His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering and programming languages. Before joining UIUC in 2002, he was a research scientist at NASA Ames. He obtained his Ph.D. at the University of California at San Diego in 2000. He was offered the CAREER award by the NSF, the Dean’s award for excellence in research by the College of Engineering at UIUC in 2014, and the outstanding junior award by the Computer Science Department at UIUC in 2005. He won the ASE IEEE/ACM most influential paper award in 2016 (for an ASE 2001 paper that helped shape the runtime verification field), the ACM SIGSOFT distinguished paper awards at ASE 2008, ASE 2016, and OOPSLA 2016, and the best software science paper award at ETAPS 2002.

————————————————————————————————————————————————————————————————————————————