SETTA 2020
Symposium on Dependable Software Engineering
Theories, Tools and Applications
Guangzhou, China, November 24-28, 2020
Saarland University
Vrije Universiteit Amsterdam
CISPA Helmholtz Center for Information Security
Zhejiang University, China
Holger Hermanns
Lab Conditions for Research on Explainable Automated Decisions
Abstract:
Artificial neural networks are being proposed for automated decision making under uncertainty in many visionary contexts, including high-stake tasks such as suggesting which patient to grant a life-saving medical treatment, or navigating autonomous cars through dense traffic. Against this background, it is imperative that the decision making entities meets central societal desiderata regarding dependability, perspicuity, explainability, and robustness. Decision making problems under uncertainty are typically captured formally as variations of Markov decision processes (MDPs). This keynote discusses a set of natural and easy to-control abstractions that altogether connect the autonomous driving challenge to the modelling world of MDPs. This is then used to study the dependability and robustness of NN-based decision entities which in turn are based on state-of-the-art NN learning techniques. We argue that this approach can be regarded as providing laboratory conditions for a systematic, structured and extensible comparative analysis of NN behaviour, of NN learning performance, as well as of NN verification and analysis techniques.Biography:
Holger Hermanns is Professor in Computer Science at Saarland University in Germany, heading the Dependable Systems and Software group, and Distinguished Professor at Institute of Intelligent Software, Guangzhou. Holger Hermanns is member of Academia Europaea and his research interests include modeling and verification of concurrent systems, resource-aware embedded systems, compositional performance and dependability evaluation, and their applications to energy informatics. He is an outspoken proponent of proactive algorithmic accountability.
Wan Fokkink
The Road Ahead for Supervisor Synthesis
Abstract:
Supervisory Control Theory, initiated by Ramadge-Wonham, turns out to be very suitable for designing and generating software for the control of large infrastructural systems like bridges, locks and tunnels. In this talk recent research results will be discussed that were pivotal in tackling such large applications, including multilevel synthesis, determining a control problem dependency graph, and several modeling guidelines.Biography:
Wan Fokkink studied Mathematics and received his PhD degree in Computer Science from the University of Amsterdam. After a lectureship at the University of Swansea, he became head of the Embedded Systems Group at CWI in Amsterdam in 2000. Since 2004 he is full professor in Theoretical Computer Science at the Vrije Universiteit Amsterdam. Since 2012 is also part-time professor in Model-Based System Design at Eindhoven University of Technology.
His research focus is on the design and analysis of distributed systems, broadly construed. He is author of three textbooks on process algebra, formal verification of distributed systems, and distributed algorithms. He is editor of Logical Methods in Computer Science and of Electronic Proceedings in Theoretical Computer Science, co-founder and former vice-chair of IFIP WG 1.8 on Concurrency Theory, and member of the steering committee of CONCUR.
Andreas Zeller
Learning Input Languages
Abstract:
Abstract: To reason about a function, one needs to know the context in which this function is executed: What are its arguments? What are its data structures? In this talk, I present novel techniques that automatically explore and learn the input language of a program, providing an input grammar from which an endless stream of syntactically valid inputs can be produced. The induced actual executions then provide context from which one can induce invariants, bridging the gap between symbolic reasoning at the function level and testing.Biography:
Andreas Zeller is faculty at the CISPA Helmholtz Center for Information Security and professor for Software Engineering at Saarland University, both in Saarbrücken, Germany. His research on automated debugging, mining software archives, specification mining, and security testing has been highly influential. Zeller is an ACM Fellow, an IFIP Fellow, an ERC Advanced Grant Awardee, and holds an ACM SIGSOFT Outstanding Research Award.
Yongwang Zhao
Rely-guarantee Reasoning about Concurrent Reactive Systems: Framework, Languages Integration and Applications
Abstract:
The rely-guarantee approach is a promising way for compositional verification of concurrent reactive systems (CRSs), e.g. concurrent operating systems, interrupt-driven control systems and business process systems. However, various reaction patterns, different abstraction levels of specification, and the complexity of realworld CRSs are still challenging the rely-guarantee approach. In this talk, we will present PiCore, a rely-guarantee reasoning framework for formal specification and verification of CRSs. We design an event specification language supporting complex reaction structures and its rely-guarantee proof system to detach specification and logic of reactive aspects of CRSs from event behaviours. PiCore parametrizes the language and its relyguarantee system for event behavior using a rely-guarantee interface and allows to easily integrate 3rd-party languages via rely-guarantee adapters. By this design, we have successfully integrated two existing languages and their rely-guarantee proof systems without any change of their specification and proofs. PiCore has been applied to two real-world case studies, i.e. formal verification of concurrent memory management in Zephyr RTOS and a verified translation for a standardized Business Process Execution Language (BPEL) to PiCore.Biography:
Yongwang Zhao, full professor at School of Cyber Science and Technology, College of Computer Science and Technology, Zhejiang University, China. Yongwang’s main research interests are formal methods and their application to security and safety critical software, in particular operating systems (OSs). His research group has formally verified various OSs from China and some OS international standards, where tens of bugs were found, resulted in publications in top formal methods conferences like CAV, FM and TACAS. His research work has been adopted in ARINC653 OS standard and Common Criteria standard.