Course Introduction

---

ECNU Summer School 2021 Program

2021.08.23 Monday	2021.08.24 Tuesday	2021.08.25 Wednesday	2021.08.26 Thursday	2021.08.27 Friday
08:00-11:00 Kristin Y. Rozier	08:00-11:00 Kristin Y. Rozier	09:00-10:00 Moshe Y. Vardi (Keynote from TASE 2021)	09:00-10:00 Kokichi Futatsugi (Keynote from TASE 2021)	08:00-11:00 Kristin Y. Rozier
15:00-18:00 Frederic Mallet	14:00-17:00 Frederic Mallet	10:30-18:30 Sessions from TASE 2021	10:30-18:30 Sessions from TASE 2021	14:00-17:00 Frederic Mallet

Introduction to Formal Methods (Prof. Kristin Yvonne Rozier)

This course will provide an introduction to formal methods, a set of mathematically rigorous techniques for the formal specification, validation, and verification of safety- and security-critical cyberphysical systems, of which aircraft and spacecraft are the prime example. We will discuss the principles of formal methods, when and why to use them, and their strengths and limitations. Our exploration will highlight state-of-the-art tools, techniques, and application

Professor Kristin Yvonne Rozier heads the Laboratory for Temporal Logic in Aerospace Engineering at Iowa State University; previously she spent 14 years as a Research Scientist at NASA and three semesters as an Assistant Professor at the University of Cincinnati.

She earned her Ph.D. from Rice University and B.S. and M.S. degrees from The College of William and Mary. Dr. Rozier's research focuses on automated techniques for the formal specification, validation, and verification of safety critical systems. Her primary research interests include: design-time checking of system logic and system requirements; runtime system health management; and safety and security analysis.

Her advances in computation for the aerospace domain earned her many awards including: the NSF CAREER Award; the NASA Early Career Faculty Award; American Helicopter Society's Howard Hughes Award; Women in Aerospace Inaugural Initiative-Inspiration-Impact Award; two NASA Group Achievement Awards; two NASA Superior Accomplishment Awards; Lockheed Martin Space Operations Lightning Award; AIAA's Intelligent Systems Distinguished Service Award. She holds an endowed position as Black & Veatch faculty fellow, is an Associate Fellow of AIAA, and is a Senior Member of IEEE, ACM, and SWE. Dr. Rozier has served on the NASA Formal Methods Symposium Steering Committee since working to found that conference in 2008.

Introduction to Synchronous Programming (Prof. Frederic Mallet)

Frederic Mallet is a Professor of Computer Sciences at Université Côte d'Azur in France. He is a permanent member of the Kairos team, a joint team between Inria Côte d'Azur and a CNRS joint unit called I3S. His research interests lie in the definition of sound models for the modeling and verification of temporal and timed aspects of safety-critical systems, including smart transportation systems, autonomous vehicles and extensions within Cyber-Physical Systems. The main results have been used to promote the use of logical time as an elastic notion of time that can cover all aspects from the early requirements to the deployment on embedded targets. The Clock Constraint Specification Language (CCSL) provides a concrete syntax to bring to life as first-class citizens this concept of logical clocks initiated by Leslie Lamport and Synchronous Languages in the late 70s, early 80s. In 2009, CCSL drives the definition of the time model of the OMG Profile for Modeling of Real-Time and Embedded systems (MARTE - https://www.omg.org/omgmarte/).

During the lecture, he is going to introduce some symbolic representations to encode efficiently properties that need to be verified (Binary Decision Diagrams, Synchronized Product of Automata) and to show how these data structures are used in practice in many verification frameworks, including synchronous languages.

Program Verification: a 70+-Year History(Prof. Moshe Y. Vardi, Keynote Talk I of TASE2021)

The year 2019 sees the 70th anniversary to Alan Turing's 1949 paper, "Checking a Large Routine" and the 50th anniversary of Tony Hoare's paper, "An Axiomatic Basis for Compuer Programming". In the latter paper, Hoare stated: "When the correctness of a program, its compiler, and the hardware of the computer have all been established with mathematical certainty, it will be possible to place great reliance on the results of the program, and predict their properties with a confidence limited only by the reliability of the electronics." In this talk, I will review the history of this vision, describing the obstacles, the controversies, and progress milestones. I will conclude with the description of both impressive progress and dramatic failures exhibited over the past few years.

Moshe Y. Vardi is University Professor and the George Distinguished Service Professor in Computational Engineering at Rice University. He is the recipient of several awards, including the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Knuth Prize, the IEEE Computer Society Goode Award, and the EATCS Distinguished Achievements Award. He is the author and co-author of over 650 papers, as well as two books. He is a Guggenheim Fellows as well as fellow of several societies, and a member of several academies, including the US National Academy of Engineering and National Academy of Science. He holds seven honorary doctorates. He is a Senior Editor of the Communications of the ACM, the premier publication in computing.

Advances of Proof Scores in CafeOBJ(Prof. Kokichi Futatsugi, Keynote Talk II of TASE2021)

Critical flaws continue to exist at the level of domain, requirement, and/or design specification, and specification verification, i.e., to prove a specification has desirable properties, is still one of the most important challenges in software engineering. CafeOBJ is an executable algebraic specification language system that can be used for specification verification by writing proof scores. Domain/requirement/design engineers using CafeOBJ are expected to construct proof scores for getting reliable specifications . CafeOBJ is a sister language of OBJ and proof scores have been brought up by the OBJ/CafeOBJ community. Specification verification is theorem proving where the specification is a set of axioms and the desirable properties are theorems. Fully automatic theorem proving often fails to convey an understanding of proof, and one should seek to make optimal use of the respective abilities of humans and computers, so that computers do the tedious formal calculations, and humans do the high level planning. Proof scores intend to meet these goals by hiding the detailed calculations done by machines while revealing the proof plan created by humans. This talk explains advances of proof scores for specification verification in CafeOBJ.

Kokichi Futatsugi is a Professor Emeritus at Japan Advanced Institute of Science and Technology (JAIST), Nomi, Ishikawa, Japan. He worked for JAIST from 1993 to 2017 as a Professor, a Dean of School, an Adviser of President, and a Specially Assigned Professor. Before getting a professorship at JAIST, he worked for Electrotechnical Laboratory (ETL, the national research institute for electronics and informatics) from 1975 to 1993 as a Researcher, a Section Chief, and a Chief Researcher of Institute. He worked for SRI International (Stanford Research Institute) in California as an International Fellow from 1983 to 1984 and designed and implemented OBJ algebraic specification language system. From around mid nineties he headed several research projects funded by Japanese Government for developing CafeOBJ algebraic specification language system. Professor Futatsugi served for many international scholarly activities including a Program Committee Chair of 20th International Conference of Software Engineering (ICSE 1998) and an Associate Editor of ACM Transactions of Software Engineering and Methodology (TOSEM) from 1995 to 2002. He is an Honorary Member of Japan Society of Software Science and Technology since 2019.