Keynote Speakers
Cesar A. Munoz (NASA)
Title. "Formal Methods in the Development of Highly Assured Software for Unmanned Aircraft Systems"
Abstract. In traditional software development methodologies, operational and functional requirements of systems are often specified in structured natural language notations. These restricted notations provide good documentation support, but only provide limited support for semantic analysis. These notations are not rich enough to unambiguously specify the requirements of safety-critical systems that, for example, involve complex numerical computations or that interact with the physical environment. Examples of these safety-critical systems are autonomous vehicles such as unmanned aircraft systems. This talk advocates the use of expressive formal logics, such as higher-order logic, to specify the operational and functional requirement of unmanned systems and to prove the correctness of these requirements. Semantic analysis of requirements written in higher-order logic is supported through the use of interactive theorem provers. Formal models serve as ideal reference implementations of functional requirements. Hence, formal logics enable software validation techniques where software implementations can be checked against functional requirements in a mechanical way. The Formal Methods group in the Safety-Critical Avionics Systems Branch at NASA Langley Research Center (LaRC) has conducted research on the development and application of formal methods technology to safety-critical applications of interest to NASA for more than 30 years. This talk provides an overview of the formal methods technology developed at NASA LaRC and illustrates its use in the design, validation, and verification of highly-assured autonomous unmanned aircraft systems.
Short Bio. Dr. Cesar Munoz is a senior research computer scientist at the NASA Langley Research Center, where he leads the Formal Methods Team. Dr. Munoz's primary research interest is the development of formal methods technology for the design, verification, and implementation of safety-critical aerospace systems. Dr. Munoz has contributed to the development of highly-assured software for the next generation of air traffic management concepts developed at NASA, including autonomous unmanned aircraft systems (UAS). In particular, Dr. Munoz is the main developer of DAIDALUS (Detect and Avoid Alerting Logic for Unmanned Systems), a software library selected by the standards organization RTCA SC-228 to be the reference implementation of detect and avoid minimum operational performance for UAS included in the standard DO-365. Dr. Munoz has made several contributions to the development of interactive theorem proving technology for industrial applications. Prior to joining NASA in 2009, he was a Research Fellow at the National Institute of Aerospace. Dr. Munoz has a bachelor degree and master's degree in Computer Engineering from the University of the Andes, Colombia. He got his Ph.D. degree in Computer Science from University of Paris 7, France, in 1997.
Jan Van den Bussche (Hasselt University, Belgium)
Title. "Fully generic queries: Open problems and some partial answers"
Abstract. The class of "fully generic" queries on complex objects was
introduced by Beeri, Milo and Ta-Shma in 1997. Such queries are
still relevant as they capture the class of manipulations on
nested big data where output can be generated without a need for
looking in detail at, or comparing, the atomic data elements.
Unfortunately, the class of fully generic queries is rather
poorly understood. We review the big open questions and
formulate some partial answers.
Joint work with Dimitri Surinx and Jonni Virtema.
Short Bio. Jan Van den Bussche is professor of databases and theoretical computer science at Hasselt University in Belgium. He received his PhD from the University of Antwerp in 1993, under the supervision of Jan Paredaens. He served as PC chair, and chair of the council, for the International Conference on Database Theory, and also as PC chair, and chair of the executive committee, for the ACM Symposium on Principles of Database Systems. His main research interest is in data models and query languages for a wide variety of data applications, ranging from spatial data to data stored in DNA. Most recently he is involved in a project on distributed data intelligence within the context of the Artificial Intelligence Research Flanders initiative.
Bernhard Thalheim (Christian Albrechts University Kiel)
Title. "Semiotics in Databases"
Abstract. In databases syntax is commonly considered a "firstness" property, while semantics is a "secondness" property (in the sense of Peirce); pragmatics is largely neglected. The talk will discuss foundations in first-order predicate logic, highlight the usefulness, but also point out problematic issues. These cover in particular safe expressions in the relational tuple calculus, rigid normalisation emphasising atomicity of attributes, and a large body of knowledge on database constraints. We first survey the beautifulness of classical database constraint theory and then develop an alternative approach to some constraints including (1) the handling of constraint sets instead of homogeneous classes of constraints, (2) visual reasoning on constraints and structures, and (3) calculi for robust reasoning, in particular for "exceptions" and object-relational reasoning.
Short Bio. Bernhard Thalheim is Full Professor of Databases and Information Systems at Christian-Albrechts-University Kiel and honorary Kolmogorov Professor at Lomonossov Moscow State University. Before being appointed to Kiel he worked as Professor at the Universities of Dresden, Kuwait, Rostock and Cottbus. His main fields of research cover databases and information systems, and conceptual modelling, in particular web information systems and foundations of modelling. He is author of the books "Entity-relationship modeling - foundations of database technology" and "Design and Development of Web Information Systems".
Rémi Delmas (ONERA)
Title. "Reinforcement learning-based methods for falsification: a new trend in critical controllers verification"
Abstract. In this talk we give an overview of a relatively recent trend in critical embedded controller verification: the use of (possibly deep) reinforcement learning algorithms for property falsification. The central idea is to use temporal logics with real-valued robust semantics to formulate safety objectives, and to formulate the property falsification problem as reward optimization problem, which can be solved using reinforcement learning algorithms for optimal planning or optimal policy synthesis. After introducing basic definitions and concepts, we review a collection of landmark papers, then we illustrate the approach with results obtained on an significant Airbus case study. Last, we outline current challenges and future research directions.
Short Bio. Rémi Delmas is a research scientist in the Deptartment of Information Processing and Systems at ONERA. He received an aerospace engineering degree from ENSMA in 2000, and completed a PhD in theoretical computer science ONERA-Sup’Aero in 2004, on the topic of compositional modelling and verification of intergated modular avionics systems. Between 2004 and 2009, he worked for Prover Technology, building SAT-based model checking solutions critical railway and train control systems. Back at ONERA since 2009, his research work focuses on adapting and using SAT and SMT-based techniques to solve various problems surrounding critical embedded software design and verification, ranging from safety assessment and fault-tolerant architecture synthesis to functional verification and automatic test case generation.