Gul Agha
University of Illinois at Urbana-Champaign, USA
Building Dependable Concurrent Systems through Probabilistic Inference, Predictive Monitoring and Self-Adaptation
The infeasibility of statically verifying complex software is well established; in concurrent systems, the difficulty is compounded by nondeterminism and the possibility of ‘Heisenbugs’. Using runtime verification, one can not only monitor a concurrent systems to check if it has violated a specification, but potentially predict future violations. However, a key challenge for runtime verification is that specifications are often incomplete. I will argue that the safety of concurrent systems could be improved by observing patterns of interaction and using probabilistic inference to capture intended coordination behavior. Actors reflecting on their choreography this way would enable deployed systems to continually improve their specifications. Mechanisms to dynamically add monitors and enforce coordination constraints during execution would then facilitate self-adaptation in concurrent systems. I will conclude by suggesting a program of research to extend runtime verification so systems can evolve robustness through such self-adaptation.
Gul Agha is Professor of Computer Science at the University of Illinois at Urbana-Champaign. Agha is a Fellow of the IEEE and a recipient of the IEEE Computer Society Meritorious Service Award. He served as Editor-in-Chief of IEEE Concurrency: Parallel, Distributed and Mobile Computing (1994-98), and of ACM Computing Surveys (2000-2007). While Agha is best known for his work on the formalization of the Actor Model and the development of actor languages, he has also led his research group in pioneering research on statistical model checking, concolic testing, computational learning for verification, and in developing a computational model for energy complexity of parallel algorithms. Agha is the co-director of the interdisciplinary Illinois Structural Health Monitoring Project which has developed sensor networks to monitor civil infrastructure, and a co-founder of Embedor Technologies which is using actor inspired distributed computing to enable continuous monitoring of bridges for improved maintenance and anomaly detection.
Oded Maler
CNRS and University of Grenoble-Alpes (UGA), France
Monitoring: Qualitative and Quantitative, Real and Virtual, Online and Offline
In this talk I will present some of the research I have been involved in concerning the specification and monitoring of timed, continuous and hybrid behaviors using formalism such as Signal Temporal Logic and Timed Regular Expressions. I will discuss the similarities and differences between properties/assertions and other “measures” which are used in many application domains to evaluate behaviors, as well as the difference between monitoring real systems during their execution and monitoring simulated models during the system design phase.
Oded Maler is research director as CNRS-VERIMAG, University of Grenoble-Alpes where he leads research activities on timed and hybrid models of cyber-physical systems. He obtained a B.A. in Computer Science (Technion, 1979), M.Sc. in Management Science (Tel-Aviv University, 1984) and Ph.D. in Computer Science (Weizmann Institute, 1990). Dr. Maler is among the initiators of the research on hybrid systems and his current research interests include the application of hybrid verification and monitoring techniques to control systems, analog circuits and systems biology as well as some topics in multi-criteria optimization and machine learning.
Fred B. Schneider
Cornell University, USA
Why Tags Could Be It
Reference monitors generally restrict operation invocation. That limits what policies can be supported. We explore an alternative means of policy enforcement — expressive classes of tags that label data. Tag specification languages will be discussed, with an eye towards static and run-time verification.
Fred B. Schneider is Samuel B. Eckert Professor of Computer Science and chair of Cornell’s CS Dept. He is a fellow of ACM, AAAS, and IEEE, and he is a member of the US National Academy of Engineering and a foreign member of the Norwegian Academy of Technologigcal Sciences. Schneider was awarded a Doctor of Science honoris causa by the University of Newcastle-upon-Tyne in 2003 for his work in computer dependability and security. He received the 2012 IEEE Emanuel R. Piore Award for “contributions to trustworthy computing through novel approaches to security, fault-tolerance and formal methods for concurrent and distributed systems”.