Invited speakers
Susanne Graf
Title: Knowledge for obtaining Distributed Implementations and proving them correct
Abstract: Deriving distributed implementations from global specifications has been extensively studied for different application domains, and under different assumptions and constraints. The solutions that have been proposed are often relatively adhoc and developed independently for different application domains. We explore here the knowledge perspective to achieve a potential for a more unifying approach: a process decides to take a local action when it has sufficient knowledge to do so. We discuss typical knowledge atoms useful for expressing local enabling conditions with respect to different notions of correctness, as well as different means for obtaining knowledge and for representing it locally in an efficient manner. Our goal is to use such a knowledge-based representation of the distribution problem for either deriving distributed implementations automatically from global specifications, or for improving the efficiency of existing protocols by exploiting local knowledge. We also argue that such a knowledge-based presentation could help for obtaining the necessary correctness proofs.
Jun Sun
Title: Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata
Abstract: Given a timed automaton P modeling an implementation and a timed automaton S as a specification, language inclusion checking is to decide whether the language of P is a subset of that of S. It is known that this problem is undecidable and “this result is an obstacle in using timed automata as a specification language”. This undecidability result, however, does not imply that all timed automata are bad for specification. In this talk, I will introduce a recent study published at TACAS this year. That is, we proposed a zone-based semi-algorithm for language inclusion checking, which incorporates simulation reduction based on Anti-Chain and LU-simulation. Though it is not guaranteed to terminate, we showed that it does in many cases through both theoretical and empirical analysis. The semi-algorithm has been incorporated into the PAT model checker, and applied to multiple systems to show its usefulness and scalability.
Bio: SUN, Jun received Bachelor and PhD degrees in computing science from National University of Singapore (NUS) in 2002 and 2006. In 2007, he received the prestigious LEE KUAN YEW postdoctoral fellowship in School of Computing of NUS. Since 2010, he joined Singapore University of Technology and Design (SUTD) as an Ass istant Professor. He was a visiting scholar at MIT from 2011-2012. Jun's research interests include software engineering, formal methods (e.g., formal specification, model checking) and cyber-security. He is the co-founder of the PAT model checker. To this date, he has about 100 journal articles or peer-reviewed conference papers. Jun is also the general co-chair of ICECCS'13 and program co-chair of FM'14.
P.S. Thiagarajan
Title: A class of distributed Markov chains
Abstract: The formal verification of large probabilistic systems is challenging. Exploiting the concurrency that is often present is one way to address this problem. Here we study a restricted class of probabilistic networks of agents in which the synchronizations obey the ``free choice'' regime of net theory. Such a network can be viewed as a distributed representation of a global Markov chain. It turns out that verification of our model, called DMCs (distributed Markov chains), can often be efficiently carried out by exploiting the partial order nature of the interleaved semantics. To demonstrate this, we develop a statistical model checking (SMC) procedure and use it to verify two large probabilistic distributed systems.
Bio: P.S. Thiagarajan is a Professor in the Department of Computer Science, National University of Singapore and Senior Faculty Member of the NUS Graduate School of Integrative Science and Engineering (NGS).
He received a B.Tech (Electronics) degree from the Indian Institute of Technology, Madras, India (1970) and a PhD degree (Computer Science) from Rice University, Houston, Texas, USA (1973).
He has been held academic positions at various levels starting MIT (USA), GMD(Germany), Aarhus University(Denmark), Institute of Mathematical Science (India) and Chennai Mathematical Institute (India).
Before coming to NUS his research had been devoted to various aspects of the theory of distributed systems including Petri nets, temporal logics and supervisory control. At NUS, he has focused mainly on real time, hybrid and embedded computing systems and computational systems biology.
Thibaut Tiberghien and Mounir Mokhtari
Title: Semantic reasoning and verification for ambient assisted living
Abstract: Our main goal is to propose a software infrastructure (Framework) for the fusion and sharing of semantically labelled ambient intelligent knowledge, and its access for enhanced services to stakeholders (Aged people and care givers). The, semantic web technologies that have already been developed in nursing home environment initiatives is being leveraged on a large scale deployment targeting individual homes and their extension to urban space (smart city). Building the infrastructure to share data is not enough. We must also put in place mechanisms to enhance data into meaningful and actionable knowledge by providing techniques for the assessment of situations in the multiple living spaces. Formal verification and model checking was used to model and verify the reliability of this complex system. During this talk we will mainly focus on the design of a reasoning engine and the use of PAT for rules design and verification in collaboration with NUS team.
Bio: Dr. Thibaut Tiberghien, Ph.D. On Computer Sciences from University Pierre and Marie Curie and Institut Mines Telecom, is expert in semantic ontologies reasoning for user modelling and ambient intelligent service provisioning. Thibaut Tiberghien is currently a Research Fellow at IPAL Lab. in Singapore.
Mounir Mokhtari, Professor at Institut Mines TELECOM, Senior Scientist at IPAL-CNRS French-Singapourian recearch Lab., and Associate Researcher at CNRS LIRMM Montpellier. Mounir Mokhtari, Ph.D. in Computer science on ICT for health, is expert on AmbientAssisted Living. He is also a Chair holder on Quality of Life of ageing people with dementia.