Tutorials

Actor-Based Methods, Concepts and Tools for Analysing Emergent Behaviour - An Introduction to a Model Based Approach

Effective organizational decision-making often requires deep understanding of various aspects of an organisation such as goals, structure, business-as-usual, operational processes etc. The large size of an organisation, its socio-technical characteristics, and fast business dynamics make this a challenging endeavor. This tutorial presents a model-based simulation approach to organisational decision-making. We introduce a new technology that supports the approach and illustrate how it is applied to real life problems using real world case studies.

Presenter Information

Tony Clark is Professor of Software Engineering at Sheffield Hallam University in the UK. His academic research on meta-modelling led to the development of a tool called XModeler that has been used in a number of commercial applications including the development of tool support for a new Enterprise Architecture modeling language.

Vinay Kulkarni is Chief Scientist at Tata Consultancy Services Research (TCSR). His research interests include model-driven software engineering, self-adaptive systems, and enterprise modeling. His work in model-driven software engineering has led to a toolset that has been used to deliver several large business-critical systems over the past 15 years. Much of this work has found a way into OMG standards. Vinay also serves as Visiting Professor at Middlesex University London.

Souvik Barat is a Senior Scientist at Tata Consultancy Services Research (TCSR). His research interests include model-driven software engineering, and enterprise modeling.

Balbir Barn is Professor of Software Engineering at Middlesex University London with extensive experience in industrial Software Engineering including the design and implementation of the IEF.


Type
Half-day tutorial


Compiler-agnostic Translation Validation

The initial behavioural specification goes through significant optimizing transformations before being mapped to an architecture during embedded system design. Establishing the validity of these transformations is crucial to ensure that the intended behaviour of a system has not been faultily altered during synthesis. Although a lot of these transformations are carried out using some automated tool(s), a significant portion of such transformations are still performed by expert programmers. Thus, there is a need to devise efficient translation validation methodologies to handle diverse code transformations. Many translation validation methods exist which depend on hints provided by the compiler, such as, what transformations have been applied and in what order. However, generating such hints requires a lot of tedious probing into the compilers; the task becomes more demanding when there are humans involved.

In this tutorial, we intend to present our translation validation framework to check equivalence between a source program and its transformed version, both represented using the control and data flow graph (CDFG) or Finite State Machine with Data path (FSMD) model or its extension, while being completely unaware of the underlying compiler. The tutorial will start with illustrating common compiler optimization techniques with their impact on performance in terms of power, area and timing. Next, we will discuss basic program verification techniques like Hoare logic, Theorem Proving, Model Checking, Program equivalence using SMT solvers, etc. We will show why equivalence checking method is most suitable for verifying compiler optimizations. Next, we will present our FSMD based equivalence checking method in detail. Next, we will discuss how bisimulation relations can be inferred from equivalence checkers. We conclude with discussing the future direction of research in this domain.

Presenter Information

Dr. Kunal Banerjee is currently a Research Scientist at Intel’s Parallel Computing Lab in Bangalore, India. His research interests are in the areas of program analysis, formal methods and parallel programming. He received his B Tech degree in Computer Science and Engineering from Heritage Institute of Technology. He received his PhD from the Department of Computer Science and Engineering, IIT Kharagpur. He has been a recipient of Senior Research Fellowship from the Department of Science and Technology, India, and TCS Research Fellowship for supporting his doctoral studies.

Dr. Chandan Karfa is currently working as an Assistant Professor is the Department of Computer Science and Engineering, IIT Guwahati. Prior to that, he has worked for five years as Sr. R&D Engineer in Synopsys (India) Pvt. Ltd. He has obtained his MS and PhD degree in Computer Science and Engineering from IIT Kharagpur. His research interests include formal verification of compiler transformations, high-level synthesis and formal methods. He has published more than twenty research papers in reputed international journals and conferences. He has received TechnoInventor Award by India Electronics and Semiconductor Association in 2014, Innovative Student Projects Award from Indian National Academy of Engineers in 2008 and 2013, Best Paper Award in ADCOM conference in 2007 and I-CARE conference in 2013, Microsoft Research India PhD Fellowship in 2008, First prize in EDA contest in VLSI Design conference in 2009.

Type
Half-day tutorial