SOFSEM   2017 :=   Keynotes

Invited talks covering an entire session will span the entire spectrum of SOFSEM.

• Jaakko Hollmèn (Aalto University, Finland )

  Jaakko Hollmén (born 1970) received his M. Sc. (Tech.) degree in 1996 and his D. Sc. (Tech.) degree with distinction from Helsinki University of Technology in Espoo, Finland in 2000. Currently, he is faculty member at the Department of Computer Science at Aalto University in Espoo, Finland. His research interests include data analysis, machine learning and data mining, with applications in health and in environmental informatics. He is a Senior Member of IEEE. He has chaired several conferences in his areas of interest, including IDA, DS, and IEEE Computer-Based Medical Systems. Currently, he is co-chair of the Program Committee of ECML-PKDD 2017, which is held in Skopje, Macedonia during September 19-23, 2017. His publications can be found at https://users.ics.aalto.fi/jhollmen/Publications.

  Trends and Challenges in Predictive Analytics

  Predictive analytics is one of the most popular areas in machine learning and data mining. I will start by reviewing some fundamentals in data science and then focus on time series analysis and prediction. In the talk, I will present recent trends in predictive analytics, covering reducing dimensionality of the data space, stream processing, learning interpretable models, and connections to multi-label classification. I will also speak about patterns of missing data and its implications on predictive analytics in stream processing where no missing data imputation is possible. The solutions will be demonstrated in the areas of environmental informatics, medical science and transportation areas.

• Kim Guldstrand Larsen (Aalborg University, Denmark )

  Kim G. Larsen is a professor in the Department of Computer Science at Aalborg University within the Distributed and Embedded Systems Unit and director of the ICT-competence center CISS, Center for Embedded Software Systems. In 2015, he won an ERC Advanced Grant with the project LASSO for learning, analysis, synthesis and optimization of cyber physical systems. He is also director of the Sino-Danish Basic Research Center IDEA4CPS, the Danish Innovation Network InfinIT, as well as the newly founded innovation research center DiCyPS: Data Intensive Cyber Physical Systems. Kim G. Larsen is prime investigator of the tool UPPAAL and co-founder of the company UP4ALL International. In 2013 he was the recipient of the CAV Award for his work on UPPAAL as "the foremost model checker for real-time Systems". Kim G. Larsen became Honorary Doctor (Honoris causa) at Uppsala University, Sweden, in 1999. In 2007 he became Knight of the Order of the Dannebrog. In 2007 he became Honorary Doctor (Honoris causa) at ENS Cachan, France. In 2012 he became Honary Member of Academia Europaea. Since 2016 he has been appointed INRIA International Chair for a 5 year period. Also he has won the prestigious industrial Grundfos Award 2016.

  Dependable and Optimal Cyber-Physical Systems

  Cyber-Physical Systems(CPS) describe systems combining computing elements with dedicated hardware and software having to monitor and control a particular physical environment. This combination of the physical and virtual world provides the digital foundation for smart solutions throughout society and within all sectors. The constant demand for increased functionality and performance that needs to be produced with tight time schedules and cost budges challenges without compromising dependability of the final products constitutes a significant challenge. What is needed are improved, scalable methods, tools and techniques that support the development of CPS. In the keynote talk we will present a model-based approached for the design of dependable and optimal CPS, that are powered by the tool UPPAAL (www.uppaal.org). The underlying formalism of UPPAAL is that of timed automata with support for so-called model checking. In the talk we will survey the various branches of the UPPAAL tool suite – developed over a 20 year period – and how they support various important faces of the development process including testing, verification and performance evaluation. Moreover recent branches of UPPAAL allow for fully automatic generation of safe and optimal control software to be obtained directly from requirement. The keynote will report on the concerted application to a range of industrial CPS examples.

• Axel Legay (Rennes University, INRIA, France )

  Axel Legay is a permanent researcher at Inria Rennes (France) and an Industry Professor at Aalborg University (Denmark). He obtained a PhD thesis from the University of Liège (Belgium, 2007) and an habilitation thesis from the University of Rennes (France, 2015). He received several awards including the IBM prize for the best thesis in Computer Science (2008) and the Velux Prize (2014). Legay is the co-author of more than 250 publications in premier conferences and journals. Legay leads the Inria efforts on security and Systems of Systems. His main research interests are in developing formal specification and verification techniques for Software Engineering. His original contributions are in verification of infinite-state systems for which he offered one of the first generic approaches. He also made significant contributions in the area of modal transition systems and product line engineering. Legay is best known for his contribution to Statistical Model Checking for which he offered extension algorithms for rare events and non-determinism. His tool Plasma is used by both academics and engineers.

  On Featured Transition Systems

  Software Product Lines (SPLs) are families of similar software products built from a common set of features. As the number of products of an SPL is potentially exponential in the number of its features, analysing SPLs is harder than for single software. In this invited paper, we synthesise six years of eorts in alleviating SPL verication and testing issues. To this end, we introduced Featured Transition Systems (FTS) as a compact behavioural model for SPLs. Based on this formalism, we designed verication algorithms and tools allowing to check temporal properties on FTS, thereby assessing the correct behaviour of all the SPL products. We also used FTS to dene test coverage and generation techniques for model-driven SPLs. We also successfully employed the formalism in order to foster mutation analysis. We conclude with future directions on the development of FTS for SPL analysis.

• Marjan Mernik (University of Maribor, Slovenia )

  Marjan Mernik received the M.Sc. and Ph.D. degrees in computer science from the University of Maribor in 1994 and 1998 respectively. He is currently a professor at the University of Maribor, Faculty of Electrical Engineering and Computer Science. He is also a visiting professor at the University of Alabama at Birmingham, Department of Computer and Information Sciences, and at the University of Novi Sad, Faculty of Technical Sciences. His research interests include programming languages, compilers, domain-specific (modeling) languages, grammar-based systems, grammatical inference, and evolutionary computations. He is a member of the IEEE, ACM and EAPLS. Dr. Mernik is the Editor-In-Chief of Computer Languages, Systems and Structures journal, as well as Associate Editor of Applied Soft Computing journal.

  Domain-Specific Languages: A Systematic Mapping Study

  Domain-specific languages (DSLs) assist a software developer (or end-user) in writing a program using idioms that are similar to the abstractions found in a specific problem domain. Indeed, the enhanced software productivity and reliability benefits that have been reported from DSL usage are hard to ignore and DSLs are flourishing. However, tool support for DSLs is lacking when compared to the capabilities provided for standard General-Purpose Languages (GPLs). For example, support for unit testing of a DSL program, as well as DSL debuggers, are rare. A Systematic Mapping Study (SMS) has been performed to better understand the DSL research field, identify research trends, and any possible open issues. In this talk I will first introduce DSLs by discussing when and how to develop DSLs, then results from SMS will be presented along with open DSL problems such as lacking tool support for DSLs and difficulties in combining DSLs.

• Óscar Pastor López (Polytechnic University of Valencia, Spain )

  Full Professor and Director of the Research Center on "Métodos de Producción de Software (PROS)" at the Universidad Politécnica de Valencia (Spain). He received his Ph.D. in 1992. He was a researcher at HP Labs, Bristol, UK. He has published more than two hundred research papers in conference proceedings, journals and books, received numerous research grants from public institutions and private industry, and been keynote speaker at several conferences and workshops. Chair of the ER Steering Committee, and member of the SC of conferences as CAiSE, ICWE, CIbSE or RCIS, his research activities focus on conceptual modeling, web engineering, requirements engineering, information systems, and model-based software production. He created the object-oriented, formal specification language OASIS and the corresponding software production method OO-METHOD. He led the research and development underlying CARE Technologies that was formed in 1996. CARE Technologies has created an advanced MDA-based Conceptual Model Compiler called IntegraNova, a tool that produces a final software product starting from a conceptual schema that represents system requirements. He is currently leading a multidisciplinary project linking Information Systems and Bioinformatics notions, oriented to designing and implementing tools for Conceptual Modeling-based interpretation of the Human Genome information.

  Model-driven Development in Practice: From Requirements to Code

  A crucial success factor in information systems development is the alignment of the final software product with business goals, business semantics and business processes. Develo-pers should be freed from programming concerns and be able to concentrate on these alignment problems. To assess that the right capabilities are used, sound Conceptual Modeling (CM) techniques within a Model-driven system development (MDD) must be applied in order to provide a structured and systematic approach to systems development, where developers can successfully use model transformation technologies to derive models of a lower abstraction level that can be further refined, even generating software code automatically. From the experience got with the use of advanced MDD platforms, this keynote will show how to use a Capability-driven Development (CDD) strategy in order to integrate business process modelling (BPM), requirements engineering (RE) and object-oriented conceptual modelling with the objective of leveraging MDD capabilities. The current state of the art on modelling methods and code generation tools will be discussed to explore different ways to match an information system with business requirements. Concrete principles, concepts and common practices of MDD will be presented with a special focus on model-driven requirements engineering, meaning by it how BPM and requirements models can be embedded in a complete CM-based software production process.

• Paul G. Spirakis (University of Liverpool, United Kingdom ) and Othon Michail (University of Patras, Greece )

  Paul G. Spirakis was born in 1955. He got his undergraduate Electr. Eng. Diploma from NTUA Greece and his MSc and PhD form Harvard University USA. He has been a post-doc at Harvard , then a faculty at NYU – Courant Institute and then a Professor in the Dept. of Computer Eng. and Informatics of Patras University in Greece. He has been the Director of the major Greek Institute CTI from 1996 till Sept. 2016. He is now a Professor of Computer Science in the CS Dept. of the University of Liverpool UK. Paul is working on Algorithms and Complexity. He has done work in the fields of Distributed and Parallel Computing , in Random Graphs , network algorithms and recently in Algorithmic Game Theory. Paul is a Fellow of EATCS , a Member of Academia Europaea and a Member of the ACM Council Europe. Paul is now the President of EATCS and also the Editor in Chief in the Journal Theoretical Computer Science (TCS) in track A. Paul has published significantly in Algorithms and Complexity. Paul has served in many national and European high level bodies including being the Chair of the ERC Panel in Informatics for 2015-16.

  Network Constructors: A Model for Programmable Matter

  We discuss two recent theoretical models of programmable matter operating in a dynamic environment. In the first model, all devices are finite automata, begin from the same initial state, execute the same protocol, and can only interact in pairs. The interactions are scheduled by a fair (or uniform random) scheduler, in the spirit of Population Protocols. When two devices interact, the protocol takes as input their states and the state of the connection between them (on/off) and updates all of them. Initially all connections are off. The goal of such protocols is to eventually construct a desired stable network, induced by the edges that are on. We present protocols and lower bounds for several basic network construction problems and also universality results. We next discuss a more applied version of this minimal and abstract model, enriched with geometric constraints, aiming at capturing some first physical restrictions in potential future programmable matter systems operating in dynamic environments.

• Igor Walukiewicz (Bordeaux University, CNRS, France )

  Igor Walukiewicz received PhD degree in Computer Science from Warsaw University in 1994. After a long post-doctoral stay at Aarhus University he worked as a lecturer at Warsaw University. Since 2001 he is a CNRS researcher at Laboratoire Bordelais de Recherche en Informatique, Bordeaux, France. He made contributions to theoretical foundations of verification: mu-calculus, automata theory, infinite state model checking, distributed systems.

  Verifying Parametric Thread Creation

  Automatic verification of concurrent systems is an active area of research since at least a quater of a century. In this talk we will be interested in analyses of systems designed to operate with an arbitrary number of processes. German and Sistla, already in 1992, initiated in depth investigation of this problem for finite state systems. For infinite state systems, like pushdown systems, extra care is needed to avoid undecidability, as reachability is undecidable even for two identical pushdown processes communicating via single variable. Kahlon and Gupta in 2006 have proposed to use parametrization as means of bypassing this undecidability barrier. Indeed when instead of two pushdown processes we consider some unspecified number of them, the reachability problem becomes decidable.
  This idea of parametrization as an abstraction has been pursued further by Hague, who in 2011 has shown that the problem is still decidable when one of the pushdown processes is made different from the others: there is one leader process and many contributor processes. In more recent works [Esparza, Ganty, Majumdar], [Florin, Muscholl, Walukiewicz], the exact complexity of the reachability and the liveness problems has been established. In a recent joint work with Seidl and Muscholl we show that the idea of parametrization as an abstraction leads to decidability, and in some cases even efficient algorithms, for verification of systems which combine recursion with dynamic thread creation. Communication between threads is via global variables as well as via local variables that are shared between a thread and its sub-threads. This talk will present an overview of this line of research.