Published: 8th July 2014
DOI: 10.4204/EPTCS.156
ISSN: 2075-2180

EPTCS 156

Proceedings 2nd French Singaporean Workshop on
Formal Methods and Applications
Singapore, 13th May 2014

Edited by: Shang-Wei Lin and Laure Petrucci

Preface
Shang-Wei Lin and Laure Petrucci
Invited Presentation: Knowledge for Obtaining Distributed Implementations and Proving Them Correct
Susanne Graf
1
Invited Presentation: Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata
Jun Sun
2
Invited Presentation: A Class of Distributed Markov Chains
P.S. Thiagarajan
3
Invited Presentation: Semantic Reasoning and Verification for Ambient Assisted Living
Thibaut Tiberghien and Mounir Mokhtari
4
Correct-by-design Control Synthesis for Multilevel Converters using State Space Decomposition
Gilles Feld, Laurent Fribourg, Denis Labrousse, Bertrand Revol and Romain Soulat
5
Experience using Coloured Petri Nets to Model Railway Interlocking Tables
Somsak Vanit-Anunchai
17
RTL2RTL Formal Equivalence: Boosting the Design Confidence
M V Achutha Kiran Kumar, Aarti Gupta and S S Bindumadhava
29
Verified Subtyping with Traits and Mixins
Asankhaya Sharma
45

Preface

This volume contains the proceedings of the 2nd French Singaporean Workshop on Formal Methods and Applications (FSFMA'14). The workshop was held in Singapore on May 13th, 2014, as a satellite event of the 19th International Symposium on Formal Methods (FM'14).

FSFMA aims at sharing research interests and launching collaborations in the area of formal methods and their applications. The scientific subject of the workshop covers (but is not limited to) areas such as formal specification, model checking, verification, program analysis/transformation, software engineering, and applications in major areas of computer science, including aeronautics and aerospace. The workshop brings together researchers and industry R&D experts from France, Singapore and other countries together to exchange their knowledge, discuss their research findings, and explore potential collaborations.

The main theme of the workshop is to establish links between academic and industry scientists interested in methods and techniques for constructing reliable systems using formal methods. The scientific topics of the workshop include, but are not limited to:

Program

This volume contains 4 regular contributions. The workshop also comprised four invited talks, that are:

The workshop received eight submissions, four of which were accepted. Each regular paper was reviewed by at least three different reviewers. The four regular papers are:

Support and Acknowledgement

FSFMA 2014 is partially supported by NUS and LIPN. We would like to thank these two entities for their organisational support.

Finally, we would like to thank the editorial board of the Electronic Proceedings in Theoretical Computer Science, and in particular Editor-in-Chief Rob van Glabbeek for his support.

In Singapore and Villetaneuse,

Shang-Wei Lin and Laure Petrucci

Program Committee

General Chairs

Program Committee Chairs

PhD Session Chairs

Program Committee


Knowledge for Obtaining Distributed Implementations and Proving Them Correct

Susanne Graf (Verimag/CNRS Grenoble)

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.


Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata

Jun Sun (Singapore University of Technology and Design)

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.

Short 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 Assistant 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.


A Class of Distributed Markov Chains

P.S. Thiagarajan (School of Computing, National University of Singapore)

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.

(Joint work with Ratul Saha, Sumit Jha and Madhavan Mukund.)

Short 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.


Semantic Reasoning and Verification for Ambient Assisted Living

Thibaut Tiberghien (Image & Pervasive Access Lab (IPAL), CNRS UMI, Singapore / Institut Mines-Télécom, France)
Mounir Mokhtari (Image & Pervasive Access Lab (IPAL), CNRS UMI, Singapore / CNRS LIRMM / Institut Mines-Télécom, France)

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.

Short bios:

Dr. Thibaut Tiberghien, Ph.D. in 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.